Gödel's completeness theorem

TheoremModus ponens for provability from sets#✓fully proved

Let \(L\) be a first-order language, let \(\alpha\) be an infinite type of variables, and let \(S\) be a set of formulas of \(L\) with free variables in \(\alpha\). For formulas \(\varphi\) and \(\psi\), if \(S\) proves \(\varphi \to \psi\) and \(S\) proves \(\varphi\), then \(S\) proves \(\psi\).

theorem mp [Infinite α] {S : Set (L.Formula α)} {φ ψ : L.Formula α}
    (h₁ : Provable S (φ.imp ψ)) (h₂ : Provable S φ) : Provable S ψ

Uses 3 · Used by 6

Statement usesProvability from a set of formulas

Proof usesNatural deduction · Weakening

Used byUniversal formulas from Henkin witnesses · Maximal consistent sets of first-order formulas are deductively closed · Maximal consistent sets decide every formula · Provability as inconsistency with the negation · Refutability as inconsistency · Truth lemma for the first-order term model

TheoremEx falso for provability from sets#✓fully proved

Let \(L\) be a first-order language, let \(\alpha\) be an infinite type of variables, and let \(S\) be a set of formulas of \(L\) with free variables in \(\alpha\). If \(S\) proves \(\bot\), then \(S\) proves every formula \(\varphi\).

theorem of_bot [Infinite α] {S : Set (L.Formula α)} {φ : L.Formula α}
    (h : Provable S ⊥) : Provable S φ

Uses 3

Statement usesProvability from a set of formulas

Proof usesNatural deduction · Weakening

TheoremDeduction theorem#✓fully proved

Let \(\alpha\) be an infinite set of variables, let \(S\) be a set of formulas with free variables in \(\alpha\), and let \(\varphi\), \(\psi\) be such formulas. If \(S \cup \{\varphi\}\) proves \(\psi\), then \(S\) proves \(\varphi \to \psi\).

theorem imp_of_insert [Infinite α] {S : Set (L.Formula α)} {φ ψ : L.Formula α}
    (h : Provable (insert φ S) ψ) : Provable S (φ.imp ψ)

Uses 3 · Used by 2

Statement usesProvability from a set of formulas

Proof usesNatural deduction · Weakening

Used byProvability as inconsistency with the negation · Refutability as inconsistency

DefinitionConsistent set of formulas#✓fully proved

Let \(L\) be a first-order language and \(\alpha\) a type of variables. A set \(S\) of formulas of \(L\) with free variables in \(\alpha\) is consistent when \(S\) does not prove \(\bot\).

def Consistent (S : Set (L.Formula α)) : Prop := ¬ Provable S ⊥

Uses 1 · Used by 19

Statement usesProvability from a set of formulas

Used byUnions of chains of consistent sets are consistent · Consistency passes to the finite-symbol sublanguage · Lindenbaum's lemma for first-order logic · Henkin extension of a consistent set · Model existence for first-order logic · Finite satisfiability · Model existence for arbitrary languages · Adding a Henkin axiom preserves consistency · Maximal consistent set · Maximal consistent sets absorb consistent extensions · Maximal consistent sets of first-order formulas are deductively closed · Maximal consistent sets decide every formula · Provability as inconsistency with the negation · Refutability as inconsistency · Strong completeness of first-order natural deduction · Strong completeness for arbitrary languages · Completeness for arbitrary languages · Truth lemma for the first-order term model · Doubling the variables preserves consistency

TheoremProvability as inconsistency with the negation#✓fully proved

Let \(L\) be a first-order language, let \(\alpha\) be an infinite type of variables, let \(S\) be a set of formulas of \(L\) with free variables in \(\alpha\), and let \(\varphi\) be a formula. Then \(S\) proves \(\varphi\) if and only if \(S \cup \{\neg\varphi\}\) is not consistent.

theorem provable_iff_not_consistent_insert_not [Infinite α] {S : Set (L.Formula α)}
    {φ : L.Formula α} : Provable S φ ↔ ¬ Consistent (insert φ.not S)

Uses 6 · Used by 3

Statement usesConsistent set of formulas · Provability from a set of formulas

Proof usesNatural deduction · Weakening · Deduction theorem · Modus ponens for provability from sets

Used byStrong completeness of first-order natural deduction · Strong completeness for arbitrary languages · Completeness for arbitrary languages

TheoremRefutability as inconsistency#✓fully proved

Let \(L\) be a first-order language, let \(\alpha\) be an infinite type of variables, let \(S\) be a set of formulas of \(L\) with free variables in \(\alpha\), and let \(\varphi\) be a formula. Then \(S\) proves \(\neg\varphi\) if and only if \(S \cup \{\varphi\}\) is not consistent.

theorem provable_not_iff_not_consistent_insert [Infinite α] {S : Set (L.Formula α)}
    {φ : L.Formula α} : Provable S φ.not ↔ ¬ Consistent (insert φ S)

Uses 5 · Used by 3

Statement usesConsistent set of formulas · Provability from a set of formulas

Proof usesNatural deduction · Deduction theorem · Modus ponens for provability from sets

Used byAdding a Henkin axiom preserves consistency · Maximal consistent sets of first-order formulas are deductively closed · Maximal consistent sets decide every formula

TheoremUnions of chains of consistent sets are consistent#✓fully proved

If \(C\) is a nonempty family of sets of formulas that is totally ordered by inclusion and every member of \(C\) is consistent, then the union \(\bigcup C\) is consistent.

A refutation uses only finitely many hypotheses, and these all lie in a single member of \(C\).

theorem consistent_sUnion_of_isChain {C : Set (Set (L.Formula α))} (hC : IsChain (· ⊆ ·) C)
    (hne : C.Nonempty) (hcons : ∀ c ∈ C, Consistent c) : Consistent (⋃₀ C)

Uses 3 · Used by 2

Statement usesConsistent set of formulas

Proof usesNatural deduction · Provability from a set of formulas

Used byLindenbaum's lemma for first-order logic · Henkin extension of a consistent set

AbbreviationMaximal consistent set#✓fully proved

A set \(\Delta\) of formulas is maximal consistent when it is consistent and every consistent set of formulas containing \(\Delta\) is contained in \(\Delta\), that is, equals \(\Delta\).

abbrev MaximalConsistent (Δ : Set (L.Formula α)) : Prop := Maximal Consistent Δ

Uses 1 · Used by 15

Statement usesConsistent set of formulas

Used byUniversal formulas from Henkin witnesses · Lindenbaum's lemma for first-order logic · Henkin extension of a consistent set · Model existence for first-order logic · Congruence for function symbols in a maximal consistent set · Universal instantiation in maximal consistent sets · Substitution of equals in maximal consistent sets · Maximal consistent sets absorb consistent extensions · Maximal consistent sets of first-order formulas are deductively closed · Maximal consistent sets decide every formula · Truth lemma for the first-order term model · Replacing an argument of a relation symbol by an equal term · Canonical assignment of the term model · Term model of a maximal consistent set · Provable equality of terms

TheoremMaximal consistent sets absorb consistent extensions#✓fully proved

Let \(\Delta\) be a maximal consistent set of first-order formulas of a language \(L\) with free variables in \(\alpha\), and let \(\varphi\) be a formula. If \(\Delta \cup \{\varphi\}\) is consistent, then \(\varphi \in \Delta\).

theorem MaximalConsistent.mem_of_consistent_insert {Δ : Set (L.Formula α)}
    (hΔ : MaximalConsistent Δ) {φ : L.Formula α} (h : Consistent (insert φ Δ)) : φ ∈ Δ

Uses 2 · Used by 2

Statement usesConsistent set of formulas · Maximal consistent set

Used byMaximal consistent sets of first-order formulas are deductively closed · Maximal consistent sets decide every formula

TheoremLindenbaum's lemma for first-order logic#✓fully proved

Every consistent set \(S\) of first-order formulas is contained in a maximal consistent set.

theorem exists_maximalConsistent {S : Set (L.Formula α)} (hS : Consistent S) :
    ∃ Δ, S ⊆ Δ ∧ MaximalConsistent Δ

Uses 3 · Used by 1

Statement usesConsistent set of formulas · Maximal consistent set

Proof usesUnions of chains of consistent sets are consistent

Used byHenkin extension of a consistent set

TheoremMaximal consistent sets of first-order formulas are deductively closed#✓fully proved

Let \(L\) be a first-order language, let \(\alpha\) be an infinite type of variables, and let \(\Delta\) be a maximal consistent set of formulas of \(L\) with free variables in \(\alpha\). Every formula \(\varphi\) that \(\Delta\) proves lies in \(\Delta\).

theorem mem_of_provable {φ : L.Formula α} (h : Provable Δ φ) : φ ∈ Δ

Uses 6 · Used by 8

Statement usesMaximal consistent set · Provability from a set of formulas

Proof usesConsistent set of formulas · Maximal consistent sets absorb consistent extensions · Modus ponens for provability from sets · Refutability as inconsistency

Used byUniversal formulas from Henkin witnesses · Model existence for first-order logic · Congruence for function symbols in a maximal consistent set · Universal instantiation in maximal consistent sets · Substitution of equals in maximal consistent sets · Maximal consistent sets decide every formula · Truth lemma for the first-order term model · Provable equality of terms

TheoremMaximal consistent sets decide every formula#✓fully proved

Let \(L\) be a first-order language, let \(\alpha\) be an infinite type of variables, and let \(\Delta\) be a maximal consistent set of formulas of \(L\) with free variables in \(\alpha\). For every formula \(\varphi\), \(\neg\varphi \in \Delta\) if and only if \(\varphi \notin \Delta\); so exactly one of \(\varphi\) and \(\neg\varphi\) lies in \(\Delta\).

theorem not_mem_iff {φ : L.Formula α} : φ.not ∈ Δ ↔ φ ∉ Δ

Uses 8 · Used by 2

