Talk:Partially ordered set: Difference between revisions

Revision as of 02:47, 9 January 2005

Revision as of 05:53, 9 January 2005

Line 40:

::::Nowhere does this use an elimination rule for <math>\bot</math>, so it's valid in minimal logic. --[[User:MarkSweep|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? [[User:Paul August|Paul August ]] [[User_talk:Paul August|&#9742;]] 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 <math>\lnot P</math>, you have to prove <math>P \to \bot</math>, 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 <math>\bot</math> 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". --[[User:MarkSweep|MarkSweep]] 05:53, 9 Jan 2005 (UTC)

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