Rules
Examples
Sequent
⊢
Proof
Verification
Enter a proof above to check it.
Each line: formula rule citations
Subproofs are indented (use spaces). Open a subproof by starting an indented assumption (A). Close it by returning to the outer level and citing the subproof as a range m–n (assumption through last line), e.g. →I 2–3. Separate multiple line numbers with commas, e.g. ∧I 1, 2.
p → q P p P q →E 1, 2
p → q P p A q →E 1, 2 p → q →I 2–3
⊥ (falsum) — type as _|_, bot, or ⊥
Predicates: P Q R S T followed by terms, e.g. Pa, Rxy
Constants: a b c d e Variables: x y z
∀ / ∃ followed by a variable, then a formula, e.g. ∀xPx, ∃y(Py∧Qy)
| Rule | Name | Cite | Result |
|---|---|---|---|
P | Premise | — | φ (a listed premise) |
A | Assumption | — | φ (any; opens subproof) |
R | Repetition | n | φ |
∧I | Conj. Intro | m, n | φ∧ψ |
∧E | Conj. Elim | n | φ or ψ |
→E | Cond. Elim (MP) | m, n | ψ |
→I | Cond. Intro | m–n | φ→ψ (subproof m–n) |
∨I | Disj. Intro | n | φ∨ψ |
∨E | Disj. Elim | m, n, k | χ |
¬E | Neg. Elim | m, n | ⊥ |
¬I | Neg. Intro | m–n | ¬φ (subproof m–n) |
EFSQ | Ex Falso | n | any φ |
DN | Double Neg. | n | φ or ¬¬φ |
| Quantifier rules | |||
∀E | Universal Elim | n | φ(a/x) from ∀xφ |
∀I | Universal Intro | n | ∀xφ from φ(a/x), a fresh |
∃I | Existential Intro | n | ∃xφ from φ(a/x) |
∃E | Existential Elim | m, n | ψ from ∃xφ and φ(a/x)→ψ, a fresh |
| Type | Symbol |
|---|---|
/\ or & | ∧ |
\/ or | | ∨ |
-> | → |
~ | ¬ |
Ax / Ay / Az | ∀x / ∀y / ∀z |
Ex / Ey / Ez | ∃x / ∃y / ∃z |
\forall or \all | ∀ |
\exists or \ex | ∃ |