Statement usesMaximal consistent set

Proof usesConsistent set of formulas · Natural deduction · Maximal consistent sets absorb consistent extensions · Maximal consistent sets of first-order formulas are deductively closed · Provability from a set of formulas · Modus ponens for provability from sets · Refutability as inconsistency

Used byUniversal formulas from Henkin witnesses · Truth lemma for the first-order term model

TheoremUniversal instantiation in maximal consistent sets#✓fully proved

Let \(\alpha\) be an infinite set of variables and let \(\Delta\) be a maximal consistent set of formulas with free variables in \(\alpha\). Let \(\varphi(x)\) be a formula with one bound variable \(x\) left open, and for a term \(t\) write \(\varphi(t)\) for the result of substituting \(t\) for \(x\). If \(\Delta\) contains \(\forall x\, \varphi\), then \(\Delta\) contains \(\varphi(t)\) for every term \(t\).

theorem instantiate_mem_of_all_mem {φ : L.BoundedFormula α 1} (h : φ.all ∈ Δ)
    (t : L.Term α) : instantiate t φ ∈ Δ

Uses 4 · Used by 1

Statement usesMaximal consistent set · Instantiating the outermost bound variable of a formula

Proof usesNatural deduction · Maximal consistent sets of first-order formulas are deductively closed

Used byTruth lemma for the first-order term model

TheoremSubstitution of equals in maximal consistent sets#✓fully proved

Let \(\alpha\) be an infinite set of variables and let \(\Delta\) be a maximal consistent set of formulas with free variables in \(\alpha\). Let \(\varphi(x)\) be a formula with one bound variable \(x\) left open, and for a term \(u\) write \(\varphi(u)\) for the result of substituting \(u\) for \(x\). If \(s\) and \(t\) are terms such that \(\Delta\) contains the equation \(s = t\) and the formula \(\varphi(s)\), then \(\Delta\) contains \(\varphi(t)\).

theorem instantiate_mem_of_equal {φ : L.BoundedFormula α 1} {s t : L.Term α}
    (h₁ : s.equal t ∈ Δ) (h₂ : instantiate s φ ∈ Δ) : instantiate t φ ∈ Δ

Uses 4 · Used by 2

Statement usesMaximal consistent set · Instantiating the outermost bound variable of a formula

Proof usesNatural deduction · Maximal consistent sets of first-order formulas are deductively closed

Used byCongruence for function symbols in a maximal consistent set · Replacing an argument of a relation symbol by an equal term

DefinitionHenkin axiom#✓fully proved

Let \(\varphi(x)\) be a formula with one bound variable \(x\) left open and let \(c\) be a variable; write \(\varphi(c)\) for the result of substituting \(c\) for \(x\). The Henkin axiom for \(\forall x\, \varphi\) with witness \(c\) is the formula \(\neg \forall x\, \varphi \to \neg \varphi(c)\).

def henkinAxiom (φ : L.BoundedFormula α 1) (c : α) : L.Formula α :=
  φ.all.not.imp (instantiate (Term.var c) φ).not

Uses 1 · Used by 4

Statement usesInstantiating the outermost bound variable of a formula

Used byUniversal formulas from Henkin witnesses · Henkin extension of a consistent set · The \(k\)-th Henkin axiom · Adding a Henkin axiom preserves consistency

TheoremAdding a Henkin axiom preserves consistency#✓fully proved

Let \(\alpha\) be an infinite set of variables and let \(S\) be a consistent set of formulas with free variables in \(\alpha\). Let \(\varphi(x)\) be a formula with one bound variable \(x\) left open, and let \(c \in \alpha\) be a variable that occurs free neither in \(\varphi\) nor in any formula of \(S\). Then \(S\) together with the Henkin axiom for \(\forall x\, \varphi\) with witness \(c\) is consistent.

theorem Consistent.insert_henkinAxiom [Infinite α] {S : Set (L.Formula α)}
    (hS : Consistent S) {φ : L.BoundedFormula α 1} {c : α}
    (hcS : ∀ ψ ∈ S, c ∉ ψ.freeVarFinset) (hcφ : c ∉ φ.freeVarFinset) :
    Consistent (insert (henkinAxiom φ c) S)

Uses 7 · Used by 1

Statement usesConsistent set of formulas · Henkin axiom

Proof usesNatural deduction · Weakening · Provability from a set of formulas · Instantiating the outermost bound variable of a formula · Refutability as inconsistency

Used byHenkin extension of a consistent set

TheoremUniversal formulas from Henkin witnesses#✓fully proved

Let \(\alpha\) be an infinite set of variables and let \(\Delta\) be a maximal consistent set of formulas with free variables in \(\alpha\). Let \(\varphi(x)\) be a formula with one bound variable \(x\) left open, let \(c \in \alpha\), and write \(\varphi(c)\) for the result of substituting \(c\) for \(x\). If \(\Delta\) contains the Henkin axiom for \(\forall x\, \varphi\) with witness \(c\) and contains \(\varphi(c)\), then \(\Delta\) contains \(\forall x\, \varphi\).

theorem MaximalConsistent.all_mem_of_henkin [Infinite α] {Δ : Set (L.Formula α)}
    (hΔ : MaximalConsistent Δ) {φ : L.BoundedFormula α 1} {c : α}
    (hH : henkinAxiom φ c ∈ Δ) (h : instantiate (Term.var c) φ ∈ Δ) : φ.all ∈ Δ

Uses 8 · Used by 1

Statement usesMaximal consistent set · Henkin axiom · Instantiating the outermost bound variable of a formula

Proof usesNatural deduction · Maximal consistent sets of first-order formulas are deductively closed · Maximal consistent sets decide every formula · Provability from a set of formulas · Modus ponens for provability from sets

Used byHenkin extension of a consistent set

TheoremFree variables of an instance#✓fully proved

Let \(t\) be a term and \(\varphi\) a first-order formula with \(m + 1\) bound variables, and let \(\varphi(t)\) be the instance obtained by substituting \(t\) for the outermost bound variable. Every free variable of \(\varphi(t)\) is a free variable of \(\varphi\) or a variable of \(t\).

theorem freeVarFinset_instantiate_subset (t : L.Term α) :
    ∀ {m : ℕ} (φ : L.BoundedFormula α (m + 1)),
      (instantiate t φ).freeVarFinset ⊆ φ.freeVarFinset ∪ t.varFinset

Uses 2 · Used by 1

Statement usesInstantiating the outermost bound variable of a formula

Proof usesInstantiating the outermost bound variable of a term

Used byHenkin extension of a consistent set

DefinitionDepth of a formula#✓fully proved

The depth \(d(\varphi)\) of a first-order formula \(\varphi\) is the nesting height of its implications and universal quantifiers: \(\bot\), equations and relation atoms have depth \(0\), the implication \(\varphi \to \psi\) has depth \(\max(d(\varphi), d(\psi)) + 1\), and \(\forall \varphi\) has depth \(d(\varphi) + 1\).

def depth : ∀ {n : ℕ}, L.BoundedFormula α n → ℕ
  | _, .falsum => 0
  | _, .equal _ _ => 0
  | _, .rel _ _ => 0
  | _, .imp φ ψ => max (depth φ) (depth ψ) + 1
  | _, .all φ => depth φ + 1

Used by 1

Used byTruth lemma for the first-order term model

TheoremRenaming depends only on the free variables#✓fully proved

Let \(\alpha\) and \(\beta\) be types of variables, let \(n \in \mathbb{N}\), and let \(\varphi\) be a formula with free variables in \(\alpha\) and \(n\) further variables reserved for binding by enclosing quantifiers. If two maps \(f, g : \alpha \to \beta\) agree on every variable from \(\alpha\) that occurs free in \(\varphi\), then renaming the variables of \(\varphi\) from \(\alpha\) along \(f\) and along \(g\) gives the same formula.

theorem rename_congr_of_eqOn {f g : α → β} {n : ℕ} {φ : L.BoundedFormula α n}
    (h : ∀ a ∈ φ.freeVarFinset, f a = g a) : rename f φ = rename g φ

Uses 2 · Used by 1

Statement usesRenaming free variables of a formula

Proof usesRenaming free variables of a term

Used byRenaming free variables along an arbitrary map preserves derivability

TheoremRenaming free variables along an arbitrary map preserves derivability#✓fully proved

Let \(\alpha\) and \(\beta\) be types of variables with \(\beta\) infinite, and let \(f : \alpha \to \beta\) be any map. If \(\varphi\) is derivable from the list of hypotheses \(\Gamma\) in natural deduction, then the formula obtained from \(\varphi\) by renaming each free variable \(x\) to \(f(x)\) is derivable from the list obtained by renaming the free variables of each formula of \(\Gamma\) in the same way.

The map need not be injective: in the proof each eigenvariable is sent to a fresh variable.

theorem Derivable.relabel_of_infinite [Infinite β] {Γ : List (L.Formula α)} {φ : L.Formula α}
    (h : Derivable Γ φ) (f : α → β) : Derivable (Γ.map (Formula.relabel f)) (φ.relabel f)

Uses 7 · Used by 1

Statement usesNatural deduction

Proof usesRelabelling a formula is renaming · 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 depends only on the free variables

Used byDoubling the variables preserves consistency

TheoremDoubling the variables preserves consistency#✓fully proved

If \(S\) is a consistent set of formulas with free variables in \(\mathbb{N}\), then the set obtained from \(S\) by renaming every free variable \(x\) to \(2x\) in each of its formulas is consistent.

Halving the variables maps any derivation of \(\bot\) from the renamed set back to one from \(S\).

theorem Consistent.relabel_double {S : Set (L.Formula ℕ)} (hS : Consistent S) :
    Consistent (Formula.relabel (2 * ·) '' S)

Uses 8 · Used by 1

Statement usesConsistent set of formulas

