Constant elimination and the syntactic consistency transport

The syntactic half of the constants question for the source-fragment adapter (issue #19).

Constant elimination

elimConstsTerm t₀ and elimConsts t₀ replace every constant c_k of L[[ℕ]] by one fixed closed base term t₀, structurally; variables and binders are untouched. Elimination retracts mapLanguage (elimConsts_mapLanguage) and commutes with relabel, castLE, openBounds and subst, so the closing operations of Methods/ConstantInstances.lean are respected: elimConsts_closeBy sends a constant-closed member of a fragment to the corresponding term-closed member.

The derivation homomorphism

Derivable.map_elimConsts: a derivation over the expansion maps to a derivation over the base, with every rule mapping to itself. The ω-rule obtains its base instances from the premises at the onTerm images of the base closed terms, and imp_intro is unaffected because no quantifier prefix is introduced — the substitution translation, not the universal-prefix translation. AConsistent.of_elimConsts is the contrapositive; Derivable.mono_perm and AConsistent.anti_perm record that permission sets enter only as side conditions.

The transport

Fragment.closedInstances F is the base-side counterpart of Fragment.withNatConstantsSentences: every member, at every arity, closed by base terms. It contains the sentence slice, and aconsistent_withConstants_of_closedInstances transports consistency over it into consistency in the constants expansion, for any closed base term t₀.

What this module does not do

It has no semantic composition with the relational kernel. Language.IsRelational empties every function arity including zero, so a relational language has no closed term (isEmpty_term_empty_of_isRelational), and the relational adapters of HenkinClosed.lean and SourceFragment.lean require [L.IsRelational]. A theorem assuming both would hold by explosion. The arbitrary-language semantic endpoint is pending the relationalization transport; the guard scripts/check_constant_transport_boundary.lean rejects any declaration in these modules whose type mentions both a relational-language instance and a closed base term.

def FirstOrder.Language.elimConstsFunc {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} (f : (L.withConstants ℕ).Functions n) (args : Fin n → L.Term α) : L.Term α

The image of a symbol application: a base symbol keeps its (translated) arguments, a constant becomes t₀.

Equations

• FirstOrder.Language.elimConstsFunc t₀ (Sum.inl g) args = FirstOrder.Language.func g args
• FirstOrder.Language.elimConstsFunc t₀ (Sum.inr val) args = FirstOrder.Language.Term.relabel Empty.elim t₀

def FirstOrder.Language.elimConstsTerm {L : Language} (t₀ : L.Term Empty) {α : Type} : (L.withConstants ℕ).Term α → L.Term α

Replace every constant by t₀.

Equations

• FirstOrder.Language.elimConstsTerm t₀ (FirstOrder.Language.var x_1) = FirstOrder.Language.var x_1
• FirstOrder.Language.elimConstsTerm t₀ (FirstOrder.Language.func f ts) = FirstOrder.Language.elimConstsFunc t₀ f fun (i : Fin l) => FirstOrder.Language.elimConstsTerm t₀ (ts i)

theorem FirstOrder.Language.elimConstsTerm_var {L : Language} (t₀ : L.Term Empty) {α : Type} (x : α) : elimConstsTerm t₀ (var x) = var x

theorem FirstOrder.Language.elimConstsTerm_func_inl {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} (g : L.Functions n) (ts : Fin n → (L.withConstants ℕ).Term α) : elimConstsTerm t₀ (func (Sum.inl g) ts) = func g fun (i : Fin n) => elimConstsTerm t₀ (ts i)

theorem FirstOrder.Language.elimConstsTerm_onTerm {L : Language} (t₀ : L.Term Empty) {α : Type} (t : L.Term α) : elimConstsTerm t₀ ((L.lhomWithConstants ℕ).onTerm t) = t

theorem FirstOrder.Language.elimConstsTerm_constTerm {L : Language} (t₀ : L.Term Empty) (k : ℕ) : elimConstsTerm t₀ (constTerm k) = Term.relabel Empty.elim t₀

Formulas

def FirstOrder.Language.elimConsts {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} : (L.withConstants ℕ).BoundedFormulaω α n → L.BoundedFormulaω α n

Replace every constant by t₀ throughout a bounded formula: structural, variables and binders untouched.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.elimConsts t₀ FirstOrder.Language.BoundedFormulaInf.falsum = FirstOrder.Language.BoundedFormulaω.falsum
• FirstOrder.Language.elimConsts t₀ (FirstOrder.Language.BoundedFormulaInf.rel (Sum.inr r) ts) = isEmptyElim r
• FirstOrder.Language.elimConsts t₀ (FirstOrder.Language.BoundedFormulaInf.imp φ ψ) = (FirstOrder.Language.elimConsts t₀ φ).imp (FirstOrder.Language.elimConsts t₀ ψ)
• FirstOrder.Language.elimConsts t₀ (FirstOrder.Language.BoundedFormulaInf.all φ) = (FirstOrder.Language.elimConsts t₀ φ).all
• FirstOrder.Language.elimConsts t₀ (FirstOrder.Language.BoundedFormulaInf.iSup φs) = FirstOrder.Language.BoundedFormulaω.iSup fun (i : ℕ) => FirstOrder.Language.elimConsts t₀ (φs i)
• FirstOrder.Language.elimConsts t₀ (FirstOrder.Language.BoundedFormulaInf.iInf φs) = FirstOrder.Language.BoundedFormulaω.iInf fun (i : ℕ) => FirstOrder.Language.elimConsts t₀ (φs i)

theorem FirstOrder.Language.elimConsts_imp {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} (φ ψ : (L.withConstants ℕ).BoundedFormulaω α n) : elimConsts t₀ (φ.imp ψ) = (elimConsts t₀ φ).imp (elimConsts t₀ ψ)

theorem FirstOrder.Language.elimConsts_not {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω α n) : elimConsts t₀ φ.not = (elimConsts t₀ φ).not

theorem FirstOrder.Language.elimConsts_falsum {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} : elimConsts t₀ BoundedFormulaω.falsum = BoundedFormulaω.falsum

theorem FirstOrder.Language.elimConsts_iInf {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} (φs : ℕ → (L.withConstants ℕ).BoundedFormulaω α n) : elimConsts t₀ (BoundedFormulaω.iInf φs) = BoundedFormulaω.iInf fun (i : ℕ) => elimConsts t₀ (φs i)

theorem FirstOrder.Language.elimConsts_iSup {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} (φs : ℕ → (L.withConstants ℕ).BoundedFormulaω α n) : elimConsts t₀ (BoundedFormulaω.iSup φs) = BoundedFormulaω.iSup fun (i : ℕ) => elimConsts t₀ (φs i)

theorem FirstOrder.Language.elimConsts_all {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω α (n + 1)) : elimConsts t₀ φ.all = (elimConsts t₀ φ).all

theorem FirstOrder.Language.elimConsts_mapLanguage {L : Language} (t₀ : L.Term Empty) {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : elimConsts t₀ (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) = φ

Base formulas mapped into the expansion come back unchanged.

Commutation with openBounds and subst

theorem FirstOrder.Language.elimConstsTerm_relabel {L : Language} (t₀ : L.Term Empty) {α β : Type} (f : α → β) (t : (L.withConstants ℕ).Term α) : elimConstsTerm t₀ (Term.relabel f t) = Term.relabel f (elimConstsTerm t₀ t)

theorem FirstOrder.Language.elimConstsTerm_subst {L : Language} (t₀ : L.Term Empty) {α β : Type} (t : (L.withConstants ℕ).Term α) (tf : α → (L.withConstants ℕ).Term β) : elimConstsTerm t₀ (t.subst tf) = (elimConstsTerm t₀ t).subst fun (a : α) => elimConstsTerm t₀ (tf a)

theorem FirstOrder.Language.elimConstsTerm_subst.Term.subst_empty_eq_relabel' {L : Language} (t : L.Term Empty) {β : Type} (f : Empty → L.Term β) (g : Empty → β) : Term.relabel g t = t.subst f

theorem FirstOrder.Language.elimConsts_castLE {L : Language} (t₀ : L.Term Empty) {α : Type} {m n : ℕ} (h : m ≤ n) (φ : (L.withConstants ℕ).BoundedFormulaω α m) : elimConsts t₀ (BoundedFormulaω.castLE h φ) = BoundedFormulaω.castLE h (elimConsts t₀ φ)

theorem FirstOrder.Language.elimConsts_relabel {L : Language} (t₀ : L.Term Empty) {α β : Type} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω α k) : elimConsts t₀ (BoundedFormulaω.relabel g φ) = BoundedFormulaω.relabel g (elimConsts t₀ φ)

theorem FirstOrder.Language.elimConsts_openBounds {L : Language} (t₀ : L.Term Empty) {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) : elimConsts t₀ φ.openBounds = (elimConsts t₀ φ).openBounds

theorem FirstOrder.Language.elimConsts_substAux {L : Language} (t₀ : L.Term Empty) {α β : Type} {n : ℕ} (tf : α → (L.withConstants ℕ).Term β) : (fun (x : α ⊕ Fin n) => elimConstsTerm t₀ (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) x)) = Sum.elim (Term.relabel Sum.inl ∘ fun (a : α) => elimConstsTerm t₀ (tf a)) (var ∘ Sum.inr)

