The constant support of a formula of L[[γ]] #
The constant support of an infinitary formula of the language L[[γ]] is the set of c : γ
whose constant symbol occurs in it, read off the occurring function symbols. The truth of a
formula in an expansion of an L-structure depends only on how the constants in its support are
interpreted. This is what allows a constant that does not occur in a set of sentences to be
reinterpreted as a witness, the argument behind the witness clauses of consistency properties.
The support is a set rather than a Finset: a countable conjunction can mention infinitely many
constants. A term mentions only finitely many (Term.finite_constantSupport).
Main definitions #
FirstOrder.Language.Term.constantSupport: the constants occurring in a term.FirstOrder.Language.BoundedFormulaInf.constantSupport: the constants occurring in an infinitary formula.
Main results #
FirstOrder.Language.BoundedFormulaInf.realize_congr_of_eqOn_constantSupport: expansions agreeing on the support of a formula give it the same truth value.FirstOrder.Language.BoundedFormulaInf.constantSupport_inst_subset: instantiating at a term adds at most the constants of the term.FirstOrder.Language.BoundedFormulaInf.IsAtomic.inst_eq_or_constantSupport_subset: an atomic instance either does not depend on the instantiated term or contains all of its constants.FirstOrder.Language.BoundedFormulaInf.constantSupport_onBoundedFormulaInf,FirstOrder.Language.BoundedFormulaInf.constantSupport_eq_empty_iff: a formula ofL[[γ]]has empty support precisely when it comes fromL.
References #
cameronfreer/infinitary-logicat commit518a366cba97b1ae8c4dc64a297a396939bc3e0b,InfinitaryLogic/Methods/ConstantSupport.lean:sentenceJConstsandTerm.jConsts, the constant supports of formulas and terms ofL[[J]], likewise read off the occurring function symbols. Divergence from that source: the support here is defined at every carrier, not only atℕ.
def
FirstOrder.Language.Term.constantSupport
{L : Language}
{γ : Type uγ}
{α : Type uα}
(t : (L.withConstants γ).Term α)
:
Set γ
The constant support of a term of L[[γ]]: the c : γ whose constant symbol occurs.
Instances For
theorem
FirstOrder.Language.Term.mem_constantSupport
{L : Language}
{γ : Type uγ}
{α : Type uα}
{t : (L.withConstants γ).Term α}
{c : γ}
:
theorem
FirstOrder.Language.Term.finite_constantSupport
{L : Language}
{γ : Type uγ}
{α : Type uα}
(t : (L.withConstants γ).Term α)
:
A term mentions finitely many constants.
@[simp]
theorem
FirstOrder.Language.Term.constantSupport_var
{L : Language}
{γ : Type uγ}
{α : Type uα}
(a : α)
:
@[simp]
theorem
FirstOrder.Language.Term.constantSupport_func
{L : Language}
{γ : Type uγ}
{α : Type uα}
{k : ℕ}
(f : L.Functions k)
(ts : Fin k → (L.withConstants γ).Term α)
:
(func ((L.lhomWithConstants γ).onFunction f) ts).constantSupport = ⋃ (i : Fin k), (ts i).constantSupport
Applying an original function symbol adds only the constants of its arguments.
@[simp]
theorem
FirstOrder.Language.Term.constantSupport_onTerm
{L : Language}
{γ : Type uγ}
{α : Type uα}
(t : L.Term α)
:
A term of L mentions no constant of L[[γ]].
theorem
FirstOrder.Language.Term.constantSupport_eq_empty_iff
{L : Language}
{γ : Type uγ}
{α : Type uα}
{t : (L.withConstants γ).Term α}
:
A term of L[[γ]] has empty constant support precisely when it comes from L.
theorem
FirstOrder.Language.Term.realize_congr_of_eqOn_constantSupport
{L : Language}
{γ : Type uγ}
{α : Type uα}
{M : Type w}
[L.Structure M]
{e e' : γ → M}
(t : (L.withConstants γ).Term α)
(h : Set.EqOn e e' t.constantSupport)
(v : α → M)
:
Expansions agreeing on the constants of a term give it the same value.
def
FirstOrder.Language.BoundedFormulaInf.constantSupport
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ : (L.withConstants γ).BoundedFormulaInf ι α n)
:
Set γ
The constant support of an infinitary formula of L[[γ]]: the c : γ whose constant
symbol occurs.
Instances For
theorem
FirstOrder.Language.BoundedFormulaInf.mem_constantSupport
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
{φ : (L.withConstants γ).BoundedFormulaInf ι α n}
{c : γ}
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_equal
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(t₁ t₂ : (L.withConstants γ).Term (α ⊕ Fin n))
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_rel
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n k : ℕ}
(R : (L.withConstants γ).Relations k)
(ts : Fin k → (L.withConstants γ).Term (α ⊕ Fin n))
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_imp
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ ψ : (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_not
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ : (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_inf
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ ψ : (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_sup
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ ψ : (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_iff
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ ψ : (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_all
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ : (L.withConstants γ).BoundedFormulaInf ι α (n + 1))
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_ex
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ : (L.withConstants γ).BoundedFormulaInf ι α (n + 1))
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_alls
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ : (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_exs
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ : (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_exsLast
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n k : ℕ}
(φ : (L.withConstants γ).BoundedFormulaInf ι α (n + k))
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_iSup
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φs : ι → (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_iInf
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φs : ι → (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_iInfAlong
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
{κ : Type u_1}
(c : TauCeti.IndexCoding ι κ)
(φs : ι → (L.withConstants γ).BoundedFormulaInf κ α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_iSupAlong
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
{κ : Type u_1}
(c : TauCeti.IndexCoding ι κ)
(φs : ι → (L.withConstants γ).BoundedFormulaInf κ α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_reindex
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
{κ : Type u_1}
(c : TauCeti.IndexCoding ι κ)
(φ : (L.withConstants γ).BoundedFormulaInf ι α n)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_mapBound
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n m : ℕ}
(f : Fin m → Fin n)
(φ : (L.withConstants γ).BoundedFormulaInf ι α m)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_castLE
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n m : ℕ}
(h : m ≤ n)
(φ : (L.withConstants γ).BoundedFormulaInf ι α m)
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_onBoundedFormulaInf
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
(φ : L.BoundedFormulaInf ι α n)
:
A formula of L mentions no constant of L[[γ]].
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_eq_empty_iff
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
{φ : (L.withConstants γ).BoundedFormulaInf ι α n}
:
φ.constantSupport = ∅ ↔ ∃ (φ₀ : L.BoundedFormulaInf ι α n), (L.lhomWithConstants γ).onBoundedFormulaInf φ₀ = φ
An infinitary formula of L[[γ]] has empty constant support precisely when it is the image of
a formula of L along lhomWithConstants.
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_inst_subset
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
(φ : (L.withConstants γ).BoundedFormulaInf ι α 1)
(t : (L.withConstants γ).Term (α ⊕ Fin 0))
:
constantSupport (φ.inst t) ⊆ φ.constantSupport ∪ t.constantSupport
Instantiating a formula at a term adds at most the constants of the term.
theorem
FirstOrder.Language.BoundedFormulaInf.constantSupport_subset_inst
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
(φ : (L.withConstants γ).BoundedFormulaInf ι α 1)
(t : (L.withConstants γ).Term (α ⊕ Fin 0))
:
φ.constantSupport ⊆ constantSupport (φ.inst t)
Every constant of a formula occurs in its instances.
theorem
FirstOrder.Language.BoundedFormulaInf.IsAtomic.inst_eq_or_constantSupport_subset
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{φ : (L.withConstants γ).BoundedFormulaInf ι α 1}
(hφ : φ.IsAtomic)
(t t' : (L.withConstants γ).Term (α ⊕ Fin 0))
:
An atomic formula either ignores its bound position, so that all its instances agree, or its
instance at t contains every constant of t.
theorem
FirstOrder.Language.BoundedFormulaInf.realize_congr_of_eqOn_constantSupport
{L : Language}
{γ : Type uγ}
{ι : Type uι}
{α : Type uα}
{n : ℕ}
{M : Type w}
[L.Structure M]
{e e' : γ → M}
(φ : (L.withConstants γ).BoundedFormulaInf ι α n)
(h : Set.EqOn e e' φ.constantSupport)
(v : α → M)
(xs : Fin n → M)
:
Constant locality. Expansions of one L-structure which interpret the constants in the
support of a formula alike give it the same truth value.