Proof usesNatural deduction · Renaming free variables along an arbitrary map preserves derivability · Provability from a set of formulas · Relabelling a formula is renaming · Renaming free variables of a formula · Renaming free variables of a term · Renaming that fixes the free variables

Used byModel existence for first-order logic

TheoremReplacing arguments one at a time#✓fully proved

Let \(r\) be a relation on a type \(\beta\), let \(n\) be a natural number and let \(P\) be a property of \(n\)-tuples \(x = (x_i)_{i < n}\) in \(\beta\). Suppose that for every tuple \(x\), every position \(i\) and all \(a, b \in \beta\) with \(r(a, b)\), if \(P\) holds of \(x\) with its \(i\)-th entry replaced by \(a\), then \(P\) holds of \(x\) with its \(i\)-th entry replaced by \(b\). Then for all tuples \(x, y\) with \(r(x_i, y_i)\) for every \(i\), \(P(x)\) implies \(P(y)\).

theorem update_chain {β : Type*} {n : ℕ} {r : β → β → Prop} (P : (Fin n → β) → Prop)
    (hstep : ∀ (x : Fin n → β) (i : Fin n) (a b : β), r a b →
      P (Function.update x i a) → P (Function.update x i b))
    {x y : Fin n → β} (hxy : ∀ i, r (x i) (y i)) (hx : P x) : P y

Used by 2

Used byModel existence for first-order logic · Truth lemma for the first-order term model

TheoremCongruence for function symbols in a maximal consistent set#✓fully proved

Let \(\Delta\) be a maximal consistent set of first-order formulas with free variables in \(\mathbb{N}\), let \(f\) be an \(n\)-ary function symbol, let \(x = (x_0, \dots, x_{n-1})\) be terms over \(\mathbb{N}\) and let \(i < n\). For a term \(u\), write \(x[i := u]\) for \(x\) with its \(i\)-th entry replaced by \(u\). If the equation \(a = b\) lies in \(\Delta\), then the equation \(f(x[i := a]) = f(x[i := b])\) lies in \(\Delta\).

theorem MaximalConsistent.func_update {n : ℕ} (f : L.Functions n) (x : Fin n → L.Term ℕ)
    (i : Fin n) {a b : L.Term ℕ} (hab : a.equal b ∈ Δ) :
    (Term.func f (Function.update x i a)).equal (Term.func f (Function.update x i b)) ∈ Δ

Uses 7 · Used by 2

Statement usesMaximal consistent set

Proof usesNatural deduction · Substitution of equals in maximal consistent sets · Maximal consistent sets of first-order formulas are deductively closed · Provability from a set of formulas · Instantiating 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

TheoremReplacing an argument of a relation symbol by an equal term#✓fully proved

Let \(\Delta\) be a maximal consistent set of formulas with free variables in \(\mathbb{N}\), let \(R\) be an \(n\)-ary relation symbol, let \(x_0, \dots, x_{n-1}\), \(a\) and \(b\) be terms with variables in \(\mathbb{N}\), and let \(i < n\). If \(\Delta\) contains \(a = b\) and contains \(R(x_0, \dots, x_{n-1})\) with \(x_i\) replaced by \(a\), then \(\Delta\) contains \(R(x_0, \dots, x_{n-1})\) with \(x_i\) replaced by \(b\).

theorem MaximalConsistent.rel_update {n : ℕ} (R : L.Relations n) (x : Fin n → L.Term ℕ)
    (i : Fin n) {a b : L.Term ℕ} (hab : a.equal b ∈ Δ)
    (h : R.formula (Function.update x i a) ∈ Δ) : R.formula (Function.update x i b) ∈ Δ

Uses 4 · Used by 2

Statement usesMaximal consistent set

Proof usesSubstitution of equals in maximal consistent sets · Instantiating 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

DefinitionTerm structure of a set of formulas#✓fully proved

Let \(\Delta\) be a set of first-order formulas in a language \(L\) with free variables in \(\mathbb{N}\). The term structure of \(\Delta\) is the \(L\)-structure whose domain is the set of \(L\)-terms with variables in \(\mathbb{N}\), in which an \(n\)-ary function symbol \(f\) sends terms \(t_1, \dots, t_n\) to the term \(f(t_1, \dots, t_n)\), and an \(n\)-ary relation symbol \(R\) holds of \(t_1, \dots, t_n\) exactly when the atomic formula \(R(t_1, \dots, t_n)\) belongs to \(\Delta\).

@[instance_reducible]
def termStructure (Δ : Set (L.Formula ℕ)) : L.Structure (L.Term ℕ) where
  funMap f ts := Term.func f ts
  RelMap R ts := R.formula ts ∈ Δ

Used by 2

Used byModel existence for first-order logic · Truth lemma for the first-order term model

DefinitionProvable equality of terms#✓fully proved

Let \(\Delta\) be a maximal consistent set of first-order formulas in a language \(L\) with free variables in \(\mathbb{N}\). Provable equality in \(\Delta\) is the equivalence relation on \(L\)-terms with variables in \(\mathbb{N}\) under which \(s \sim t\) holds exactly when the equation \(s = t\) belongs to \(\Delta\).

def termSetoid (hΔ : MaximalConsistent Δ) : Setoid (L.Term ℕ) where
  r s t := s.equal t ∈ Δ
  iseqv := ⟨hΔ.equal_refl, hΔ.equal_symm, hΔ.equal_trans⟩

Uses 6 · Used by 4

Statement usesNatural deduction · Symmetry of equality in natural deduction · Transitivity of equality in natural deduction · Maximal consistent set · Maximal consistent sets of first-order formulas are deductively closed · Provability from a set of formulas

Used byModel existence for first-order logic · Truth lemma for the first-order term model · Canonical assignment of the term model · Term model of a maximal consistent set

AbbreviationTerm model of a maximal consistent set#✓fully proved

For a maximal consistent set \(\Delta\) of formulas with free variables in \(\mathbb{N}\), the term model of \(\Delta\) is the set of terms with variables in \(\mathbb{N}\) modulo the equivalence relation that identifies \(s\) and \(t\) when the formula \(s = t\) belongs to \(\Delta\).

abbrev TermModel (hΔ : MaximalConsistent Δ) : Type u := Quotient (termSetoid hΔ)

Uses 2 · Used by 3

Statement usesMaximal consistent set · Provable equality of terms

Used byModel existence for first-order logic · Truth lemma for the first-order term model · Canonical assignment of the term model

DefinitionCanonical assignment of the term model#✓fully proved

For a maximal consistent set \(\Delta\) of formulas with free variables in \(\mathbb{N}\), the canonical assignment sends each variable \(x \in \mathbb{N}\) to \([x]\), the class of the variable term \(x\) in the term model of \(\Delta\).

def termAssignment (hΔ : MaximalConsistent Δ) : ℕ → TermModel hΔ :=
  fun x ↦ ⟦Term.var x⟧

Uses 3 · Used by 2

Statement usesMaximal consistent set · Term model of a maximal consistent set · Provable equality of terms

Used byModel existence for first-order logic · Truth lemma for the first-order term model

DefinitionLowering a term with no bound variables#✓fully proved

A term whose variables are free variables from \(\mathbb{N}\) together with bound variables from the empty index set is lowered to the term over \(\mathbb{N}\) of the same shape, in which every free variable \(x\) stays \(x\).

def lowerTerm (s : L.Term (ℕ ⊕ Fin 0)) : L.Term ℕ := s.subst (Sum.elim Term.var finZeroElim)

Used by 1

Used byTruth lemma for the first-order term model

TheoremTruth lemma for the first-order term model#✓fully proved

Let \(\Delta\) be a maximal consistent set of formulas with free variables in \(\mathbb{N}\) such that, for every formula \(\varphi\) with one bound variable, if \(\Delta\) contains \(\varphi(t)\) for every term \(t\) (where \(\varphi(t)\) is the result of substituting \(t\) for the bound variable), then \(\Delta\) contains \(\forall x\,\varphi\). Then a formula \(\psi\) with free variables in \(\mathbb{N}\) holds in the term model of \(\Delta\) under the canonical assignment \(x \mapsto [x]\) if and only if \(\psi \in \Delta\).

theorem realize_termModel_iff
    (hH : ∀ φ : L.BoundedFormula ℕ 1, (∀ t, instantiate t φ ∈ Δ) → φ.all ∈ Δ)
    (φ : L.Formula ℕ) : φ.Realize (termAssignment hΔ) ↔ φ ∈ Δ

Uses 23 · Used by 1

Statement usesNatural deduction · Symmetry of equality in natural deduction · Transitivity of equality in natural deduction · Maximal consistent set · Congruence for function symbols in a maximal consistent set · Maximal consistent sets of first-order formulas are deductively closed · Replacing an argument of a relation symbol by an equal term · Provability from a set of formulas · Term model of a maximal consistent set · Instantiating the outermost bound variable of a formula · Canonical assignment of the term model · Provable equality of terms · Term structure of a set of formulas · Replacing arguments one at a time

Proof usesConsistent set of formulas · Universal instantiation in maximal consistent sets · Maximal consistent sets decide every formula · Modus ponens for provability from sets · Depth of a formula · Instantiating the outermost bound variable of a term · Lowering a term with no bound variables · Truth of a universal formula · Truth of an instance

Used byModel existence for first-order logic

DefinitionEnumeration of formulas with one bound variable#✓fully proved

For a language with countably many symbols, the formulas \(\varphi_0, \varphi_1, \dots\) are a fixed enumeration, chosen by choice, of all first-order formulas with free variables in \(\mathbb{N}\) and one bound variable: every such formula is \(\varphi_k\) for some \(k \in \mathbb{N}\).

noncomputable def enumBody : ℕ → L.BoundedFormula ℕ 1 :=
  (exists_surjective_nat (L.BoundedFormula ℕ 1)).choose

Used by 3

Used byHenkin extension of a consistent set · The \(k\)-th Henkin axiom · Witness bases

