Skip to content

First-order natural deduction

InductiveNatural deduction#✓fully proved

Fix a first-order language \(L\) and a type \(\alpha\) of variables; formulas and terms below are those of \(L\) with free variables in \(\alpha\). For a formula \(\varphi\) with one additional bound variable and a term \(t\), write \(\varphi[t]\) for \(\varphi\) with \(t\) substituted for that bound variable and \(\forall \varphi\) for its universal quantification. Write \(\neg \psi\) for \(\psi \to \bot\), and \(\psi, \Gamma\) for the list \(\Gamma\) with \(\psi\) added in front. Derivability \(\Gamma \vdash \varphi\) of a formula \(\varphi\) (the conclusion) from a finite list \(\Gamma\) of formulas (the open hypotheses) is the least relation closed under the following rules.

  • Assumption: \(\Gamma \vdash \varphi\) whenever \(\varphi\) is a member of \(\Gamma\).
  • Implication introduction: from \(\varphi, \Gamma \vdash \psi\) infer \(\Gamma \vdash \varphi \to \psi\).
  • Implication elimination: from \(\Gamma \vdash \varphi \to \psi\) and \(\Gamma \vdash \varphi\) infer \(\Gamma \vdash \psi\).
  • Reductio ad absurdum: from \(\neg \varphi, \Gamma \vdash \bot\) infer \(\Gamma \vdash \varphi\).
  • Universal introduction: if a variable \(x\) occurs free in no member of \(\Gamma\) and does not occur free in \(\varphi\), then from \(\Gamma \vdash \varphi[x]\) infer \(\Gamma \vdash \forall \varphi\).
  • Universal elimination: from \(\Gamma \vdash \forall \varphi\) infer \(\Gamma \vdash \varphi[t]\), for every term \(t\).
  • Reflexivity: \(\Gamma \vdash t = t\) for every term \(t\).
  • Substitution: from \(\Gamma \vdash s = t\) and \(\Gamma \vdash \varphi[s]\) infer \(\Gamma \vdash \varphi[t]\).
Cslib.Logic.FOL.Derivable · 24 lines 
inductive Derivable : List (L.Formula α) → L.Formula α → Prop
  /-- Use a hypothesis. -/
  | ax {Γ : List (L.Formula α)} {φ : L.Formula α} : φ ∈ Γ → Derivable Γ φ
  /-- `⟹`-introduction: discharge the hypothesis `φ`. -/
  | impI {Γ : List (L.Formula α)} {φ ψ : L.Formula α} :
      Derivable (φ :: Γ) ψ → Derivable Γ (φ.imp ψ)
  /-- `⟹`-elimination (modus ponens). -/
  | impE {Γ : List (L.Formula α)} {φ ψ : L.Formula α} :
      Derivable Γ (φ.imp ψ) → Derivable Γ φ → Derivable Γ ψ
  /-- Classical reductio ad absurdum. -/
  | byContra {Γ : List (L.Formula α)} {φ : L.Formula α} :
      Derivable (φ.not :: Γ) ⊥ → Derivable Γ φ
  /-- `∀`-introduction with an eigenvariable `x` free neither in `Γ` nor in `∀' φ`. -/
  | allI {Γ : List (L.Formula α)} {φ : L.BoundedFormula α 1} {x : α} :
      (∀ ψ ∈ Γ, x ∉ ψ.freeVarFinset) → x ∉ φ.freeVarFinset →
      Derivable Γ (instantiate (Term.var x) φ) → Derivable Γ φ.all
  /-- `∀`-elimination at a term. -/
  | allE {Γ : List (L.Formula α)} {φ : L.BoundedFormula α 1} (t : L.Term α) :
      Derivable Γ φ.all → Derivable Γ (instantiate t φ)
  /-- Reflexivity of equality. -/
  | refl {Γ : List (L.Formula α)} (t : L.Term α) : Derivable Γ (t.equal t)
  /-- Substitution of equals into a one-variable body. -/
  | subst {Γ : List (L.Formula α)} {φ : L.BoundedFormula α 1} {s t : L.Term α} :
      Derivable Γ (s.equal t) → Derivable Γ (instantiate s φ) → Derivable Γ (instantiate t φ)
