Documentation

TauCeti.ModelTheory.ModelExistence.AElementary

Elementarity relative to a fragment and the Tarski–Vaught criterion #

Let A be a fragment of L_{ω₁ω}. An embedding f : N ↪[L] M is A-elementary when every member ⟨n, φ⟩ of A holds of f ∘ a in M exactly when it holds of a in N, for every tuple a : Fin n → N. It is stated as an equivalence, since a fragment need not contain negations.

The fragment Tarski–Vaught criterion upgrades a witness condition to A-elementarity: if, for every universal member ∀ x, φ of A and every tuple from N, whenever φ has a counterexample in M at that tuple it has one in the image of N, then f is A-elementary. The witnesses are elements, so no substitution of terms enters the induction, which uses exactly the component closure of A. No formation closure of A, countability of the language or nonemptiness of the carriers is needed.

Main definitions #

Main results #

References #

source
def FirstOrder.Language.AElementary {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (A : L.Fragment) (f : L.Embedding N M) :
Prop

An embedding f : N ↪[L] M is A-elementary for a fragment A when every member of A holds of f ∘ a in M exactly when it holds of a in N, at every tuple a from N.

Instances For
    source
    theorem FirstOrder.Language.aElementary_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {A : L.Fragment} {f : L.Embedding N M} :
    AElementary A f ↔ ∀ {n : ℕ} (φ : L.BoundedFormulaω Empty n), ⟨n, φ⟩ ∈ A → ∀ (a : Fin n → N), BoundedFormulaInf.Realize φ Empty.elim (⇑f ∘ a) ↔ BoundedFormulaInf.Realize φ Empty.elim a

    Unfolding lemma for AElementary.

    source
    theorem FirstOrder.Language.AElementary.realize_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {A : L.Fragment} {f : L.Embedding N M} (h : AElementary A f) {n : ℕ} {φ : L.BoundedFormulaω Empty n} (hφ : ⟨n, φ⟩ ∈ A) (a : Fin n → N) :
    BoundedFormulaInf.Realize φ Empty.elim (⇑f ∘ a) ↔ BoundedFormulaInf.Realize φ Empty.elim a

    An A-elementary embedding preserves and reflects every member of A at every tuple.

    source
    theorem FirstOrder.Language.AElementary.refl {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) :
    AElementary A (Embedding.refl L M)

    The identity embedding is A-elementary.

    source
    theorem FirstOrder.Language.AElementary.comp {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] {A : L.Fragment} {f : L.Embedding N M} {g : L.Embedding P N} (hf : AElementary A f) (hg : AElementary A g) :
    AElementary A (f.comp g)

    A-elementary embeddings compose.

    source
    theorem FirstOrder.Language.AElementary.of_comp {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] {A : L.Fragment} {f : L.Embedding N M} {g : L.Embedding P N} (hf : AElementary A f) (hfg : AElementary A (f.comp g)) :
    AElementary A g

    Two out of three. If f and f ∘ g are A-elementary, so is g.

    source
    theorem FirstOrder.Language.AElementary.mono {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {A B : L.Fragment} {f : L.Embedding N M} (hAB : A ≤ B) (h : AElementary B f) :
    AElementary A f

    A-elementarity passes to smaller fragments.

    source
    theorem FirstOrder.Language.AElementary.realize_sentenceInf_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {A : L.Fragment} {f : L.Embedding N M} (h : AElementary A f) {φ : L.Sentenceω} (hφ : ⟨0, φ⟩ ∈ A) :
    SentenceInf.Realize φ M ↔ SentenceInf.Realize φ N

    Sentences of A hold in N exactly when they hold in M.

    source
    theorem FirstOrder.Language.AElementary.theoryω_model_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {A : L.Fragment} {f : L.Embedding N M} (h : AElementary A f) {T : L.Theoryω} (hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A) :
    T.Model M ↔ T.Model N

    Theories of A hold in N exactly when they hold in M.

    source
    theorem FirstOrder.Language.OmitsType.of_aElementary {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {A : L.Fragment} {f : L.Embedding N M} (hf : AElementary A f) {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} (hp : ∀ φ ∈ p, ⟨n, φ⟩ ∈ A) (h : OmitsType M p) :
    OmitsType N p

    Omission passes along A-elementary embeddings. If M omits a partial type whose members lie in A, so does every structure embedded in M by an A-elementary embedding.

    source
    theorem FirstOrder.Language.Equiv.aElementary {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (A : L.Fragment) (e : L.Equiv N M) :
    AElementary A e.toEmbedding

    An isomorphism is A-elementary for every fragment A.

    source
    theorem FirstOrder.Language.aElementary_of_tarskiVaught {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {A : L.Fragment} (f : L.Embedding N M) (htv : ∀ {n : ℕ} (φ : L.BoundedFormulaω Empty (n + 1)), ⟨n, BoundedFormulaInf.all φ⟩ ∈ A → ∀ (a : Fin n → N), (∃ (m : M), ¬BoundedFormulaInf.Realize φ Empty.elim (Fin.snoc (⇑f ∘ a) m)) → ∃ (b : N), ¬BoundedFormulaInf.Realize φ Empty.elim (Fin.snoc (⇑f ∘ a) (f b))) :
    AElementary A f

    The fragment Tarski–Vaught criterion. If, for every universal member ∀ x, φ of A and every tuple a from N, whenever φ has a counterexample at f ∘ a in M it has one in the image of f, then f is A-elementary.