Natural Deduction Proof Generator & Checker

Logic

First-order

Premises Conclusion

Edit tools
	Delete this line
	Add a line below `Enter`
	Begin a subproof below `Tab`
	End this subproof and add a line below `Shift`+`Enter`
	End this subproof and begin another below `Shift`+`Tab`

Syntax rules
TFL
Propositional variables	single uppercase letters (A-Z)
Not	not ¬ ~ ∼ - −
And	and ∧ ^ & . · *
Or	or ∨ \| +
Implies	imp → ⇒ ⊃ -> => >
Iff	iff ↔ ≡ <-> <=>
Contradiction	bot ⊥ XX # _
FOL
Atomic formulas	predicates applied to terms, or identities (P(a), L(x, y), a = b, etc.)
Predicates	single uppercase letters (A-Z)
Terms	constants, variables, or functions applied to terms (a, x, f(c), etc.)
Constants / Functions	single lowercase letters (a-r)
Variables	single lowercase letters (s-z)
Forall	forall ∀ Ax ⋀ !
Exists	exists ∃ Ex ⋁ ?
ML
Box	box ☐ []
Diamond	dia ◇ <>