Instances of infinitary formulas at constants

For an infinitary formula φ of L with n bound positions and a tuple c : Fin n → γ, the instance φ.instConstants c is the formula of the constant expansion L[[γ]] obtained by substituting the constant L.con (c i) for the bound position i. In an expansion of an L-structure it holds exactly when φ holds at the values of the constants (BoundedFormulaInf.realize_instConstants).

The instances of the members of a fragment A at tuples of constants form the set of sentences A.instances γ. Every component of an instance is again an instance: the components of an implication, of a countable conjunction or disjunction, and the instantiation of a universal sentence at a constant. When A is formation-closed, the negation of an instance is an instance, and every atomic sentence of L[[γ]] is an instance, since the finitely many constants of an atomic sentence can be abstracted into bound positions.

These are the sentences a consistency property built from satisfiable sets of sentences works with: a sentence is true at a tuple of constants exactly when the formula it instantiates holds at their values, so changing the interpretation of a constant outside the tuple does not change its truth value.

Main definitions

• FirstOrder.Language.BoundedFormulaInf.instConstants: the instance of a formula at a tuple of constants.
• FirstOrder.Language.Fragment.instances: the instances of the members of a fragment.

Main results

• FirstOrder.Language.BoundedFormulaInf.realize_instConstants: an instance holds exactly when the formula holds at the values of the constants.
• FirstOrder.Language.BoundedFormulaInf.realize_instConstants_constantsOn and FirstOrder.Language.BoundedFormulaInf.realize_instConstants_congr: in the expansion interpreting each constant c as e c, an instance at d holds exactly when the formula holds at e ∘ d, so it does not depend on the interpretation of the other constants.
• FirstOrder.Language.Theoryω.Model.of_eqOn_constantsOn: a model of a theory of instances at constants from a set F stays a model when the constants outside F are reinterpreted.
• FirstOrder.Language.BoundedFormulaInf.instConstants_eq_imp_iff and its companions: the instances of the components of a formula are the components of its instance.
• FirstOrder.Language.BoundedFormulaInf.IsAtomic.exists_instConstants_eq: every atomic formula of L[[γ]] without bound positions is the instance of an atomic formula of L.
• FirstOrder.Language.Fragment.FormationClosed.mem_instances_of_isAtomic: every atomic sentence of L[[γ]] is an instance of a member of a formation-closed fragment.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, §4.1.