Uses 1 · Used by 32
Statement usesInstantiating the outermost bound variable of a formula
Used byCut · Existential introduction · Soundness for theories · Weakening · Consistency of the calculus · Provability from a set of formulas · Injective relabeling preserves derivability · Injective renaming preserves derivability · Soundness of first-order natural deduction · Symmetry of equality in natural deduction · Transitivity of equality in natural deduction · Universal formulas from Henkin witnesses · Unions of chains of consistent sets are consistent · Consistency passes to the finite-symbol sublanguage · Henkin extension of a consistent set · Model existence for first-order logic · Model existence for arbitrary languages · Congruence for function symbols in a maximal consistent set · Deduction theorem · Adding a Henkin axiom preserves consistency · Universal instantiation in maximal consistent sets · Substitution of equals in maximal consistent sets · Derivations survive language homomorphisms · Modus ponens for provability from sets · Maximal consistent sets decide every formula · Ex falso for provability from sets · Provability as inconsistency with the negation · Refutability as inconsistency · Truth lemma for the first-order term model · Doubling the variables preserves consistency · Renaming free variables along an arbitrary map preserves derivability · Provable equality of terms
12 fully proved

Soundness

TheoremSoundness of first-order natural deduction#✓fully proved

Let \(\Gamma\) be a finite list of formulas of a first-order language \(L\) with free variables in \(\alpha\), and let \(\varphi\) be such a formula. If \(\Gamma \vdash \varphi\) in natural deduction, then for every \(L\)-structure \(M\) and every assignment \(v \colon \alpha \to M\) under which all members of \(\Gamma\) hold, \(\varphi\) holds under \(v\).

theorem sound {Γ : List (L.Formula α)} {φ : L.Formula α} (h : Derivable Γ φ) {M : Type*}
    [L.Structure M] (v : α → M) (hΓ : ∀ ψ ∈ Γ, ψ.Realize v) : φ.Realize v
Uses 5 · Used by 2
Statement usesNatural deduction
Proof usesInstantiating the outermost bound variable of a formula · Truth of a universal formula · Truth depends only on the free variables · Truth of an instance
Used bySoundness for theories · Consistency of the calculus

Renaming and weakening

TheoremInjective renaming preserves derivability#✓fully proved

Let \(f \colon \alpha \to \beta\) be an injective map between types of variables. For a formula \(\psi\) of a first-order language \(L\) with free variables in \(\alpha\), write \(f(\psi)\) for the renaming of the free variables of \(\psi\) by \(f\), and for a finite list \(\Gamma\) of such formulas write \(f(\Gamma)\) for the list obtained by renaming each member of \(\Gamma\). If \(\Gamma\) is such a list, \(\varphi\) is such a formula and \(\Gamma \vdash \varphi\) in natural deduction, then \(f(\Gamma) \vdash f(\varphi)\).

On formulas this renaming coincides with Mathlib's relabeling of free variables.

