Talk:Fitch notation

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)

Yes, I think the example is wrong, I checked with Fitch proof system (Propositional). I'm changing the example with a correct proof.

-- MaD70 (talk) 17:29, 30 August 2014 (UTC)

Nevermind, I wasted my time: I cannot decide if using a screenshot from Proofmood is fair use or not. I wanted to show the proof of

A → B ∨ C ├ (A → B) ∨ (A → C).

What follows is the verified proof in raw ASCII form accepted by Proofmood for someone with a better knowledge of Wikipedia quirks and copyright policies:

[ A $ B | C entails [ ~((A $ B) | (A $ C)) entails [ A $ B entails (A $ B) | (A $ C) :| intro 3 ;^ :^ intro 4,2 ] ;~(A $ B) :~ intro 3-5 ;[ A entails B | C :$ elim 7,1 ;[ B entails [ A entails B :repeat 9 ] ;A $ B :$ intro 10-11 ;^ :^ intro 12,6 ;C :^ elim 13 ] ;[ C entails C :repeat 15 ] ;C :| elim 15-16,9-14,8 ] ;A $ C :$ intro 7-17 ;(A $ B) | (A $ C) :| intro 18 ;^ :^ intro 19,2 ] ;(A $ B) | (A $ C) :~ elim 2-20 ] !line_cnc21

Select the [Input] link in Fitch proof system (Propositional), a window opens, copy this proof into the textarea in such window and press the Go button: the proof will be rendered in HTML.

-- MaD70 (talk) 18:36, 30 August 2014 (UTC)

Note also that Proofmood can output LaTeX, which is accepted by Wikipedia (see Help:Displaying a formula), but it requires the use of its style file proofmood_en.sty, so I think such output it's not usable here. Can someone confirm this?

-- MaD70 (talk) 18:54, 30 August 2014 (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)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Fitch notation. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20130903114953/http://ssdi.di.fct.unl.pt/~pb/cadeiras/lc/0102/lpl%20textbook.pdf to http://ssdi.di.fct.unl.pt/~pb/cadeiras/lc/0102/lpl%20textbook.pdf

When you have finished reviewing my changes, please set the checked parameter below to true or failed to let others know (documentation at {{Sourcecheck}}).

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 12:46, 21 July 2016 (UTC)