DefinitionVariable bound of a formula#✓fully proved

Let \(\varphi\) be a first-order formula whose variables are natural numbers together with \(n\) variables reserved for quantifiers. Its variable bound \(b(\varphi)\) is one more than the largest natural number occurring as a free variable of \(\varphi\), or \(1\) when there is none; it is a strict upper bound on these free variables.

def varBound {n : ℕ} (φ : L.BoundedFormula ℕ n) : ℕ := φ.freeVarFinset.sup id + 1

Used by 2

Used byHenkin extension of a consistent set · Witness bases

DefinitionWitness bases#✓fully proved

Let \(L\) be a first-order language with countably many symbols, let \(\varphi_0, \varphi_1, \dots\) be the fixed surjective enumeration of the \(L\)-formulas with free variables in \(\mathbb{N}\) and one variable reserved for a quantifier, and let \(b(\varphi)\) be one more than the largest free variable of \(\varphi\), or \(1\) if it has none. The witness bases are defined by \(w_0 = b(\varphi_0)\) and \(w_{k+1} = w_k + 1 + b(\varphi_{k+1})\). They are strictly increasing, and \(w_k\) exceeds every free variable of \(\varphi_0, \dots, \varphi_k\).

noncomputable def witnessBase (L : Language.{u, v}) [Countable L.Symbols] : ℕ → ℕ
  | 0 => varBound (enumBody (L := L) 0)
  | k + 1 => witnessBase L k + 1 + varBound (enumBody (L := L) (k + 1))

Uses 2 · Used by 2

Statement usesEnumeration of formulas with one bound variable · Variable bound of a formula

Used byHenkin extension of a consistent set · Henkin witnesses

DefinitionHenkin witnesses#✓fully proved

Let \(L\) be a first-order language with countably many symbols and let \(w_0 < w_1 < \dots\) be its witness bases, built from the fixed enumeration \(\varphi_0, \varphi_1, \dots\) of the \(L\)-formulas with one variable reserved for a quantifier. The \(k\)-th Henkin witness is the variable \(c_k = 2 w_k + 1\). It is odd, so it is not a free variable of any formula whose free variables are all even, and it exceeds every free variable of \(\varphi_0, \dots, \varphi_k\).

noncomputable def witness (L : Language.{u, v}) [Countable L.Symbols] (k : ℕ) : ℕ :=
  2 * witnessBase L k + 1

Uses 1 · Used by 2

Statement usesWitness bases

Used byHenkin extension of a consistent set · The \(k\)-th Henkin axiom

DefinitionThe \(k\)-th Henkin axiom#✓fully proved

For a language with countably many symbols and \(k \in \mathbb{N}\), the \(k\)-th Henkin axiom is the Henkin axiom \(\neg \forall \varphi_k \to \neg \varphi_k(c_k)\), where \(\varphi_k\) is the \(k\)-th formula in the enumeration of formulas with one bound variable and \(c_k\) is the \(k\)-th Henkin witness.

noncomputable def henkinAxiomAt (k : ℕ) : L.Formula ℕ :=
  henkinAxiom (enumBody k) (witness L k)

Uses 3 · Used by 3

Statement usesEnumeration of formulas with one bound variable · Henkin axiom · Henkin witnesses

Used byHenkin extension of a consistent set · Henkin extension · Stages of the Henkin extension

DefinitionStages of the Henkin extension#✓fully proved

Let \(S\) be a set of first-order formulas with free variables in \(\mathbb{N}\), in a language with countably many symbols, and let \(H_k\) be the \(k\)-th Henkin axiom. The stages \(S_k\) are defined by \(S_0 = S\) and \(S_{k+1} = S_k \cup \{H_k\}\), so \(S_k\) is \(S\) together with \(H_0, \dots, H_{k-1}\).

noncomputable def henkinStage (S : Set (L.Formula ℕ)) : ℕ → Set (L.Formula ℕ)
  | 0 => S
  | k + 1 => insert (henkinAxiomAt k) (henkinStage S k)

Uses 1 · Used by 1

Statement usesThe \(k\)-th Henkin axiom

Used byHenkin extension of a consistent set

DefinitionHenkin extension#✓fully proved

For a language with countably many symbols, the Henkin extension of a set \(S\) of first-order formulas with free variables in \(\mathbb{N}\) is \(S\) together with all Henkin axioms, the \(k\)-th Henkin axiom for every \(k \in \mathbb{N}\).

noncomputable def henkinSet (S : Set (L.Formula ℕ)) : Set (L.Formula ℕ) :=
  S ∪ Set.range (henkinAxiomAt (L := L))

Uses 1 · Used by 1

Statement usesThe \(k\)-th Henkin axiom

Used byHenkin extension of a consistent set

TheoremHenkin extension of a consistent set#✓fully proved

Let \(L\) be a language with countably many symbols and let \(S\) be a consistent set of first-order formulas with free variables in \(\mathbb{N}\) such that every free variable of every formula in \(S\) is even. Then \(S\) is contained in a maximal consistent set \(\Delta\) with the Henkin property: for every formula \(\varphi\) with one bound variable, if every instance \(\varphi(t)\), for \(t\) a term over \(\mathbb{N}\), lies in \(\Delta\), then \(\forall \varphi\) lies in \(\Delta\).

theorem exists_maximalConsistent_henkin {S : Set (L.Formula ℕ)} (hS : Consistent S)
    (hEven : ∀ ψ ∈ S, ∀ x ∈ ψ.freeVarFinset, x % 2 = 0) :
    ∃ Δ, S ⊆ Δ ∧ MaximalConsistent Δ ∧
      ∀ φ : L.BoundedFormula ℕ 1, (∀ t, instantiate t φ ∈ Δ) → φ.all ∈ Δ

Uses 18 · Used by 1

Statement usesConsistent set of formulas · Maximal consistent set · Instantiating the outermost bound variable of a formula

Proof usesAdding a Henkin axiom preserves consistency · Natural deduction · Universal formulas from Henkin witnesses · Provability from a set of formulas · Unions of chains of consistent sets are consistent · Enumeration of formulas with one bound variable · Lindenbaum's lemma for first-order logic · Free variables of an instance · Henkin axiom · The \(k\)-th Henkin axiom · Henkin extension · Stages of the Henkin extension · Variable bound of a formula · Henkin witnesses · Witness bases

Used byModel existence for first-order logic

TheoremModel existence for first-order logic#✓fully proved

Let \(L\) be a language with countably many symbols. Every consistent set \(S\) of first-order formulas with free variables in \(\mathbb{N}\) is satisfiable: there are a nonempty \(L\)-structure \(M\), in the universe of the function symbols of \(L\), and an assignment \(v : \mathbb{N} \to M\) under which every formula of \(S\) holds.

The free variables are first doubled, which keeps the set consistent and leaves the odd variables free for Henkin witnesses.

theorem exists_model_of_consistent {S : Set (L.Formula ℕ)} (hS : Consistent S) :
    ∃ (M : Type u) (_ : L.Structure M) (v : ℕ → M), Nonempty M ∧ ∀ ψ ∈ S, ψ.Realize v

Uses 21 · Used by 2

Statement usesConsistent set of formulas

Proof usesDoubling the variables preserves consistency · Natural deduction · Symmetry of equality in natural deduction · Transitivity of equality in natural deduction · Maximal consistent set · Congruence for function symbols in a maximal consistent set · Maximal consistent sets of first-order formulas are deductively closed · Replacing an argument of a relation symbol by an equal term · Provability from a set of formulas · Term model of a maximal consistent set · Henkin extension of a consistent set · Relabelling a formula is renaming · Free variables of a renamed formula · Instantiating the outermost bound variable of a formula · Truth lemma for the first-order term model · Renaming free variables of a formula · Canonical assignment of the term model · Provable equality of terms · Term structure of a set of formulas · Replacing arguments one at a time

Used byFinite satisfiability · Strong completeness of first-order natural deduction

TheoremStrong completeness of first-order natural deduction#✓fully proved

Let \(L\) be a language with countably many function and relation symbols, whose function symbols live in universe \(u\). Let \(S\) be a set of formulas of \(L\) and \(\varphi\) a formula of \(L\), all with free variables in \(\mathbb{N}\). If for every \(L\)-structure \(M\) with carrier in universe \(u\) and every assignment \(v : \mathbb{N} \to M\) under which all formulas of \(S\) hold, \(\varphi\) also holds under \(v\), then \(\varphi\) is provable from \(S\).

theorem provable_of_entails {S : Set (L.Formula ℕ)} {φ : L.Formula ℕ}
    (h : ∀ (M : Type u) [L.Structure M] (v : ℕ → M), (∀ ψ ∈ S, ψ.Realize v) → φ.Realize v) :
    Provable S φ

Uses 4 · Used by 1

Statement usesProvability from a set of formulas

Proof usesConsistent set of formulas · Model existence for first-order logic · Provability as inconsistency with the negation

Used byCompleteness of first-order natural deduction for theories

TheoremCompleteness of first-order natural deduction for theories#✓fully proved

Let \(L\) be a language with countably many function and relation symbols, whose function symbols live in universe \(u\) and relation symbols in universe \(v\). Let \(T\) be a theory of \(L\) and \(\varphi\) a formula of \(L\) with free variables in \(\mathbb{N}\). If \(\varphi\) holds under every assignment of the variables in every nonempty model of \(T\) whose carrier lies in universe \(\max(u, v)\), then \(\varphi\) is provable from the sentences of \(T\), viewed as formulas over \(\mathbb{N}\).

theorem provable_of_models {T : L.Theory} {φ : L.Formula ℕ} (h : T ⊨ᵇ φ) :
    Provable (Formula.relabel Empty.elim '' T) φ

Uses 2 · Used by 1

Statement usesProvability from a set of formulas

Proof usesStrong completeness of first-order natural deduction

Used bySoundness and completeness of first-order natural deduction

