Axioms and goal
Enter the statements you may use, then the statement you intend to prove.
Axioms
Enter a goal.
Logical symbols
Shorthand changes as you type: \forall, \exists, /\, \/, ->, <->, and \neg.
Supported proof moves
- Universal and existential instantiation/generalization
- Make-believe, detachment, and arbitrary-object worlds
- And introduction/elimination
- Or introduction and proof by cases
- De Morgan’s laws and double negation
- If-and-only-if introduction/elimination
References may name axioms such as A1 and earlier proof lines such as 2, 4. A closing move may omit its reference to use the most recent formula inside that world.
Your proof
Choose the justification for each line. The checker tracks which pretend world each line belongs to.