Consistency Property from a Model

This file constructs a ConsistencyPropertyEq from a model M equipped with a naming function. The consistency property is: S is consistent iff every sentence in S is true in M.

The naming function ι : M → L.Term Empty assigns a closed term to each element, with the soundness condition that each term evaluates to the element it names.

Main Results

• NamingFunction: A function mapping elements to closed terms that evaluate to them.
• trueInModelConsistencyPropertyEq: The sets of sentences true in M form a ConsistencyPropertyEq, enabling the model existence theorem to produce a countable model satisfying the same sentences.

Application

This is used in the proof of the downward Löwenheim-Skolem theorem: given a model M of a sentence φ, we construct a consistency property where {φ} is consistent (true in M), then apply model existence to get a countable model of φ.

References

• [Mar16], §4.1

structure FirstOrder.Language.NamingFunction (L : Language) (M : Type w) [L.Structure M] : Type (max u w)

A naming function maps each element of M to a closed term that evaluates to it.

• name : M → L.Term Empty

  The function assigning a closed term to each element.

• sound (m : M) : Term.realize Empty.elim (self.name m) = m

  The soundness condition: each term evaluates to the element it names.

def FirstOrder.Language.trueInModel {L : Language} (M : Type w) [L.Structure M] : Set L.Sentenceω

The set of sentences true in M.

Equations

• FirstOrder.Language.trueInModel M = {σ : L.Sentenceω | σ.Realize M}

def FirstOrder.Language.trueInModelFamily {L : Language} (M : Type w) [L.Structure M] : Set (Set L.Sentenceω)

The family of sets of sentences where every element is true in M.

Equations

• FirstOrder.Language.trueInModelFamily M = {S : Set L.Sentenceω | S ⊆ FirstOrder.Language.trueInModel M}

def FirstOrder.Language.trueInModelConsistencyProperty {L : Language} (M : Type w) [L.Structure M] : L.ConsistencyProperty

The family of true-in-M sets forms a ConsistencyProperty.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FirstOrder.Language.trueInModelConsistencyPropertyEq {L : Language} (M : Type w) [L.Structure M] (ι : L.NamingFunction M) : L.ConsistencyPropertyEq

Given a model M with a naming function, the true-in-M family forms a ConsistencyPropertyEq.

All C7 axioms are proved using realize_relabel_sumInr_zero (for the relabel Sum.inr variants) and realize_openBounds (for the openBounds variants).

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.singleton_in_trueInModelSets {L : Language} {M : Type w} [L.Structure M] (ι : L.NamingFunction M) (φ : L.Sentenceω) (hM : φ.Realize M) : {φ} ∈ (trueInModelConsistencyPropertyEq M ι).sets

A model of a sentence φ in a language with a naming function gives a consistency property where {φ} is consistent.

theorem FirstOrder.Language.subset_trueInModel_in_sets {L : Language} {M : Type w} [L.Structure M] (ι : L.NamingFunction M) (S : Set L.Sentenceω) (hS : ∀ φ ∈ S, φ.Realize M) : S ∈ (trueInModelConsistencyPropertyEq M ι).sets

A set of sentences true in M is in the consistency property.