The bound-variable-aware substitution map of BoundedFormulaω.subst commutes with constant elimination, pointwise.

theorem FirstOrder.Language.elimConsts_subst {L : Language} (t₀ : L.Term Empty) {α β : Type} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω α n) (tf : α → (L.withConstants ℕ).Term β) : elimConsts t₀ (φ.subst tf) = (elimConsts t₀ φ).subst fun (a : α) => elimConstsTerm t₀ (tf a)

The derivation homomorphism

@[reducible, inline]

abbrev FirstOrder.Language.elimConstsSet {L : Language} (t₀ : L.Term Empty) (P : Set (L.withConstants ℕ).Sentenceω) : Set L.Sentenceω

The image of a sentence set.

Equations

• FirstOrder.Language.elimConstsSet t₀ P = FirstOrder.Language.elimConsts t₀ '' P

theorem FirstOrder.Language.Derivable.map_elimConsts {L : Language} (t₀ : L.Term Empty) {P T : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} (hd : Derivable P T φ) : Derivable (elimConstsSet t₀ P) (elimConstsSet t₀ T) (elimConsts t₀ φ)

Derivations transport along constant elimination. Every rule maps to itself; the ω-rule needs instances at every closed base term, obtained from the premise at that term's image in the expansion.

theorem FirstOrder.Language.AConsistent.of_elimConsts {L : Language} (t₀ : L.Term Empty) {P T : Set (L.withConstants ℕ).Sentenceω} (h : AConsistent (elimConstsSet t₀ P) (elimConstsSet t₀ T)) : AConsistent P T