theorem rename {β : Type w'} [DecidableEq β] {f : α → β} (hf : Function.Injective f)
    {Γ : List (L.Formula α)} {φ : L.Formula α} (h : Derivable Γ φ) :
    Derivable (Γ.map (FOL.rename f)) (FOL.rename f φ)
Uses 6 · Used by 2
Statement usesNatural deduction · Renaming free variables of a formula
Proof usesFree variables of a renamed formula · Instantiating the outermost bound variable of a formula · Instantiating the outermost bound variable of a term · Renaming free variables of a term
Used byWeakening · Injective relabeling preserves derivability

TheoremInjective relabeling preserves derivability#✓fully proved

Let \(f \colon \alpha \to \beta\) be an injective map between types of variables. For a formula \(\psi\) of a first-order language \(L\) with free variables in \(\alpha\), write \(f(\psi)\) for Mathlib's relabeling of \(\psi\) by \(f\), which replaces each free variable \(x\) by \(f(x)\), and for a finite list \(\Gamma\) of such formulas write \(f(\Gamma)\) for the list obtained by applying this to each member of \(\Gamma\). If \(\Gamma\) is such a list, \(\varphi\) is such a formula and \(\Gamma \vdash \varphi\) in natural deduction, then \(f(\Gamma) \vdash f(\varphi)\).

theorem relabel {β : Type w'} [DecidableEq β] {f : α → β} (hf : Function.Injective f)
    {Γ : List (L.Formula α)} {φ : L.Formula α} (h : Derivable Γ φ) :
    Derivable (Γ.map (Formula.relabel f)) (φ.relabel f)
Uses 4
Statement usesNatural deduction
Proof usesInjective renaming preserves derivability · Relabelling a formula is renaming · Renaming free variables of a formula

TheoremWeakening#✓fully proved

Let \(\alpha\) be an infinite type of variables, let \(\Gamma\) and \(\Delta\) be finite lists of formulas of a first-order language \(L\) with free variables in \(\alpha\) such that every member of \(\Gamma\) is a member of \(\Delta\), and let \(\varphi\) be such a formula. If \(\Gamma \vdash \varphi\) in natural deduction, then \(\Delta \vdash \varphi\).

theorem mono [Infinite α] {Γ : List (L.Formula α)} {φ : L.Formula α} (h : Derivable Γ φ) :
    ∀ {Δ : List (L.Formula α)}, Γ ⊆ Δ → Derivable Δ φ
Uses 7 · Used by 5
Statement usesNatural deduction
Proof usesInjective renaming preserves derivability · Instantiating the outermost bound variable of a formula · Instantiating the outermost bound variable of a term · Renaming free variables of a formula · Renaming free variables of a term · Renaming that fixes the free variables
Used byDeduction theorem · Adding a Henkin axiom preserves consistency · Modus ponens for provability from sets · Ex falso for provability from sets · Provability as inconsistency with the negation

Derived rules

TheoremCut#✓fully proved

Let \(\Gamma\) be a finite list of formulas of a first-order language \(L\) with free variables in \(\alpha\), let \(\varphi\) and \(\psi\) be such formulas, and write \(\varphi, \Gamma\) for the list \(\Gamma\) with \(\varphi\) added in front. If \(\Gamma \vdash \varphi\) and \(\varphi, \Gamma \vdash \psi\) in natural deduction, then \(\Gamma \vdash \psi\).

theorem cut {Γ : List (L.Formula α)} {φ ψ : L.Formula α} (h₁ : Derivable Γ φ)
    (h₂ : Derivable (φ :: Γ) ψ) : Derivable Γ ψ
Uses 1 · Used by 1
Statement usesNatural deduction
Used byExistential introduction

TheoremExistential introduction#✓fully proved

Let \(\Gamma\) be a finite list of formulas of a first-order language \(L\) with free variables in \(\alpha\), let \(\varphi\) be such a formula with one additional bound variable, let \(t\) be a term, and write \(\varphi[t]\) for \(\varphi\) with \(t\) substituted for that bound variable. If \(\Gamma \vdash \varphi[t]\) in natural deduction, then \(\Gamma \vdash \exists \varphi\), where \(\exists \varphi\) abbreviates \(\neg \forall \neg \varphi\) as in Mathlib.

theorem exI {Γ : List (L.Formula α)} {φ : L.BoundedFormula α 1} (t : L.Term α)
    (h : Derivable Γ (instantiate t φ)) : Derivable Γ φ.ex
Uses 4
Statement usesNatural deduction · Instantiating the outermost bound variable of a formula
Proof usesCut · Instantiating the outermost bound variable of a term

TheoremSymmetry of equality in natural deduction#✓fully proved

Let \(\Gamma\) be a list of first-order formulas and let \(s\) and \(t\) be terms. If the equation \(s = t\) is derivable from the hypotheses \(\Gamma\), then the equation \(t = s\) is derivable from \(\Gamma\).

theorem symm {Γ : List (L.Formula α)} {s t : L.Term α} (h : Derivable Γ (s.equal t)) :
    Derivable Γ (t.equal s)
Uses 3 · Used by 3
Statement usesNatural deduction
Proof usesInstantiating the outermost bound variable of a formula · Instantiating the outermost bound variable of a term
Used byModel existence for first-order logic · Truth lemma for the first-order term model · Provable equality of terms

TheoremTransitivity of equality in natural deduction#✓fully proved

Let \(\Gamma\) be a list of first-order formulas and let \(r\), \(s\) and \(t\) be terms. If the equations \(r = s\) and \(s = t\) are both derivable from the hypotheses \(\Gamma\), then the equation \(r = t\) is derivable from \(\Gamma\).

theorem trans {Γ : List (L.Formula α)} {r s t : L.Term α} (h₁ : Derivable Γ (r.equal s))
    (h₂ : Derivable Γ (s.equal t)) : Derivable Γ (r.equal t)
Uses 3 · Used by 3
Statement usesNatural deduction
Proof usesInstantiating the outermost bound variable of a formula · Instantiating the outermost bound variable of a term
Used byModel existence for first-order logic · Truth lemma for the first-order term model · Provable equality of terms

Theories

DefinitionProvability from a set of formulas#✓fully proved

A set \(T\) of formulas of a first-order language \(L\) with free variables in \(\alpha\) proves such a formula \(\varphi\) when there is a finite list \(\Gamma\) of members of \(T\) with \(\Gamma \vdash \varphi\) in natural deduction.

def Provable (T : Set (L.Formula α)) (φ : L.Formula α) : Prop :=
  ∃ Γ : List (L.Formula α), (∀ ψ ∈ Γ, ψ ∈ T) ∧ Derivable Γ φ
Uses 1 · Used by 26
Statement usesNatural deduction
Used bySoundness for theories · Universal formulas from Henkin witnesses · Consistent set of formulas · Unions of chains of consistent sets are consistent · Consistency passes to the finite-symbol sublanguage · Henkin extension of a consistent set · Model existence for first-order logic · Model existence for arbitrary languages · Congruence for function symbols in a maximal consistent set · Deduction theorem · Adding a Henkin axiom preserves consistency · Maximal consistent sets of first-order formulas are deductively closed · Modus ponens for provability from sets · Maximal consistent sets decide every formula · Ex falso for provability from sets · Soundness and completeness of first-order natural deduction · Soundness and completeness for arbitrary languages · Provability as inconsistency with the negation · Refutability as inconsistency · Strong completeness of first-order natural deduction · Strong completeness for arbitrary languages · Completeness of first-order natural deduction for theories · Completeness for arbitrary languages · Truth lemma for the first-order term model · Doubling the variables preserves consistency · Provable equality of terms

TheoremSoundness for theories#✓fully proved

Let \(T\) be a theory, that is, a set of sentences of a first-order language \(L\), and regard each sentence of \(T\) as a formula with free variables in \(\alpha\). If a formula \(\varphi\) with free variables in \(\alpha\) is provable from these formulas, then \(\varphi\) holds in every model of \(T\) under every assignment of elements of the model to the variables in \(\alpha\).

theorem Provable.models {T : L.Theory} {φ : L.Formula α}
    (h : Provable (Formula.relabel Empty.elim '' T) φ) : T.ModelsBoundedFormula φ
Uses 3 · Used by 2
Statement usesProvability from a set of formulas
Proof usesNatural deduction · Soundness of first-order natural deduction
Used bySoundness and completeness of first-order natural deduction · Soundness and completeness for arbitrary languages

TheoremConsistency of the calculus#✓fully proved

The empty context does not derive ⊥.

theorem not_derivable_nil_bot : ¬ Derivable ([] : List (L.Formula α)) ⊥
Uses 2
Statement usesNatural deduction
Proof usesSoundness of first-order natural deduction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.