How to express the special property of a partial order? A partial order is a preorder with the following property:
$a\leq b \wedge b\leq a \implies a = b\quad(1)$
In my opinion, the following property it’s more intuitive:
$a\leq b \wedge b\leq c \implies a \neq c\quad(2)$
How do I prove they are equivalent?
First I start by saying $(1) \implies (2)$
$\lnot \big( (1) \land \lnot (2) \big)=\lnot(1)\lor(2) =$
$\lnot(a\leq b \land b\leq a\implies a=b)\lor(2)=$
$\lnot\Big(\lnot\big((a\leq b\land b\leq a)\land\lnot(a=b)\big)\Big)\lor(2)=$
$\big((a\le b\land b\le a)\land\lnot(a=b)\big)\lor(2)=$
$(a\le b\land b\le a \land a\ne b)\lor(2)=$
$(a\le b\land b\le a \land a\ne b)\lor\lnot\big((a\le b \land b \le c)\land\lnot(a\ne c)\big) = $
$(a\le b\land b\le a \land a\ne b)\lor\big(\lnot(a\le b \land b \le c)\lor(a\ne c)\big) =  \quad ...$
I’m kind of stuck there. Is there a way to continue showing that this is a tautology?
 A: Your alternative doesn't work, since a partial order is reflexive, and so if you pick $a=b=c$, then with your suggestion you get $a \not = a$, which is a contradiction.
A: Order relations come into two brands: strict and loose. Actually, they’re equivalent formulations, when the identity relation is available.
Let’s talk about relations on the set $A$. A relation $R$ on $A$ is areflexive if $(a,a)\notin R$, for all $a\in A$.
A strict preorder is just a transitive relation. A strict order is an areflexive and transitive relation.
A loose preorder is a reflexive and transitive relation. A loose order is a reflexive, antisymmetric (the property you seem not to like) and transitive relation.
Note that the identity relation is needed for stating the antisymmetric property.
How can one pass from strict to loose (pre)orders? Of course we need to have the identity relation available.
Suppose $S$ is a strict (pre)order on $A$ and define
$$
S^+=S\cup\{(a,a):a\in A\}
$$
It’s easy to show that $S^+$ is transitive as well. It is also reflexive by construction. Hence $S^+$ is a loose preorder when $S$ is a strict preorder.
Suppose $S$ is a strict order and also that $(a,b)\in S^+$ and $(b,a)\in S^+$. We cannot have $a\ne b$, because otherwise $(a,b)\in S$ and $(b,a)\in S$ and, by transitivity, $(a,a)\in S$: a contradiction to $S$ being areflexive. Therefore $a=b$ and so $S^+$ is antisymmetric.
Thus, from any strict order $S$ we obtain a loose one. Conversely, if $L$ is a loose order on $A$, it can be easily proved that
$$
L^-=L\setminus\{(a,a):a\in A\}
$$
is a strict order on $A$. Moreover, it is obvious that


*

*if $S$ is a strict order, then $S=(S^+)^-$;

*if $L$ is a loose order, then $L=(L^-)^+$.


Hence there’s no real difference between strict and loose orders on $A$: they correspond bijectively.
In order that a strict preorder $S$ is a strict order, it is necessary and sufficient that

for all $a,b,c\in A$, if $(a,b)\in S$ and $(b,c)\in S$, then $a\ne c$.

Indeed, suppose $S$ is a strict order. Then $(a,b)\in S$ and $(b,a)\in S$ implies $(a,a)\in S$, by transitivity: a contradiction to $S$ being areflexive.
Conversely, suppose $S$ is a strict preorder that satisfies the above property and $(a,a)\in S$ (that is, $S$ is not areflexive). Then, with $b=c=a$, we have $(a,b)\in S$, $(b,c)\in S$ and $a=c$: a contradiction.
So your “more intuitive” property indeed characterizes strict preorders that are strict orders. But is it really more intuitive? This is a matter of preference. Strict (pre)orders can be defined with no appeal to the identity relation, but your property makes use of it (of its negation, but it’s the same).
For a loose preorder the property you like is definitely not equivalent to it being a loose order. Indeed, no loose order satisfies it for the simple reason it is reflexive.
