Talk:Partially ordered set

Am I wrong or follows asymmetry of a strict partial order already from irreflexivity and transitivity? If a < b and b < a then by transitivity would a < a which is a contradiction to irreflexivity. So b < a must be false ...

Yes, as your proof shows, irreflexivity and transitivity imply asymmetry. Although your proof makes use of Reductio ad absurdum, which in turn makes use of the law of the excluded middle which some mathematicians called intuitionists eschew. Paul August ☎ 17:53, Jan 6, 2005 (UTC)

Hold on, what makes that proof non-constructive? We're asked to show that

${\displaystyle \lnot (a<b\land b<a)}$

which is equivalent, sometimes by definition, to

${\displaystyle (a<b\land b<a)\to \bot }$

in both classical and intuitionistic logic. Now prove the conditional by assuming its antecedent and deriving its consequent:

  ${\displaystyle a<b\land b<a}$ (assumption)
  ${\displaystyle (a<b\land b<a)\to a<a}$ (${\displaystyle \forall }$ elimination, from transitivity axiom)
  ${\displaystyle a<a\,\!}$ (${\displaystyle \to }$ elimination)
  ${\displaystyle a<a\to \bot }$ (${\displaystyle \forall }$ elimination, from irreflexivity axiom)
  ${\displaystyle \bot }$ (${\displaystyle \to }$ elimination)

Which proves the conditional. It's straightforward constructive reasoning, no? --MarkSweep 18:50, 6 Jan 2005 (UTC)

The first proof given above is non-contstructive since it is a proof by contradiction. Your proof may be constructive but I'm not an expert and I'm not sure if it does not somehow make use of the assumption that (A or not A) is always true. In particular I would wonder about the equivalence for (not A) that you use above, since in intuitionist logic (not A) is defined differently than in classical logic. Paul August ☎ 21:05, Jan 6, 2005 (UTC)

No, the first proof above is essentially the same proof as mine (with perhaps another layer of implication on the outside), and it is constructive. Just because a proof uses a contradiction ${\displaystyle \bot }$ doesn't mean it's non-constructive. If you define ${\displaystyle \lnot A}$ as ${\displaystyle A\to \bot }$ as usual, then natural deduction systems for classical, intuitionistic, and minimal logic only differ in terms of which (if any) form the elimination rule for ${\displaystyle \bot }$ takes. However, in the proof above, one doesn't eliminate ${\displaystyle \bot }$ at all, so it is in fact valid in minimal logic, which does not allow ${\displaystyle \bot }$ elimination. Observe:

1  ${\displaystyle (\forall x,y,z)x<y\land y<z\to x<z}$ [transitivity axiom]
2  ${\displaystyle (\forall x)\lnot (x<x)}$ [irreflexivity axiom]
3  | ${\displaystyle a<b\,\!}$ [assumption, a and b arbitrary]
4  | | ${\displaystyle b<a\,\!}$ [assumption]
5  | | ${\displaystyle a<b\land b<a}$ [${\displaystyle \land }$I 3,4]
6  | | ${\displaystyle a<b\land b<a\to a<a}$ [${\displaystyle \forall }$E 1]
7  | | ${\displaystyle a<a\,\!}$ [${\displaystyle \to }$E 5,6]
8  | | ${\displaystyle \lnot (a<a)}$ [${\displaystyle \forall }$E 2]
9  | | ${\displaystyle a<a\to \bot }$ [definition of ${\displaystyle \lnot }$ 8]
10 | | ${\displaystyle \bot }$ [${\displaystyle \to }$E 7,9]
11 | ${\displaystyle b<a\to \bot }$ [${\displaystyle \to }$I 4-10]
12 | ${\displaystyle \lnot (b<a)}$ [definition of ${\displaystyle \lnot }$ 11]
13 ${\displaystyle a<b\to \lnot (b<a)}$ [${\displaystyle \to }$I 3-12]
14 ${\displaystyle (\forall x,y)x<y\to \lnot (y<x)}$ [${\displaystyle \forall }$I 3-13]

Nowhere does this use an elimination rule for ${\displaystyle \bot }$, so it's valid in minimal logic. --MarkSweep 00:44, 7 Jan 2005 (UTC)

Well, I might be wrong ;-) but I assumed that the first poster's proof was essentially the following: Suppose a < b. We want to show that it is not the case that b < a. Now assume that b < a, then by transitivity, a < a, but this is a contradiction by irreflexivity, therefore since assuming b < a leads to a contradiction, b < a must be false, QED. Is this not an example of "proof by contradiction? Don't the intuitionists reject this method of proof? Paul August ☎ 01:09, Jan 9, 2005 (UTC)

Negated statements are "classical" (regular) so 'proofs by contradiction' are intuitionistically valid. DefLog 02:47, 9 Jan 2005 (UTC)