TheoremSoundness and completeness of first-order natural deduction#✓fully proved

Let \(L\) be a language with countably many function and relation symbols, whose function symbols live in universe \(u\) and relation symbols in universe \(v\). For every theory \(T\) of \(L\) and every formula \(\varphi\) of \(L\) with free variables in \(\mathbb{N}\), \(\varphi\) is provable from the sentences of \(T\), viewed as formulas over \(\mathbb{N}\), if and only if \(\varphi\) holds under every assignment of the variables in every nonempty model of \(T\) whose carrier lies in universe \(\max(u, v)\).

theorem provable_iff_models {T : L.Theory} {φ : L.Formula ℕ} :
    Provable (Formula.relabel Empty.elim '' T) φ ↔ T ⊨ᵇ φ

Uses 3

Statement usesProvability from a set of formulas

Proof usesSoundness for theories · Completeness of first-order natural deduction for theories

DefinitionFinite set of symbols of a term#✓fully proved

The finite set of symbols occurring in a term \(t\) of a first-order language \(L\), a finite subset of the function and relation symbols of \(L\), is defined by recursion on \(t\): it is empty when \(t\) is a variable, and when \(t = f(t_0, \dots, t_{l-1})\) for an \(l\)-ary function symbol \(f\) it consists of \(f\) together with the symbols occurring in each of \(t_0, \dots, t_{l-1}\).

noncomputable def termSymbolFinset : L.Term α → Finset L.Symbols
  | .var _ => ∅
  | .func f ts =>
      insert (Sum.inl ⟨_, f⟩) (Finset.univ.biUnion fun i => termSymbolFinset (ts i))

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1 (the finite set of symbols occurring in a finite derivation).

Used by 9

Used byBounded formulas lift to the finite-symbol sublanguage · Terms lift to the finite-symbol sublanguage · Finite set of symbols of a formula · The relation symbol of an atomic formula occurs in it · The head function symbol of a term occurs in it · Symbols of the left side of an equation · Symbols of the right side of an equation · Symbols of an argument of a function application · Symbols of an argument of a relational atomic formula

TheoremThe head function symbol of a term occurs in it#✓fully proved

Let \(L\) be a first-order language, \(f\) an \(l\)-ary function symbol of \(L\), and \(t_1, \dots, t_l\) \(L\)-terms with variables in \(\alpha\). Then \(f\) belongs to the finite set of symbols occurring in the term \(f(t_1, \dots, t_l)\).

theorem mem_termSymbolFinset_func {l : ℕ} {f : L.Functions l} {ts : Fin l → L.Term α} :
    (Sum.inl ⟨l, f⟩ : L.Symbols) ∈ termSymbolFinset (Term.func f ts)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 1 · Used by 1

Statement usesFinite set of symbols of a term

Used byTerms lift to the finite-symbol sublanguage

TheoremSymbols of an argument of a function application#✓fully proved

Let \(f\) be an \(l\)-ary function symbol of a first-order language \(L\) and let \(t_0, \dots, t_{l-1}\) be terms of \(L\) in variables from \(\alpha\). For every \(i < l\), every symbol occurring in \(t_i\) occurs in the term \(f(t_0, \dots, t_{l-1})\): the finite set of symbols of \(t_i\) is contained in that of \(f(t_0, \dots, t_{l-1})\).

theorem termSymbolFinset_func_subset {l : ℕ} {f : L.Functions l} {ts : Fin l → L.Term α}
    {i : Fin l} : termSymbolFinset (ts i) ⊆ termSymbolFinset (Term.func f ts)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 1 · Used by 1

Statement usesFinite set of symbols of a term

Used byTerms lift to the finite-symbol sublanguage

DefinitionFinite set of symbols of a formula#✓fully proved

The finite set of function and relation symbols occurring in a bounded formula of a first-order language \(L\), defined by recursion on the formula: \(\bot\) has no symbols; an equation \(t_1 = t_2\) has the function symbols of \(t_1\) and \(t_2\); an atomic formula \(R(t_1, \dots, t_l)\) has \(R\) together with the function symbols of \(t_1, \dots, t_l\); an implication \(\varphi \to \psi\) has the symbols of \(\varphi\) and of \(\psi\); and \(\forall \varphi\) has the symbols of \(\varphi\).

noncomputable def formulaSymbolFinset {n : ℕ} : L.BoundedFormula α n → Finset L.Symbols
  | .falsum => ∅
  | .equal t₁ t₂ => termSymbolFinset t₁ ∪ termSymbolFinset t₂
  | .rel R ts => insert (Sum.inr ⟨_, R⟩) (Finset.univ.biUnion fun i => termSymbolFinset (ts i))
  | .imp φ ψ => formulaSymbolFinset φ ∪ formulaSymbolFinset ψ
  | .all φ => formulaSymbolFinset φ

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 1 · Used by 10

Statement usesFinite set of symbols of a term

Used byBounded formulas lift to the finite-symbol sublanguage · Finite satisfiability · Symbols of the antecedent occur in an implication · Symbols of the consequent occur in an implication · The relation symbol of an atomic formula occurs in it · A symbol of a member of a set of formulas is a symbol of the set · Symbols of a finite set of formulas · Symbols of the left side of an equation · Symbols of the right side of an equation · Symbols of an argument of a relational atomic formula

TheoremSymbols of the left side of an equation#✓fully proved

Let \(L\) be a first-order language and let \(t_1\), \(t_2\) be terms of \(L\) in free variables from \(\alpha\) and \(n\) bound variables. Every symbol occurring in \(t_1\) occurs in the atomic formula \(t_1 = t_2\), viewed as a formula with \(n\) bound variables: the finite set of symbols of \(t_1\) is contained in that of \(t_1 = t_2\).

theorem termSymbolFinset_equal_subset_left {n : ℕ} {t₁ t₂ : L.Term (α ⊕ Fin n)} :
    termSymbolFinset t₁ ⊆ formulaSymbolFinset (.equal t₁ t₂ : L.BoundedFormula α n)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 2 · Used by 1

Statement usesFinite set of symbols of a formula · Finite set of symbols of a term

Used byBounded formulas lift to the finite-symbol sublanguage

TheoremSymbols of the right side of an equation#✓fully proved

Let \(L\) be a first-order language and let \(t_1\), \(t_2\) be terms of \(L\) in free variables from \(\alpha\) and \(n\) bound variables. Every symbol occurring in \(t_2\) occurs in the atomic formula \(t_1 = t_2\), viewed as a formula with \(n\) bound variables: the finite set of symbols of \(t_2\) is contained in that of \(t_1 = t_2\).

theorem termSymbolFinset_equal_subset_right {n : ℕ} {t₁ t₂ : L.Term (α ⊕ Fin n)} :
    termSymbolFinset t₂ ⊆ formulaSymbolFinset (.equal t₁ t₂ : L.BoundedFormula α n)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 2 · Used by 1

Statement usesFinite set of symbols of a formula · Finite set of symbols of a term

Used byBounded formulas lift to the finite-symbol sublanguage

TheoremThe relation symbol of an atomic formula occurs in it#✓fully proved

Let \(L\) be a first-order language, \(R\) an \(l\)-ary relation symbol of \(L\), and \(t_1, \dots, t_l\) \(L\)-terms with free variables in \(\alpha\) and \(n\) bound variables. Then \(R\) belongs to the finite set of symbols occurring in the atomic bounded formula \(R(t_1, \dots, t_l)\).

theorem mem_formulaSymbolFinset_rel {n l : ℕ} {R : L.Relations l}
    {ts : Fin l → L.Term (α ⊕ Fin n)} :
    (Sum.inr ⟨l, R⟩ : L.Symbols) ∈ formulaSymbolFinset (.rel R ts : L.BoundedFormula α n)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 2 · Used by 1

Statement usesFinite set of symbols of a formula

Proof usesFinite set of symbols of a term

Used byBounded formulas lift to the finite-symbol sublanguage

TheoremSymbols of an argument of a relational atomic formula#✓fully proved

Let \(R\) be an \(l\)-ary relation symbol of a first-order language \(L\) and let \(t_0, \dots, t_{l-1}\) be terms of \(L\) in free variables from \(\alpha\) and \(n\) bound variables. For every \(i < l\), every symbol occurring in \(t_i\) occurs in the atomic formula \(R(t_0, \dots, t_{l-1})\), viewed as a formula with \(n\) bound variables: the finite set of symbols of \(t_i\) is contained in that of \(R(t_0, \dots, t_{l-1})\).

theorem termSymbolFinset_rel_subset {n l : ℕ} {R : L.Relations l}
    {ts : Fin l → L.Term (α ⊕ Fin n)} {i : Fin l} :
    termSymbolFinset (ts i) ⊆ formulaSymbolFinset (.rel R ts : L.BoundedFormula α n)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 2 · Used by 1

Statement usesFinite set of symbols of a formula · Finite set of symbols of a term

Used byBounded formulas lift to the finite-symbol sublanguage

TheoremSymbols of the antecedent occur in an implication#✓fully proved

For bounded formulas \(\varphi\) and \(\psi\) of a first-order language \(L\) with free variables in \(\alpha\) and \(n\) bound variables, every symbol occurring in \(\varphi\) occurs in \(\varphi \to \psi\).

theorem formulaSymbolFinset_imp_subset_left {n : ℕ} {φ ψ : L.BoundedFormula α n} :
    formulaSymbolFinset φ ⊆ formulaSymbolFinset (φ.imp ψ)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 1 · Used by 1

Statement usesFinite set of symbols of a formula

Used byBounded formulas lift to the finite-symbol sublanguage

TheoremSymbols of the consequent occur in an implication#✓fully proved

For bounded formulas \(\varphi\) and \(\psi\) of a first-order language \(L\) with free variables in \(\alpha\) and \(n\) bound variables, every symbol occurring in \(\psi\) occurs in \(\varphi \to \psi\).