def FirstOrder.Language.BoundedFormulaInf.instConstants {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (c : Fin n → γ) : (L.withConstants γ).FormulaInf ι α

The instance of φ at the tuple c of constants: the formula of L[[γ]] obtained by substituting the constant L.con (c i) for the bound position i of φ.

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_def {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (c : Fin n → γ) : φ.instConstants c = substBounds (fun (i : Fin n) => (L.con (c i)).term) ((L.lhomWithConstants γ).onBoundedFormulaInf φ)

Unfolding lemma for BoundedFormulaInf.instConstants.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_falsum {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) : falsum.instConstants c = falsum

The instance of ⊥ is ⊥.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_bot {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) : ⊥.instConstants c = ⊥

The instance of ⊥ is ⊥.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_imp {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (φ ψ : L.BoundedFormulaInf ι α n) : (φ.imp ψ).instConstants c = imp (φ.instConstants c) (ψ.instConstants c)

Instances commute with implication.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_not {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (φ : L.BoundedFormulaInf ι α n) : φ.not.instConstants c = BoundedFormulaInf.not (φ.instConstants c)

Instances commute with negation.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_iSup {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (φs : ι → L.BoundedFormulaInf ι α n) : (iSup φs).instConstants c = iSup fun (i : ι) => (φs i).instConstants c

Instances commute with disjunctions over the carrier.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_iInf {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (φs : ι → L.BoundedFormulaInf ι α n) : (iInf φs).instConstants c = iInf fun (i : ι) => (φs i).instConstants c

Instances commute with conjunctions over the carrier.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_equal {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (t₁ t₂ : L.Term (α ⊕ Fin n)) : (equal t₁ t₂).instConstants c = equal (((L.lhomWithConstants γ).onTerm t₁).subst (Sum.elim (var ∘ Sum.inl) fun (i : Fin n) => (L.con (c i)).term)) (((L.lhomWithConstants γ).onTerm t₂).subst (Sum.elim (var ∘ Sum.inl) fun (i : Fin n) => (L.con (c i)).term))

The instance of an equation substitutes the constants into the images of both sides.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_rel {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : (rel R ts).instConstants c = rel (Sum.inl R) fun (i : Fin l) => ((L.lhomWithConstants γ).onTerm (ts i)).subst (Sum.elim (var ∘ Sum.inl) fun (i : Fin n) => (L.con (c i)).term)

The instance of a relational atom substitutes the constants into the images of its terms.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_all {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (φ : L.BoundedFormulaInf ι α (n + 1)) : φ.all.instConstants c = (substBounds (liftSubst fun (i : Fin n) => (L.con (c i)).term) ((L.lhomWithConstants γ).onBoundedFormulaInf φ)).all

The instance of a universal formula is the universal formula of the body with the constants substituted for the outer bound positions.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_ex {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (φ : L.BoundedFormulaInf ι α (n + 1)) : φ.ex.instConstants c = (substBounds (liftSubst fun (i : Fin n) => (L.con (c i)).term) ((L.lhomWithConstants γ).onBoundedFormulaInf φ)).ex

The instance of an existential formula is the existential formula of the body with the constants substituted for the outer bound positions.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_top {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) : ⊤.instConstants c = ⊤

The instance of ⊤ is ⊤.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_inf {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (φ ψ : L.BoundedFormulaInf ι α n) : (φ ⊓ ψ).instConstants c = φ.instConstants c ⊓ ψ.instConstants c

Instances commute with conjunction.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_sup {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (φ ψ : L.BoundedFormulaInf ι α n) : (φ ⊔ ψ).instConstants c = φ.instConstants c ⊔ ψ.instConstants c

Instances commute with disjunction.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_iff {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} (c : Fin n → γ) (φ ψ : L.BoundedFormulaInf ι α n) : (φ.iff ψ).instConstants c = BoundedFormulaInf.iff (φ.instConstants c) (ψ.instConstants c)

Instances commute with the biconditional.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_zero {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} (φ : L.BoundedFormulaInf ι α 0) (c : Fin 0 → γ) : φ.instConstants c = (L.lhomWithConstants γ).onBoundedFormulaInf φ

An instance at the empty tuple is the image of the formula in L[[γ]].

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_instConstants {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {M : Type u_1} [L.Structure M] [(L.withConstants γ).Structure M] [(L.lhomWithConstants γ).IsExpansionOn M] {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (c : Fin n → γ) (v : α → M) : (φ.instConstants c).Realize v ↔ φ.Realize v fun (i : Fin n) => ↑(L.con (c i))

An instance holds at the values of its constants: in an expansion of an L-structure to L[[γ]], the instance of φ at c is realized exactly when φ is realized at the values of the constants L.con (c i).

theorem FirstOrder.Language.BoundedFormulaInf.realize_instConstants_constantsOn {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {M : Type u_1} [L.Structure M] (e : γ → M) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (d : Fin n → γ) (v : α → M) : (φ.instConstants d).Realize v ↔ φ.Realize v (e ∘ d)

In the expansion of an L-structure interpreting each constant c as e c, the instance of φ at d is realized exactly when φ is realized at e ∘ d.

theorem FirstOrder.Language.BoundedFormulaInf.realize_instConstants_congr {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {M : Type u_1} [L.Structure M] {e e' : γ → M} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) {d : Fin n → γ} (h : Set.EqOn e e' (Set.range d)) (v : α → M) : (φ.instConstants d).Realize v ↔ (φ.instConstants d).Realize v

An instance depends only on its constants: reinterpreting the constants outside the tuple d does not change whether the instance at d is realized.

Inversion

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_eq_falsum_iff {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} {c : Fin n → γ} : φ.instConstants c = falsum ↔ φ = falsum

An instance is ⊥ exactly when the formula is.

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_eq_imp_iff {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} {c : Fin n → γ} {ψ₁ ψ₂ : (L.withConstants γ).FormulaInf ι α} : φ.instConstants c = imp ψ₁ ψ₂ ↔ ∃ (φ₁ : L.BoundedFormulaInf ι α n) (φ₂ : L.BoundedFormulaInf ι α n), φ = φ₁.imp φ₂ ∧ φ₁.instConstants c = ψ₁ ∧ φ₂.instConstants c = ψ₂

An instance is an implication exactly when the formula is an implication whose sides have the two sides of the instance as their instances.

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_eq_iSup_iff {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} {c : Fin n → γ} {ψs : ι → (L.withConstants γ).FormulaInf ι α} : φ.instConstants c = iSup ψs ↔ ∃ (φs : ι → L.BoundedFormulaInf ι α n), φ = iSup φs ∧ ∀ (i : ι), (φs i).instConstants c = ψs i

An instance is a disjunction over the carrier exactly when the formula is a disjunction over the carrier whose disjuncts have the disjuncts of the instance as their instances.

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_eq_iInf_iff {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} {c : Fin n → γ} {ψs : ι → (L.withConstants γ).FormulaInf ι α} : φ.instConstants c = iInf ψs ↔ ∃ (φs : ι → L.BoundedFormulaInf ι α n), φ = iInf φs ∧ ∀ (i : ι), (φs i).instConstants c = ψs i

An instance is a conjunction over the carrier exactly when the formula is a conjunction over the carrier whose conjuncts have the conjuncts of the instance as their instances.

theorem FirstOrder.Language.BoundedFormulaInf.instConstants_eq_all_iff {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} {c : Fin n → γ} {ψ : (L.withConstants γ).BoundedFormulaInf ι α 1} : φ.instConstants c = ψ.all ↔ ∃ (φ' : L.BoundedFormulaInf ι α (n + 1)), φ = φ'.all ∧ substBounds (liftSubst fun (i : Fin n) => (L.con (c i)).term) ((L.lhomWithConstants γ).onBoundedFormulaInf φ') = ψ

An instance is a universal formula ∀ ψ exactly when the formula is a universal formula ∀ φ' and ψ is the body φ' with the constants substituted for the outer bound positions.

theorem FirstOrder.Language.BoundedFormulaInf.exists_eq_all_of_instConstants_eq_all {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} {c : Fin n → γ} {ψ : (L.withConstants γ).BoundedFormulaInf ι α 1} (h : φ.instConstants c = ψ.all) : ∃ (φ' : L.BoundedFormulaInf ι α (n + 1)), φ = φ'.all ∧ ∀ (d : γ), ψ.inst (L.con d).term = φ'.instConstants (Fin.snoc c d)

If an instance is a universal formula ∀ ψ, the formula is a universal formula ∀ φ', and instantiating ψ at a constant d gives the instance of φ' at the extended tuple.

Atomic formulas over the constant expansion

theorem FirstOrder.Language.BoundedFormulaInf.IsAtomic.exists_instConstants_eq {L : Language} {ι : Type uι} {α : Type uα} {γ : Type w} {φ : (L.withConstants γ).FormulaInf ι α} (h : IsAtomic φ) : ∃ (n : ℕ) (ψ : L.BoundedFormulaInf ι α n) (c : Fin n → γ), ψ.IsAtomic ∧ ψ.instConstants c = φ

Atomic formulas abstract their constants: an atomic formula of L[[γ]] without bound positions is the instance of an atomic formula of L at a tuple of constants.

theorem FirstOrder.Language.Theoryω.model_of_forall_realize_instConstants {L : Language} {γ : Type w} {M : Type u_1} [L.Structure M] {s : (L.withConstants γ).Theoryω} (e : γ → M) (h : ∀ φ ∈ s, ∃ (n : ℕ) (χ : L.BoundedFormulaω Empty n) (d : Fin n → γ), BoundedFormulaInf.instConstants χ d = φ ∧ BoundedFormulaInf.Realize χ Empty.elim (e ∘ d)) : s.Model M

The expansion of an L-structure interpreting each constant c as e c models a theory whose sentences are instances of formulas holding at the values of their constants.

theorem FirstOrder.Language.Theoryω.Model.realize_of_instConstants_mem {L : Language} {γ : Type w} {M : Type u_1} [L.Structure M] {s : (L.withConstants γ).Theoryω} {e : γ → M} (hM : s.Model M) {n : ℕ} {χ : L.BoundedFormulaω Empty n} {d : Fin n → γ} (h : BoundedFormulaInf.instConstants χ d ∈ s) : BoundedFormulaInf.Realize χ Empty.elim (e ∘ d)

In a model of s that is the expansion of an L-structure interpreting each constant c as e c, an instance in s holds at the values of its constants.

theorem FirstOrder.Language.Theoryω.Model.of_eqOn_constantsOn {L : Language} {γ : Type w} {M : Type u_1} [L.Structure M] {s : (L.withConstants γ).Theoryω} {e e' : γ → M} {F : Set γ} (hF : ∀ φ ∈ s, ∃ (n : ℕ) (χ : L.BoundedFormulaω Empty n) (d : Fin n → γ), BoundedFormulaInf.instConstants χ d = φ ∧ ∀ (i : Fin n), d i ∈ F) (he : Set.EqOn e e' F) (hM : s.Model M) : s.Model M

Reinterpreting the constants outside a set F preserves a model of a theory whose sentences are instances at tuples of constants from F.

def FirstOrder.Language.Fragment.instances {L : Language} (A : L.Fragment) (γ : Type w) : Set (L.withConstants γ).Sentenceω

The instances of a fragment A at constants indexed by γ: the sentences of L[[γ]] that are the instance of a member of A at a tuple of constants.

theorem FirstOrder.Language.Fragment.mem_instances {L : Language} {A : L.Fragment} {γ : Type w} {φ : (L.withConstants γ).Sentenceω} : φ ∈ A.instances γ ↔ ∃ (n : ℕ) (ψ : L.BoundedFormulaω Empty n) (c : Fin n → γ), ⟨n, ψ⟩ ∈ A ∧ BoundedFormulaInf.instConstants ψ c = φ

Membership in the instances of a fragment.

theorem FirstOrder.Language.Fragment.instConstants_mem_instances {L : Language} {A : L.Fragment} {γ : Type w} {n : ℕ} {ψ : L.BoundedFormulaω Empty n} (h : ⟨n, ψ⟩ ∈ A) (c : Fin n → γ) : BoundedFormulaInf.instConstants ψ c ∈ A.instances γ

The instance of a member at a tuple of constants is an instance.

theorem FirstOrder.Language.Fragment.onBoundedFormulaInf_mem_instances {L : Language} {A : L.Fragment} {γ : Type w} {φ : L.Sentenceω} (h : ⟨0, φ⟩ ∈ A) : (L.lhomWithConstants γ).onBoundedFormulaInf φ ∈ A.instances γ

The image in L[[γ]] of a member sentence is an instance.

theorem FirstOrder.Language.Fragment.imp_left_mem_instances {L : Language} {A : L.Fragment} {γ : Type w} {φ ψ : (L.withConstants γ).Sentenceω} (h : BoundedFormulaInf.imp φ ψ ∈ A.instances γ) : φ ∈ A.instances γ

The antecedent of an instance implication is an instance.

theorem FirstOrder.Language.Fragment.imp_right_mem_instances {L : Language} {A : L.Fragment} {γ : Type w} {φ ψ : (L.withConstants γ).Sentenceω} (h : BoundedFormulaInf.imp φ ψ ∈ A.instances γ) : ψ ∈ A.instances γ

The consequent of an instance implication is an instance.

theorem FirstOrder.Language.Fragment.iInf_mem_instances {L : Language} {A : L.Fragment} {γ : Type w} {φs : ℕ → (L.withConstants γ).Sentenceω} (h : BoundedFormulaInf.iInf φs ∈ A.instances γ) (k : ℕ) : φs k ∈ A.instances γ

Every conjunct of an instance countable conjunction is an instance.

theorem FirstOrder.Language.Fragment.iSup_mem_instances {L : Language} {A : L.Fragment} {γ : Type w} {φs : ℕ → (L.withConstants γ).Sentenceω} (h : BoundedFormulaInf.iSup φs ∈ A.instances γ) (k : ℕ) : φs k ∈ A.instances γ

Every disjunct of an instance countable disjunction is an instance.

theorem FirstOrder.Language.Fragment.inst_mem_instances {L : Language} {A : L.Fragment} {γ : Type w} {φ : (L.withConstants γ).BoundedFormulaω Empty 1} (h : BoundedFormulaInf.all φ ∈ A.instances γ) (d : γ) : BoundedFormulaInf.inst φ (L.con d).term ∈ A.instances γ

Instantiating an instance universal sentence at a constant gives an instance.

@[simp]

theorem FirstOrder.Language.Fragment.FormationClosed.not_mem_instances_iff {L : Language} {A : L.Fragment} {γ : Type w} (hA : A.FormationClosed) {φ : (L.withConstants γ).Sentenceω} : BoundedFormulaInf.not φ ∈ A.instances γ ↔ φ ∈ A.instances γ

Over a formation-closed fragment, a negation is an instance exactly when the negated sentence is.

theorem FirstOrder.Language.Fragment.FormationClosed.mem_instances_of_isAtomic {L : Language} {A : L.Fragment} {γ : Type w} (hA : A.FormationClosed) {φ : (L.withConstants γ).Sentenceω} (h : BoundedFormulaInf.IsAtomic φ) : φ ∈ A.instances γ

Atomic sentences are instances: over a formation-closed fragment, every atomic sentence of L[[γ]] is an instance.