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 (line 3). We want to show that it is not the case that b < a. Now assume that b < a (line 4), then by transitivity (line 6), a < a (line 7), but this is a contradiction (line 10) by irreflexivity (line 8), therefore since assuming b < a leads to a contradiction (line 11), b < a must be false (line 12), 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)

I've taken the liberty of annotating your informal proof with pointers to lines of the formal proof, to make it clear that the formal proof is in fact a more explicit version of the informal proof. You wrote, "since assuming b < a leads to a contradiction, b < a must be false": this is true, but it's true by definition. This means if you want to show ${\displaystyle \lnot P}$, you have to prove ${\displaystyle P\to \bot }$, which will necessarily involve a contradiction, but it is not a proof by contradiction in my book. It's just a plain old conditional proof, where the formula you conditionally derive just happens to be a contradiction. "Proof by contradiction" means that you derive something from a contradiction, in other words, you eliminate the contradiction. Note that this is possible in intuitionistic logic, which has rule for ${\displaystyle \bot }$ elimination (in Natural Deduction), sometimes called "ex falso quodlibet", that allows you to derive any formula you want from a contradiction (but you cannot withdraw any assumptions, for that you need Classical logic). But in this case, the contradiction is not eliminated, and in that sense this is not a "proof by contradiction". --MarkSweep 05:53, 9 Jan 2005 (UTC)

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