theorem formulaSymbolFinset_imp_subset_right {n : ℕ} {φ ψ : L.BoundedFormula α n} :
    formulaSymbolFinset ψ ⊆ formulaSymbolFinset (φ.imp ψ)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 1 · Used by 1

Statement usesFinite set of symbols of a formula

Used byBounded formulas lift to the finite-symbol sublanguage

DefinitionSymbols of a finite set of formulas#✓fully proved

For a finite set \(F\) of first-order formulas of a language \(L\) with free variables indexed by \(\mathbb{N}\), the symbols of \(F\) are the finite set of function and relation symbols of \(L\) that occur in some formula of \(F\), that is, the union over \(\psi \in F\) of the finite sets of symbols occurring in \(\psi\).

noncomputable def symbolsOf (F : Finset (L.Formula ℕ)) : Finset L.Symbols :=
  F.biUnion fun ψ => formulaSymbolFinset ψ

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 1 · Used by 11

Statement usesFinite set of symbols of a formula

Used byBounded formulas lift to the finite-symbol sublanguage · Finite satisfiability · Terms lift to the finite-symbol sublanguage · Symbols of a generated sublanguage occur in the generating formulas · A symbol of a member of a set of formulas is a symbol of the set · Sublanguage of a finite set of formulas · Inclusion of the sublanguage of a finite set of formulas · The inclusion of the sublanguage of a finite set of formulas is injective · Symbols of the sublanguage of a finite set of formulas as symbols of the language · The symbol map of the sublanguage of a finite set of formulas is injective · Symbols of the sublanguage as symbols occurring in a finite set of formulas

TheoremA symbol of a member of a set of formulas is a symbol of the set#✓fully proved

Let \(L\) be a first-order language, \(F\) a finite set of \(L\)-formulas with free variables in \(\mathbb{N}\), and \(\psi \in F\). Every symbol occurring in \(\psi\) belongs to the finite set of symbols occurring in some formula of \(F\).

theorem mem_symbolsOf {F : Finset (L.Formula ℕ)} {ψ : L.Formula ℕ} {s : L.Symbols}
    (hψ : ψ ∈ F) (hs : s ∈ formulaSymbolFinset ψ) : s ∈ symbolsOf F

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 2 · Used by 1

Statement usesFinite set of symbols of a formula · Symbols of a finite set of formulas

Used byFinite satisfiability

DefinitionSublanguage of a finite set of formulas#✓fully proved

For a finite set \(F\) of formulas of a first-order language \(L\) with free variables in \(\mathbb{N}\), the sublanguage of \(L\) on the symbols occurring in \(F\) has as its \(n\)-ary function symbols the \(n\)-ary function symbols of \(L\) that occur in some formula of \(F\), and as its \(n\)-ary relation symbols the \(n\)-ary relation symbols of \(L\) that occur in some formula of \(F\).

