THE LOGIC EDITOR

Welcome to The Logic Editor!

Here you can do natural deduction proofs in propositional logic by entering premises and assumptions, and applying inference rules. This editor follows the rules of G. Forbes' "Modern Logic."

An example proof is currently shown. Click on “Clear all” to begin your own!

1
(1)
A → B
Premise
2
(2)
¬ B
Assumption
3
(3)
A
Assumption
1,3
(4)
B
1,3 →E
1,2,3
(5)
2,4 ¬E
1,2
(6)
¬ A
3,5 ¬I
1
(7)
¬ B → ¬ A
2,6 →I
A → B ⊢ ¬ B → ¬ A
Negation symbol
Conjunction symbol
Disjunction symbol
Conditional symbol
Biconditional symbol
Contradiction symbol
EFQ rule available

Note: If EFQ is used, your proof will not be registered in the database even if it is the shortest yet.

Propositional letters

The Logic Editor is created by Casper Storm Hansen. Please send me bug reports and other feedback. I would be happy to consider any requests for both new features and versions that follow systems of natural deduction different from that of G. Forbes' "Modern Logic."