Natural Deduction

PROPOSITIONAL LOGIC PROOF BUILDER
empty
filled
proved
error
0:00

Begin Your Proof

Enter the formula you wish to prove. The tree grows upward from this root.

— or generate a provable formula —

SYNTAX GUIDE

/\ or \and∧conjunction
\/ or \or∨disjunction
-> or \to→implication
~ or \neg¬negation
_|_ or \bot⊥falsum
( )grouping
\forall x. P or \all x. P∀universal
\exists x. P or \ex x. P∃existential
P(x,y) f(x)predicates & functions
Precedence (high→low): ¬ > ∧ > ∨ > → > ∀ ∃. All right-associative. Quantifier scope extends as far right as possible.

SYNTAX GUIDE

/\  or  \and∧conjunction
\/  or  \or∨disjunction
->  or  \to→implication
~  or  \neg¬negation
_|_  or  \bot⊥false
\forall x. P∀universal
\exists x. P∃existential
A -> B {->I}{ }formula, then apply a rule
A {2}{n}formula, then cancel hypothesis n

Rule names in braces: →I →E ∧I ∧E1 ∧E2 ∨I1 ∨I2 ∨E ¬I ¬E ⊥E DNE LEM ∀I ∀E ∃I ∃E. Type them with the usual shortcuts, e.g. {/\I}, {\/I2}, {~E}, {_|_E}.

INFERENCE RULES

🎉 Proof Complete!

Proof History

Leaderboard