def subLanguage (F : Finset (L.Formula ℕ)) : Language.{u, v} where
  Functions n := {f : L.Functions n // (Sum.inl ⟨n, f⟩ : L.Symbols) ∈ symbolsOf F}
  Relations n := {r : L.Relations n // (Sum.inr ⟨n, r⟩ : L.Symbols) ∈ symbolsOf F}

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V (the sublanguage generated by a finite set of formulas).

Uses 1 · Used by 11

Statement usesSymbols of a finite set of formulas

Used byConsistency passes to the finite-symbol sublanguage · Bounded formulas lift to the finite-symbol sublanguage · Finite satisfiability · Terms lift to the finite-symbol sublanguage · Symbols of a generated sublanguage occur in the generating formulas · Inclusion of the sublanguage of a finite set of formulas · The inclusion of the sublanguage of a finite set of formulas is injective · Preimage of a finite set of formulas in its sublanguage · Symbols of the sublanguage of a finite set of formulas as symbols of the language · The symbol map of the sublanguage of a finite set of formulas is injective · Symbols of the sublanguage as symbols occurring in a finite set of formulas

DefinitionInclusion of the sublanguage of a finite set of formulas#✓fully proved

Let \(L\) be a first-order language. For a finite set \(F\) of formulas of \(L\) with free variables in \(\mathbb{N}\), this is the language homomorphism from the sublanguage of \(L\) on the symbols occurring in \(F\) into \(L\) that sends each function symbol and each relation symbol to itself.

def subLanguageIncl (F : Finset (L.Formula ℕ)) : subLanguage F →ᴸ L :=
  ⟨fun _ f => f.1, fun _ r => r.1⟩

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 2 · Used by 6

Statement usesSublanguage of a finite set of formulas · Symbols of a finite set of formulas

Used byConsistency passes to the finite-symbol sublanguage · Bounded formulas lift to the finite-symbol sublanguage · Finite satisfiability · Terms lift to the finite-symbol sublanguage · The inclusion of the sublanguage of a finite set of formulas is injective · Preimage of a finite set of formulas in its sublanguage

TheoremThe inclusion of the sublanguage of a finite set of formulas is injective#✓fully proved

Let \(L\) be a first-order language. For every finite set \(F\) of formulas of \(L\) with free variables in \(\mathbb{N}\), the inclusion into \(L\) of the sublanguage of \(L\) on the symbols occurring in \(F\) is injective on function symbols and on relation symbols.

theorem subLanguageIncl_injective (F : Finset (L.Formula ℕ)) :
    (subLanguageIncl F).Injective

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 3 · Used by 1

Statement usesSublanguage of a finite set of formulas · Inclusion of the sublanguage of a finite set of formulas

Proof usesSymbols of a finite set of formulas

Used byFinite satisfiability

TheoremTerms lift to the finite-symbol sublanguage#✓fully proved

Let \(F\) be a finite set of formulas of a first-order language \(L\) with free variables in \(\mathbb{N}\), and let \(L_F\) be the sublanguage of \(L\) on the symbols occurring in \(F\), with inclusion \(\iota : L_F \to L\). Every term \(t\) of \(L\) whose variables are drawn from \(\mathbb{N}\) and from \(n\) bound variables, each of whose symbols occurs in some formula of \(F\), is the image under \(\iota\) of a term of \(L_F\) with variables drawn from the same set.

theorem exists_term_preimage {F : Finset (L.Formula ℕ)} {n : ℕ}
    {t : L.Term (ℕ ⊕ Fin n)} (ht : termSymbolFinset t ⊆ symbolsOf F) :
    ∃ t₀ : (subLanguage F).Term (ℕ ⊕ Fin n), (subLanguageIncl F).onTerm t₀ = t

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 6 · Used by 1

Statement usesSublanguage of a finite set of formulas · Inclusion of the sublanguage of a finite set of formulas · Symbols of a finite set of formulas · Finite set of symbols of a term

Proof usesThe head function symbol of a term occurs in it · Symbols of an argument of a function application

Used byBounded formulas lift to the finite-symbol sublanguage

TheoremBounded formulas lift to the finite-symbol sublanguage#✓fully proved

Let \(F\) be a finite set of formulas of a first-order language \(L\) with free variables in \(\mathbb{N}\), and let \(L_F\) be the sublanguage of \(L\) on the symbols occurring in \(F\), with inclusion \(\iota : L_F \to L\). Every bounded formula \(\varphi\) of \(L\) with free variables in \(\mathbb{N}\) and \(n\) bound variables, each of whose symbols occurs in some formula of \(F\), is the image under \(\iota\) of a bounded formula of \(L_F\) with free variables in \(\mathbb{N}\) and \(n\) bound variables.

theorem exists_boundedFormula_preimage {F : Finset (L.Formula ℕ)} {n : ℕ}
    {φ : L.BoundedFormula ℕ n} (hφ : formulaSymbolFinset φ ⊆ symbolsOf F) :
    ∃ φ₀ : (subLanguage F).BoundedFormula ℕ n,
      (subLanguageIncl F).onBoundedFormula φ₀ = φ

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 12 · Used by 1

Statement usesFinite set of symbols of a formula · Sublanguage of a finite set of formulas · Inclusion of the sublanguage of a finite set of formulas · Symbols of a finite set of formulas

Proof usesTerms lift to the finite-symbol sublanguage · Symbols of the antecedent occur in an implication · Symbols of the consequent occur in an implication · The relation symbol of an atomic formula occurs in it · Finite set of symbols of a term · Symbols of the left side of an equation · Symbols of the right side of an equation · Symbols of an argument of a relational atomic formula

Used byFinite satisfiability

TheoremLanguage homomorphisms commute with renaming variables#✓fully proved

Let \(h \colon L \to L'\) be a homomorphism of first-order languages, and for an \(L\)-term \(u\) write \(h(u)\) for the \(L'\)-term obtained by replacing every function symbol by its image under \(h\). Let \(t\) be an \(L\)-term with variables in \(\alpha\) and \(g \colon \alpha \to \beta\) a map. Then \(h\) applied to the term obtained from \(t\) by renaming each variable \(a\) to \(g(a)\) equals the term obtained from \(h(t)\) by the same renaming.

theorem onTerm_relabel {L' : Language.{u, v}} (ϕ : L →ᴸ L') {β : Type w} {t : L.Term α}
    {g : α → β} : ϕ.onTerm (t.relabel g) = (ϕ.onTerm t).relabel g

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1 (derivations depend only on the shape of a formula, not on the names of its symbols).

Used by 2

Used byLanguage homomorphisms preserve equations · Language homomorphisms commute with instantiation in terms

TheoremLanguage homomorphisms commute with substitution in terms#✓fully proved

Let \(h \colon L \to L'\) be a homomorphism of first-order languages, and for an \(L\)-term \(u\) write \(h(u)\) for the \(L'\)-term obtained by replacing every function symbol by its image under \(h\). Let \(s\) be an \(L\)-term with variables in \(\beta\) and \(g\) a map assigning to each \(b \in \beta\) an \(L\)-term \(g(b)\) with variables in \(\gamma\). Then \(h\) applied to the term obtained from \(s\) by substituting \(g(b)\) for each variable \(b\) equals the term obtained from \(h(s)\) by substituting \(h(g(b))\) for each variable \(b\).

theorem onTerm_subst {L' : Language.{u, v}} (ϕ : L →ᴸ L') {β γ : Type w}
    {s : L.Term β} {g : β → L.Term γ} :
    ϕ.onTerm (s.subst g) = (ϕ.onTerm s).subst (fun b => ϕ.onTerm (g b))

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Used by 1

Used byLanguage homomorphisms commute with instantiation in terms

TheoremTerm substitution depends only on the values of the substitution#✓fully proved

Let \(L\) be a first-order language, let \(s\) be a term of \(L\) with variables in a type \(\beta\), and let \(g\) and \(g'\) assign to each variable in \(\beta\) a term of \(L\) with variables in a type \(\gamma\). If \(g(a) = g'(a)\) for every \(a \in \beta\), then substituting \(g\) into \(s\) gives the same term as substituting \(g'\) into \(s\).

theorem subst_congr {β γ : Type w} {s : L.Term β} {g g' : β → L.Term γ}
    (h : ∀ a, g a = g' a) : s.subst g = s.subst g'

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Used by 1

Used byLanguage homomorphisms commute with instantiation in terms

TheoremLanguage homomorphisms commute with instantiation in terms#✓fully proved

Let \(h \colon L \to L'\) be a homomorphism of first-order languages, and for an \(L\)-term \(u\) write \(h(u)\) for the \(L'\)-term obtained by replacing every function symbol by its image under \(h\). Let \(t\) be an \(L\)-term with free variables in \(\alpha\) and \(s\) an \(L\)-term with free variables in \(\alpha\) and \(m + 1\) bound variables. Then \(h\) applied to the instantiation of \(t\) for the outermost bound variable (the one with index \(0\)) of \(s\) equals the instantiation of \(h(t)\) for the outermost bound variable of \(h(s)\).

theorem onTerm_instantiateTerm {L' : Language.{u, v}} (ϕ : L →ᴸ L') {m : ℕ}
    {t : L.Term α} {s : L.Term (α ⊕ Fin (m + 1))} :
    ϕ.onTerm (instantiateTerm t s) = instantiateTerm (ϕ.onTerm t) (ϕ.onTerm s)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 4 · Used by 1

Statement usesInstantiating the outermost bound variable of a term

Proof usesLanguage homomorphisms commute with renaming variables · Language homomorphisms commute with substitution in terms · Term substitution depends only on the values of the substitution

Used byLanguage homomorphisms commute with instantiation in formulas

TheoremLanguage homomorphisms commute with instantiation in formulas#✓fully proved

Let \(h \colon L \to L'\) be a homomorphism of first-order languages. For an \(L\)-term or bounded \(L\)-formula \(x\), write \(h(x)\) for the term or bounded formula of \(L'\) obtained by replacing every symbol by its image under \(h\). Let \(t\) be an \(L\)-term with free variables in \(\alpha\) and \(\varphi\) a bounded \(L\)-formula with free variables in \(\alpha\) and \(m + 1\) bound variables. Then \(h\) applied to the instantiation of \(t\) for the outermost bound variable (the one with index \(0\)) of \(\varphi\) equals the instantiation of \(h(t)\) for the outermost bound variable of \(h(\varphi)\).

theorem onBoundedFormula_instantiate {L' : Language.{u, v}} (ϕ : L →ᴸ L') {t : L.Term α} :
    ∀ {m : ℕ} (φ : L.BoundedFormula α (m + 1)),
      ϕ.onBoundedFormula (instantiate t φ) = instantiate (ϕ.onTerm t) (ϕ.onBoundedFormula φ)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 4 · Used by 1

Statement usesInstantiating the outermost bound variable of a formula

Proof usesInstantiating the outermost bound variable of a term · Instantiation commutes with the universal quantifier · Language homomorphisms commute with instantiation in terms

Used byDerivations survive language homomorphisms

TheoremLanguage homomorphisms preserve the free variables of a term#✓fully proved

Let \(\phi : L \to L'\) be a homomorphism of first-order languages and let \(t\) be a term of \(L\) in free variables from \(\alpha\) and \(n\) bound variables. The finite set of free variables from \(\alpha\) occurring in the image \(\phi(t)\) of \(t\) under \(\phi\) equals the finite set of those occurring in \(t\).

theorem varFinsetLeft_onTerm {L' : Language.{u, v}} (ϕ : L →ᴸ L') {n : ℕ}
    {t : L.Term (α ⊕ Fin n)} : (ϕ.onTerm t).varFinsetLeft = t.varFinsetLeft

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Used by 1

Used byLanguage homomorphisms preserve free variables

TheoremLanguage homomorphisms preserve free variables#✓fully proved

Let \(h : L \to L'\) be a homomorphism of first-order languages, and let \(\varphi\) be a bounded formula of \(L\) with free variables in \(\alpha\) and \(n\) bound variables. The formula of \(L'\) obtained from \(\varphi\) by replacing each symbol by its image under \(h\) has the same free variables as \(\varphi\).

theorem freeVarFinset_onBoundedFormula {L' : Language.{u, v}} (ϕ : L →ᴸ L') {n : ℕ}
    {φ : L.BoundedFormula α n} :
    (ϕ.onBoundedFormula φ).freeVarFinset = φ.freeVarFinset

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 1 · Used by 1

Proof usesLanguage homomorphisms preserve the free variables of a term

Used byDerivations survive language homomorphisms

TheoremLanguage homomorphisms preserve equations#✓fully proved

Let \(h \colon L \to L'\) be a homomorphism of first-order languages. For an \(L\)-term or \(L\)-formula \(x\), write \(h(x)\) for the term or formula of \(L'\) obtained by replacing every symbol by its image under \(h\). If \(s\) and \(t\) are \(L\)-terms with free variables in \(\alpha\), then \(h\) applied to the formula \(s = t\) is the formula \(h(s) = h(t)\).

theorem onFormula_equal {L' : Language.{u, v}} (ϕ : L →ᴸ L') {s t : L.Term α} :
    ϕ.onFormula (s.equal t) = (ϕ.onTerm s).equal (ϕ.onTerm t)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 1 · Used by 1

Proof usesLanguage homomorphisms commute with renaming variables

Used byDerivations survive language homomorphisms

TheoremDerivations survive language homomorphisms#✓fully proved

Let \(h : L \to L'\) be a homomorphism of first-order languages, and write \(h(\varphi)\) for the formula of \(L'\) obtained from a formula \(\varphi\) of \(L\) by replacing each symbol by its image under \(h\). Let \(\Gamma\) be a finite list of formulas of \(L\) with free variables in \(\alpha\), and let \(\varphi\) be a formula of \(L\) with free variables in \(\alpha\). If \(\Gamma \vdash \varphi\) in natural deduction, then \(h(\Gamma) \vdash h(\varphi)\), where \(h(\Gamma)\) is the list of the images of the members of \(\Gamma\).

The calculus never inspects a symbol.

theorem Derivable.mapLHom {L' : Language.{u, v}} (ϕ : L →ᴸ L')
    {Γ : List (L.Formula α)} {φ : L.Formula α} (h : Derivable Γ φ) :
    Derivable (Γ.map ϕ.onFormula) (ϕ.onFormula φ)

Sources

• D. van Dalen, Logic and Structure, 5th ed., Springer 2013, §3.1.

Uses 5 · Used by 1

Statement usesNatural deduction

Proof usesLanguage homomorphisms preserve free variables · Instantiating the outermost bound variable of a formula · Language homomorphisms commute with instantiation in formulas · Language homomorphisms preserve equations

Used byConsistency passes to the finite-symbol sublanguage

DefinitionPreimage of a finite set of formulas in its sublanguage#✓fully proved

Let \(L\) be a first-order language. For a finite set \(F\) of formulas of \(L\) with free variables in \(\mathbb{N}\), this is the set of those formulas \(\psi_0\) of the sublanguage of \(L\) on the symbols occurring in \(F\), with free variables in \(\mathbb{N}\), whose image under the inclusion of that sublanguage into \(L\) belongs to \(F\).

def subLanguagePreimage (F : Finset (L.Formula ℕ)) : Set ((subLanguage F).Formula ℕ) :=
  {ψ₀ | (subLanguageIncl F).onFormula ψ₀ ∈ F}

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 2 · Used by 2

Statement usesSublanguage of a finite set of formulas · Inclusion of the sublanguage of a finite set of formulas

Used byConsistency passes to the finite-symbol sublanguage · Finite satisfiability

TheoremConsistency passes to the finite-symbol sublanguage#✓fully proved

Let \(F\) be a finite set of formulas of a first-order language \(L\) with free variables in \(\mathbb{N}\), and let \(L_F\) be the sublanguage of \(L\) on the symbols occurring in \(F\), with inclusion \(\iota : L_F \to L\). If \(F\) is consistent, then so is the preimage of \(F\) in \(L_F\): the set of formulas \(\psi_0\) of \(L_F\) with free variables in \(\mathbb{N}\) whose image \(\iota(\psi_0)\) under the inclusion belongs to \(F\).

A refutation of the preimage maps along the inclusion to a refutation of \(F\).

theorem consistent_subLanguagePreimage {F : Finset (L.Formula ℕ)}
    (hF : Consistent (F : Set (L.Formula ℕ))) : Consistent (subLanguagePreimage F)

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 7 · Used by 1

Statement usesConsistent set of formulas · Sublanguage of a finite set of formulas · Preimage of a finite set of formulas in its sublanguage

Proof usesNatural deduction · Derivations survive language homomorphisms · Provability from a set of formulas · Inclusion of the sublanguage of a finite set of formulas

Used byFinite satisfiability

DefinitionSymbols of the sublanguage of a finite set of formulas as symbols of the language#✓fully proved

Let \(L\) be a first-order language. For a finite set \(F\) of formulas of \(L\) with free variables in \(\mathbb{N}\), this map sends each function symbol (respectively relation symbol) of the sublanguage of \(L\) on the symbols occurring in \(F\) to the same function symbol (respectively relation symbol) of \(L\), with the same arity.

def subLanguageSymbolsTo (F : Finset (L.Formula ℕ)) : (subLanguage F).Symbols → L.Symbols
  | Sum.inl ⟨l, f⟩ => Sum.inl ⟨l, f.1⟩
  | Sum.inr ⟨l, r⟩ => Sum.inr ⟨l, r.1⟩

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 2 · Used by 4

Statement usesSublanguage of a finite set of formulas · Symbols of a finite set of formulas

Used byFinite satisfiability · Symbols of a generated sublanguage occur in the generating formulas · The symbol map of the sublanguage of a finite set of formulas is injective · Symbols of the sublanguage as symbols occurring in a finite set of formulas

TheoremSymbols of a generated sublanguage occur in the generating formulas#✓fully proved

Let \(L\) be a first-order language and \(F\) a finite set of \(L\)-formulas with free variables in \(\mathbb{N}\). The map from the symbols of the sublanguage of \(L\) on the symbols occurring in \(F\) to the symbols of \(L\) sends every symbol of that sublanguage to a symbol occurring in some formula of \(F\).

theorem mem_subLanguageSymbolsTo (F : Finset (L.Formula ℕ)) (s : (subLanguage F).Symbols) :
    subLanguageSymbolsTo F s ∈ symbolsOf F

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 3 · Used by 2

Statement usesSublanguage of a finite set of formulas · Symbols of the sublanguage of a finite set of formulas as symbols of the language · Symbols of a finite set of formulas

Used byFinite satisfiability · Symbols of the sublanguage as symbols occurring in a finite set of formulas

TheoremThe symbol map of the sublanguage of a finite set of formulas is injective#✓fully proved

Let \(L\) be a first-order language. For every finite set \(F\) of formulas of \(L\) with free variables in \(\mathbb{N}\), the map sending each symbol of the sublanguage of \(L\) on the symbols occurring in \(F\) to the same symbol of \(L\) is injective.

theorem subLanguageSymbolsTo_injective (F : Finset (L.Formula ℕ)) :
    Function.Injective (subLanguageSymbolsTo F)

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 3 · Used by 1

Statement usesSublanguage of a finite set of formulas · Symbols of the sublanguage of a finite set of formulas as symbols of the language

Proof usesSymbols of a finite set of formulas

Used byFinite satisfiability

DefinitionSymbols of the sublanguage as symbols occurring in a finite set of formulas#✓fully proved

Let \(L\) be a first-order language. For a finite set \(F\) of formulas of \(L\) with free variables in \(\mathbb{N}\), this map sends each symbol of the sublanguage of \(L\) on the symbols occurring in \(F\) to the same symbol of \(L\), regarded as an element of the finite set of symbols occurring in \(F\).

def symEmbed (F : Finset (L.Formula ℕ)) (s : (subLanguage F).Symbols) :
    {x // x ∈ symbolsOf F} :=
  ⟨subLanguageSymbolsTo F s, mem_subLanguageSymbolsTo F s⟩

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 4 · Used by 1

Statement usesSymbols of a generated sublanguage occur in the generating formulas · Sublanguage of a finite set of formulas · Symbols of the sublanguage of a finite set of formulas as symbols of the language · Symbols of a finite set of formulas

Used byFinite satisfiability

TheoremFinite satisfiability#✓fully proved

Let \(L\) be a first-order language, with no countability hypothesis on its symbols. Every finite consistent set \(F\) of formulas of \(L\) with free variables in \(\mathbb{N}\) is satisfiable: there are a nonempty \(L\)-structure \(M\), in the universe of the function symbols of \(L\), and an assignment \(v : \mathbb{N} \to M\) under which every formula of \(F\) holds.

The proof passes to the sublanguage on the finitely many symbols occurring in \(F\), applies the countable Henkin theorem there, and expands the resulting structure along the inclusion.

theorem exists_model_of_consistent_finset {F : Finset (L.Formula ℕ)}
    (hF : Consistent (F : Set (L.Formula ℕ))) :
    ∃ (M : Type u) (_ : L.Structure M) (v : ℕ → M), Nonempty M ∧ ∀ ψ ∈ F, ψ.Realize v

Sources

• H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 15 · Used by 1

Statement usesConsistent set of formulas

Proof usesConsistency passes to the finite-symbol sublanguage · Bounded formulas lift to the finite-symbol sublanguage · Model existence for first-order logic · Finite set of symbols of a formula · Symbols of a generated sublanguage occur in the generating formulas · A symbol of a member of a set of formulas is a symbol of the set · Sublanguage of a finite set of formulas · Inclusion of the sublanguage of a finite set of formulas · The inclusion of the sublanguage of a finite set of formulas is injective · Preimage of a finite set of formulas in its sublanguage · Symbols of the sublanguage of a finite set of formulas as symbols of the language · The symbol map of the sublanguage of a finite set of formulas is injective · Symbols of the sublanguage as symbols occurring in a finite set of formulas · Symbols of a finite set of formulas

Used byModel existence for arbitrary languages

TheoremModel existence for arbitrary languages#✓fully proved

Let \(L\) be a first-order language, with no countability hypothesis on its symbols. Every consistent set \(S\) of formulas of \(L\) with free variables in \(\mathbb{N}\) is satisfiable: there are a nonempty \(L\)-structure \(M\), in the larger of the universes of the function symbols and the relation symbols of \(L\), and an assignment \(v : \mathbb{N} \to M\) under which every formula of \(S\) holds.

theorem exists_model_of_consistent_general {S : Set (L.Formula ℕ)} (hS : Consistent S) :
    ∃ (M : Type (max u v)) (_ : L.Structure M) (v : ℕ → M),
      Nonempty M ∧ ∀ ψ ∈ S, ψ.Realize v

Sources

• L. Henkin, The completeness of the first-order functional calculus, J. Symbolic Logic 14, 1949, 159-166; H.-D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 2nd ed., Springer 1994, Chapter V.

Uses 4 · Used by 2

Statement usesConsistent set of formulas

Proof usesNatural deduction · Provability from a set of formulas · Finite satisfiability

Used byStrong completeness for arbitrary languages · Completeness for arbitrary languages

TheoremStrong completeness for arbitrary languages#✓fully proved

Let \(L\) be a first-order language whose function symbols live in universe \(u\) and relation symbols in universe \(v\), with no restriction on the number of symbols. Let \(S\) be a set of formulas of \(L\) and \(\varphi\) a formula of \(L\), all with free variables in \(\mathbb{N}\). If for every \(L\)-structure \(M\) with carrier in universe \(\max(u, v)\) and every assignment \(e : \mathbb{N} \to M\) under which all formulas of \(S\) hold, \(\varphi\) also holds under \(e\), then \(\varphi\) is provable from \(S\).

theorem provable_of_entails_general {S : Set (L.Formula ℕ)} {φ : L.Formula ℕ}
    (h : ∀ (M : Type (max u v)) [L.Structure M] (v : ℕ → M),
      (∀ ψ ∈ S, ψ.Realize v) → φ.Realize v) : Provable S φ

Sources

• L. Henkin, The completeness of the first-order functional calculus, J. Symbolic Logic 14, 1949, 159-166.

Uses 4

Statement usesProvability from a set of formulas

Proof usesConsistent set of formulas · Model existence for arbitrary languages · Provability as inconsistency with the negation

TheoremCompleteness for arbitrary languages#✓fully proved

Let \(L\) be a first-order language whose function symbols live in universe \(u\) and relation symbols in universe \(v\), with no restriction on the number of symbols. Let \(T\) be a theory of \(L\) and \(\varphi\) a formula of \(L\) with free variables in \(\mathbb{N}\). If \(\varphi\) holds under every assignment of the variables in every nonempty model of \(T\) whose carrier lies in universe \(\max(u, v)\), then \(\varphi\) is provable from the sentences of \(T\), viewed as formulas over \(\mathbb{N}\).

theorem provable_of_models_general {T : L.Theory} {φ : L.Formula ℕ} (h : T ⊨ᵇ φ) :
    Provable (Formula.relabel Empty.elim '' T) φ

Sources

• L. Henkin, The completeness of the first-order functional calculus, J. Symbolic Logic 14, 1949, 159-166.

Uses 4 · Used by 1

Statement usesProvability from a set of formulas

Proof usesConsistent set of formulas · Model existence for arbitrary languages · Provability as inconsistency with the negation

Used bySoundness and completeness for arbitrary languages

TheoremSoundness and completeness for arbitrary languages#✓fully proved

Let \(L\) be a first-order language, with no countability hypothesis, \(T\) a theory of \(L\) (a set of sentences), and \(\varphi\) an \(L\)-formula with free variables in \(\mathbb{N}\). Then \(\varphi\) is provable from the sentences of \(T\), each regarded as a formula with free variables in \(\mathbb{N}\), if and only if \(\varphi\) holds in every nonempty model of \(T\) under every assignment of elements of the model to the variables in \(\mathbb{N}\).

The models range over types in the universe \(\max(u, v)\), where \(u\) and \(v\) are the universe levels of the function and relation symbols of \(L\).

theorem provable_iff_models_general {T : L.Theory} {φ : L.Formula ℕ} :
    Provable (Formula.relabel Empty.elim '' T) φ ↔ T ⊨ᵇ φ

Sources

• L. Henkin, The completeness of the first-order functional calculus, J. Symbolic Logic 14, 1949, 159-166.

Uses 3

Statement usesProvability from a set of formulas

Proof usesSoundness for theories · Completeness for arbitrary languages

80 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.