Natural Deduction

• Software
In order to help you to find proofs in natural deduction , I propose to use this PROVER.
The web presentation and the theorem prover principles are adaptations of the work of Professor Staerk assistant at ETH until 2005. You can find his prover here.

Let us consider a propositional formula.
If the formula has an intuitionistic proof, the prover gives you such a proof,i.e. a proof which does not use the reduction ad absurdum.
If the formula is valid, but not intuitionistically provable, the prover gives you a proof using the reduction ad absurdum.
Il the formula is not valid, the prover gives you a counter-model of the formule.
The intuitionistic proof search is based on the LJT system described in :
R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, J. Symb. Logic 57, pp 795--807, 1992. (ISSN 0022-4812)



• Documents
We recommand to read an History of Natural Deduction and Elementary Logic Textbooks written by Francis Jeffry Pelletier