Talk:Fitch-style calculus
From Wikipedia, the free encyclopedia
[edit] Proof example
I am not an expert, but the example doesn't seem to make sense. For example, in line 5, something from the same line (and line 2) is introduced, which sounds impossible to me, since we are currently on line 5, so there can't be a premise there. Also, shouldn't the elim in line 4 mention it's elim type and premise 2 as well? And finally, this doesn't seem to prove P, but actually ~(~P->Q). I'll rewrite it to something else when I get time, unless someone tells me that I am telling nonsense here (it's been a while). --Menesteus 18:40, 22 January 2007 (UTC)
- You're right, it does look like nonsense to me (the article that is, not your reply). Also, the last conclusion (~~P -> P) is not actually ~ Elim I think, but rather a derived rule. Also, one could justify the ~ Intro in (~~P) by "absurdity" Elim instead: we can eliminate the contradiction caused by ~P by assuming P. Anyway, a rewrite would be a good idea. Perhaps with the correct symbols and layout as well. --CompuChip 19:50, 9 March 2007 (UTC)
- In line 5, since I didn't know how to insert the "absurdity introduction" symbol, it looks a little redundant to say it twice, but it is the correct syntax. When you introduce the absurdity symbol, then you need to refer to the two places which make it absurd.
- In the last line the conclusion that "not-not-P" equals "P" is not really a derived rule. I think there's a wiki page for intuitionist logic, which disputes this claim about the law of excluded middle. But for Fitch-style proofs it's perfectly legitimate.
Acumensch 7:03, 26 April 2007
-
- definately works. I'll see if I can find the HTML version somewhere (wouldn't be surprised if ⊥ worked :)) --CompuChip 15:03, 26 April 2007 (UTC)
- Edit: Found it on the contradiction page: ⊥. But clearly the above also work. And definately is spelled with an i. --CompuChip 15:05, 26 April 2007 (UTC)