We stipulate that a proof P proves a formula φ from a set of formulas Γ (written ⌜P proves Γ ⊢ φ⌝) just in case it does so according to the rules listed in § 3 below.
If A is a proof and φ is a formula, then A|φ is the result of replacing every atomic sub-proof
in A with the nullary proof
A term is closed just in case it does not contain any variables. In other words:
All constants are closed terms.
If t₁,...,tₙ are closed terms, and f is an n-place function symbol, then ⌜f(t₁,...,tₙ)⌝ is a closed term.
Nothing else is a closed term.
If φ is a formula, x is a variable, and t is closed term, then φ(t/x) is the result of replacing every free ocurrence of x in φ with t.
For every formula φ, ψ and χ, set of formulas Γ, Δ, and Σ, and for every proof A, B, and C:
By the rule of assumption, the atomic proof
proves Γ ∪ {φ} ⊢ φ.
If A proves Γ ⊢ φ, and B proves Δ ⊢ ψ, then
proves Γ ∪ Δ ⊢ φ ∧ ψ.
If A proves Γ ⊢ φ ∧ ψ, then
proves Γ ⊢ φ, and
proves Γ ⊢ ψ.
If A proves Γ ⊢ φ, then
proves Γ ⊢ φ ∨ ψ, and
proves Γ ⊢ ψ ∨ φ.
If A proves Γ ⊢ φ ∨ ψ, B proves Δ ⊢ χ, and C proves Σ ⊢ χ, then
proves Γ ∪ (Δ - {φ}) ∪ (Σ - {ψ}) ⊢ χ.
If A proves Γ ⊢ ψ, then
proves Γ - {φ} ⊢ φ → ψ.
If A proves Γ ⊢ φ → ψ, and B proves Δ ⊢ φ, then
proves Γ ∪ Δ ⊢ ψ.
If A proves Γ ⊢ φ → ψ, and B proves Δ ⊢ ψ → φ, then
proves Γ ∪ Δ ⊢ φ ↔ ψ.
If A proves Γ ⊢ φ ↔ ψ, then
proves Γ ⊢ φ → ψ, and
proves Γ ⊢ ψ → φ.
If A proves Γ ⊢ ψ, and B proves Δ ⊢ ¬ψ, then
proves (Γ - {φ}) ∪ (Δ - {φ}) ⊢ ¬φ.
If A proves Γ ⊢ ψ, and B proves Δ ⊢ ¬ψ, then
proves (Γ - {¬φ}) ∪ (Δ - {¬φ}) ⊢ φ.
For every formula φ and ψ, variable x, closed term t, constant c, set of formulas Γ and Δ, and for every proof A and B:
If A proves Γ ⊢ φ(c/x), and c does not occur in Γ nor in φ, then
proves Γ ⊢ ∀x φ.
If A proves Γ ⊢ ∀x φ, then
proves Γ ⊢ φ(t/x).
If A proves Γ ⊢ φ(t/x), then
proves Γ ⊢ ∃x φ.
If A proves Γ ⊢ ∃x φ, B proves Δ ⊢ ψ, and c does not occur in (Δ - {φ(c/x)}), in φ, nor in ψ, then
proves Γ ∪ (Δ - {φ(c/x)}) ⊢ ψ.
For every formula φ, closed term s and t, set of formulas Γ and Δ, and for every proof A and B:
By the rule of identity introduction,
proves Γ ⊢ t = t.
If A proves Γ ⊢ s = t, B proves Δ ⊢ φ, and φ(s/t) is the result of replacing zero or some occurrences of t in φ with s, then
proves Γ ∪ Δ ⊢ φ(s/t).