Natural Deduction Prover A prover in natural deduction with Fitch style for classical propositional logic

, par Michel Lévy

The following prover provides proofs in natural deduction with Fitch style for any propositional formula that is valid in classical logic, and counter-models for any propositional formula that is invalid in classical logic.

Remarks :

Supposing that A is a formula taken as input to the above prover, then

  1. If A is intuitionistically valid, then the proof provided by the above prover is also an intuitionistic proof in natural deduction whose construction is based on the rules of Roy Dyckhoff’s sequent calculus LJT [1] also called now « G4ip » [2] [3].
  2. If A is valid only in classical logic, then its proof contains the classical absurdity rule RAA.
  3. If A is not a logical theorem, then the prover gives a counter-model that satisfies the negation of A.
  4. To get the annotated proof of A in Fitch style, please allow the popups of your browser for this website.

Voir en ligne : Michel Levy’s web page


[1 Dyckhoff R. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic. 1992;57(3):795-807. Available at: Consulté sans date.

[2 Negri S, Plato J von. Structural proof theory. Cambridge; 2001. [pages 122-125]

[3 Dyckhoff R, Negri S. Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic. Journal of Symbolic Logic. 2000.