Talk:Fitch-style calculus

From Wikipedia, the free encyclopedia

WikiProject Mathematics
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: Stub Class Low Priority  Field: Foundations, logic, and set theory
Please update this rating as the article progresses, or if the rating is inaccurate. Please also add comments to suggest improvements to the article.

[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

\perp 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)