Consistency transports back: consistency of the images gives consistency in the expansion.

The base-side closed-instance universe and the transport theorem

def FirstOrder.Language.closeByTerms {L : Language} {n : ℕ} (φ : L.BoundedFormulaω Empty n) (τ : Fin n → L.Term Empty) : L.Sentenceω

Close a bounded formula by closed base terms: the base analogue of closeBy.

Equations

• FirstOrder.Language.closeByTerms φ τ = FirstOrder.Language.BoundedFormulaω.subst φ.openBounds τ

def FirstOrder.Language.Fragment.closedInstances {L : Language} (F : L.Fragment) : Set L.Sentenceω

The closed-instance universe of a fragment: every member, at every arity, closed by base terms.

Equations

• F.closedInstances = {σ : L.Sentenceω | ∃ (n : ℕ) (φ : L.BoundedFormulaω Empty n) (τ : Fin n → L.Term Empty), ⟨n, φ⟩ ∈ F ∧ σ = FirstOrder.Language.closeByTerms φ τ}

theorem FirstOrder.Language.Fragment.sentenceSlice_subset_closedInstances {L : Language} (F : L.Fragment) : F.sentenceSlice ⊆ F.closedInstances

theorem FirstOrder.Language.elimConsts_closeBy {L : Language} (t₀ : L.Term Empty) {n : ℕ} (φ : L.BoundedFormulaω Empty n) (a : Fin n → ℕ) : elimConsts t₀ (closeBy (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) a) = closeByTerms φ fun (x : Fin n) => Term.relabel Empty.elim t₀

Eliminating the constants from a constant-closed member gives a term-closed member.

theorem FirstOrder.Language.elimConsts_image_withNatConstantsSentences_subset {L : Language} (t₀ : L.Term Empty) (F : L.Fragment) : elimConstsSet t₀ F.withNatConstantsSentences ⊆ F.closedInstances

theorem FirstOrder.Language.elimConsts_image_mapLanguage {L : Language} (t₀ : L.Term Empty) (T : Set L.Sentenceω) : elimConstsSet t₀ (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' T) = T

theorem FirstOrder.Language.Derivable.mono_perm {L : Language} {P P' T : Set L.Sentenceω} {φ : L.Sentenceω} (hP : P ⊆ P') (hd : Derivable P T φ) : Derivable P' T φ

Permission sets only appear as side conditions, so derivability is monotone in them.

theorem FirstOrder.Language.AConsistent.anti_perm {L : Language} {P P' T : Set L.Sentenceω} (hP : P ⊆ P') (h : AConsistent P' T) : AConsistent P T

theorem FirstOrder.Language.aconsistent_withConstants_of_closedInstances {L : Language} (t₀ : L.Term Empty) (F : L.Fragment) {T₀ : Set L.Sentenceω} (h : AConsistent F.closedInstances T₀) : AConsistent F.withNatConstantsSentences (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' T₀)

The transport: consistency over the closed-instance universe gives consistency in the constants expansion, for any closed base term t₀.

The boundary with the relational kernel

Language.IsRelational empties every function arity, including arity zero, so a relational language has no closed term. The transport above therefore has no composition with the relational kernel adapters of HenkinClosed.lean and SourceFragment.lean, which require [L.IsRelational]: a theorem assuming both would be vacuous. The arbitrary-language semantic endpoint is pending the relationalization transport, and scripts/check_constant_transport_boundary.lean rejects any declaration whose type mentions both.

theorem FirstOrder.Language.isEmpty_term_empty_of_isRelational {L : Language} [L.IsRelational] : IsEmpty (L.Term Empty)

A relational language has no closed term.