Rules
Examples
Sequent
⊢
Proof
Proof Check
Enter a proof above to check it.
Each line: formula rule citations
Premises and assumptions share one label, A: at the top level A means premise; indented inside a subproof it opens that subproof. Close a subproof by returning to the outer level and citing it 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 A p A q E→ 1, 2
p → q A 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 |
|---|---|---|---|
A | Premise / Assumption | — | φ (top level: listed premise; indented: 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 |
| Identity rules | |||
=I | Identity Intro | — | τ = τ (any term τ) |
=E | Identity Elim | m, n | φ' from τ₁ = τ₂ and φ, substituting τ₁↔τ₂ |
| Type | Symbol |
|---|---|
/\ or & | ∧ |
\/ or | | ∨ |
-> | → |
~ | ¬ |
Ax / Ay / Az | ∀x / ∀y / ∀z |
Ex / Ey / Ez | ∃x / ∃y / ∃z |
\forall or \all | ∀ |
\exists or \ex | ∃ |