Weak preferences and negative transitivity

Question

Let $ \succ $ be a binary relationship on the set $X$ such that, given any $ x, y, z\in X $, if $x\succ y$:

1. (Asymmetry): $\neg(y\succ x)$,
2. (Negative transitivity): $(x\succ z) \vee (z\succ y)$.

Let us define the abbreviations:

3. $x\succeq y \;:=\; \neg(y\succ x) $,

4. $x \sim y \;:=\; x\succeq y\; \wedge \;y \succeq x$.

As usual, the relations $\succ, \succeq, \sim$ denote strong preference, weak preference, and indifference.

Intuition suggests that I can conclude: $$x\succeq y \; \leftrightarrow \;(x\succ y\; \vee \;x\sim y) $$

If so, how can I derive it formally? Any useful references?

Answer 1

Probably it can be done easier if you do both steps separately ($\implies$ and $\impliedby$), but here is a proof that does both at the same time: \begin{align*} &x\succ y \vee x\sim y\\ \iff\;& x \succ y \vee (x\succeq y \wedge y \succeq x) & \text{Definition of $\sim$} \\ \iff\;& (x \succ y \vee x\succeq y) \wedge (x \succ y \vee y \succeq x)& \text{Distributivity}\\ \iff\;& [x \succ y \vee \neg( y \succ x)] \wedge [x \succ y \vee \neg(x\succ y)]& \text{Definition of $\succeq$}\\ \iff\;& x \succ y \vee \neg( y \succ x)& \text{LEM}\\ \iff\;& [x \succ y \vee \neg( y \succ x)] \wedge[x \succ y \to \neg( y \succ x)]& \text{Asymmetry}\\ \iff\;& [x \succ y \vee \neg( y \succ x)] \wedge[\neg(x \succ y) \vee \neg( y \succ x)]& \text{Definition of $\to$}\\ \iff\;& [x \succ y \wedge \neg(x \succ y)] \vee \neg( y \succ x)& \text{Distributivity}\\ \iff\;& \neg( y \succ x)& \text{Contradiction}\\ \iff\;& x \succeq y& \text{Definition of $\succeq$}\\ \end{align*}

Negative transitivity seems to not be a necessary condition for this proposition.