Documentation

TauCeti.ModelTheory.ModelExistence.Isolation

Isolation of partial types over an L_{ω₁ω} theory #

A partial type p, a set of formulas with n bound positions and no free variables, is isolated over a theory T in a fragment A when some member φ of A with n bound positions is consistent with T and implies every formula of p modulo T: the theory T together with φ.exs is satisfiable, and T entails (φ.imp ψ).alls for every ψ ∈ p, where exs and alls quantify the n bound positions.

Non-isolation is the hypothesis of the omitting types theorem, by which a satisfiable theory in a countable formation-closed fragment has a countable model omitting countably many partial types none of which is isolated. An isolated type, on the other hand, is realized in some countable model of a countable theory, and in every structure whose L_{ω₁ω} theory the theory entails. Conversely, in a structure realizing only countably many complete n-types, each realized complete type is isolated over the theory of the structure.

Main definitions #

Main results #

References #

source
def FirstOrder.Language.Theoryω.IsolatesIn {L : Language} {n : ℕ} (A : L.Fragment) (T : L.Theoryω) (p : Set (L.BoundedFormulaω Empty n)) :
Prop

A partial type p in n bound positions is isolated over the theory T in the fragment A when some member φ of A with n bound positions is consistent with T, in that T together with φ.exs is satisfiable, and implies every formula of p modulo T: T entails (φ.imp ψ).alls for every ψ ∈ p. Here exs and alls quantify the n bound positions.

Instances For
    source
    theorem FirstOrder.Language.Theoryω.isolatesIn_iff {L : Language} {A : L.Fragment} {T : L.Theoryω} {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} :
    IsolatesIn A T p ↔ ∃ (φ : L.BoundedFormulaω Empty n), ⟨n, φ⟩ ∈ A ∧ (insert (BoundedFormulaInf.exs φ) T).IsSatisfiable ∧ ∀ ψ ∈ p, T.Entails (BoundedFormulaInf.imp φ ψ).alls

    Unfolding lemma for Theoryω.IsolatesIn.

    source
    theorem FirstOrder.Language.Theoryω.IsolatesIn.mono {L : Language} {A B : L.Fragment} {T : L.Theoryω} {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} (h : IsolatesIn A T p) (hAB : A ≤ B) :
    IsolatesIn B T p

    Isolation in a fragment is isolation in every larger fragment.

    source
    theorem FirstOrder.Language.Theoryω.IsolatesIn.subset {L : Language} {A : L.Fragment} {T : L.Theoryω} {n : ℕ} {p q : Set (L.BoundedFormulaω Empty n)} (h : IsolatesIn A T p) (hqp : q ⊆ p) :
    IsolatesIn A T q

    A formula isolating a partial type isolates each of its subsets.

    source
    theorem FirstOrder.Language.Theoryω.IsolatesIn.isSatisfiable {L : Language} {A : L.Fragment} {T : L.Theoryω} {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} (h : IsolatesIn A T p) :
    T.IsSatisfiable

    Only a satisfiable theory isolates a partial type.

    source
    theorem FirstOrder.Language.Theoryω.IsolatesIn.exists_model_not_omitsType {L : Language} {A : L.Fragment} {T : L.Theoryω} {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} (h : IsolatesIn A T p) :
    ∃ (M : Type (max u v)) (x : L.Structure M), Nonempty M ∧ T.Model M ∧ ¬OmitsType M p

    Isolated types are realized. A partial type isolated over T is realized in some nonempty model of T in the universe max u v.

    source
    theorem FirstOrder.Language.Theoryω.IsolatesIn.exists_countable_model_not_omitsType {L : Language} {A : L.Fragment} {T : L.Theoryω} {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} (hT : Set.Countable T) (h : IsolatesIn A T p) :
    ∃ (M : Type w) (x : L.Structure M), Countable M ∧ Nonempty M ∧ T.Model M ∧ ¬OmitsType M p

    Isolated types are realized in countable models. A partial type isolated over a countable theory T is realized in some countable nonempty model of T, in every universe w.

    source
    theorem FirstOrder.Language.Theoryω.IsolatesIn.not_omitsType {L : Language} {A : L.Fragment} {T : L.Theoryω} {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} {N : Type w} [L.Structure N] (h : IsolatesIn A T p) (hN : ∀ (σ : L.Sentenceω), SentenceInf.Realize σ N → T.Entails σ) :
    ¬OmitsType N p

    Isolated types are realized in structures whose theory T entails. If T entails every sentence true in N, for instance when T is the L_{ω₁ω} theory of N, then N realizes every partial type isolated over T. The structure N may be empty and of any cardinality, in any universe.

    source
    theorem FirstOrder.Language.Theoryω.isolatesIn_top_infinitaryType {L : Language} {n : ℕ} {M : Type w} [L.Structure M] [Nonempty M] [Small.{max u v, w} M] (h : (realizedTypes M n).Countable) (a : Fin n → M) :
    IsolatesIn ⊤ {σ : L.Sentenceω | SentenceInf.Realize σ M} (infinitaryType M a)

    Realized types are isolated over the theory of the structure. If a nonempty structure M, small in the universe max u v, realizes only countably many complete n-types, then the complete type of each n-tuple of M is isolated over the L_{ω₁ω} theory of M in the fragment of all formulas.

    source
    theorem FirstOrder.Language.Theoryω.isolatesIn_firstOrder_iff {L : Language} {n : ℕ} {T : L.Theory} {p : Set (L.BoundedFormula Empty n)} :
    IsolatesIn (Fragment.firstOrder L) (BoundedFormula.toOmega '' T) (BoundedFormula.toOmega '' p) ↔ ∃ (φ : L.BoundedFormula Empty n), (insert φ.exs T).IsSatisfiable ∧ ∀ ψ ∈ p, T ⊨ᵇ (φ.imp ψ).alls

    Isolation in the first-order image. A first-order partial type is isolated over a first-order theory in the first-order image fragment exactly when some first-order formula φ isolates it modulo the theory in Mathlib's sense: the theory together with the existential closure of φ is satisfiable, and the theory models the universal closure of φ → ψ for every ψ in the type.