The functional Θ: syntax and semantics (issue #10, Unit 2a)

Marker's Lemma-4.23 sentence over the two-sorted mid-language MidLang L = L.sum WitnessLang (one witness copy; Unit 2b maps it into the tagged KLang per side), with the audit's Unit-2 revision: a default-coordinate clause absent from Marker's bijective-pairing presentation. Without it the f-sequence could carry arbitrary bits at coordinates outside range queryEmbedding while Unit 0's queryCode fixes those coordinates to false, and a path through T would not correspond to the base reduct's query code.

The six clauses:

1. omegaAxioms — (c, s) enumerate the carrier as (ℕ, 0, succ): s injective, c not a successor, and every element is a numeral (countable disjunction);
2. bitAxiom — every f(x) equals c or s(c);
3. codeAxiom — for every query q, R(numerals of q) ↔ f(numeral (queryEmbedding q)) = s(c);
4. defaultAxiom — f(numeral n) = c for every n ∉ range queryEmbedding;
5. treeDiagram T — every tree n pinned at all numeral tuples according to T n (classically: atom if the node is in T, its negation otherwise), including n = 0;
6. pathAxiom — every prefix formed from f and g satisfies tree n, including tree 0.

Exports: per-clause realization lemmas; numMap_bijective (clause 1 gives a bijective numeral map); fBit_eq_queryCode (clauses 1–4 identify the f-bit sequence exactly with queryCode of the base-reduct code pulledCode); the tree pinning as an iff (realize_treeDiagram); and the bundled functionalTheta T.

@[reducible, inline]

abbrev FirstOrder.Language.MidLang (L : Language) : Language

The two-sorted mid-language: the base plus one witness copy.

Equations

• L.MidLang = L.sum FirstOrder.Language.WitnessLang

Terms

def FirstOrder.Language.mNum (L : Language) (α : Type) : ℕ → L.MidLang.Term α

Numeral terms in the mid-language: c, s c, s (s c), ….

Equations

• L.mNum α 0 = FirstOrder.Language.func (Sum.inr FirstOrder.Language.WitnessFun.c) Fin.elim0
• L.mNum α n.succ = FirstOrder.Language.func (Sum.inr FirstOrder.Language.WitnessFun.s) ![L.mNum α n]

def FirstOrder.Language.mF (L : Language) {α : Type} (t : L.MidLang.Term α) : L.MidLang.Term α

f applied to a term.

Equations

• L.mF t = FirstOrder.Language.func (Sum.inr FirstOrder.Language.WitnessFun.f) ![t]

def FirstOrder.Language.mG (L : Language) {α : Type} (t : L.MidLang.Term α) : L.MidLang.Term α

g applied to a term.

Equations

• L.mG t = FirstOrder.Language.func (Sum.inr FirstOrder.Language.WitnessFun.g) ![t]

Semantic shorthands (the language argument is explicit throughout — it is not

inferable from the carrier)

def FirstOrder.Language.sMap (L : Language) (M : Type) [inst : L.MidLang.Structure M] (x : M) : M

The interpreted successor.

Equations

• L.sMap M x = FirstOrder.Language.Structure.funMap (Sum.inr FirstOrder.Language.WitnessFun.s) ![x]

def FirstOrder.Language.fMap (L : Language) (M : Type) [inst : L.MidLang.Structure M] (x : M) : M

The interpreted f.

Equations

• L.fMap M x = FirstOrder.Language.Structure.funMap (Sum.inr FirstOrder.Language.WitnessFun.f) ![x]

def FirstOrder.Language.gMap (L : Language) (M : Type) [inst : L.MidLang.Structure M] (x : M) : M

The interpreted g.

Equations

• L.gMap M x = FirstOrder.Language.Structure.funMap (Sum.inr FirstOrder.Language.WitnessFun.g) ![x]

def FirstOrder.Language.numMap (L : Language) (M : Type) [inst : L.MidLang.Structure M] : ℕ → M

The numeral map ℕ → M.

Equations

• L.numMap M 0 = FirstOrder.Language.Structure.funMap (Sum.inr FirstOrder.Language.WitnessFun.c) Fin.elim0
• L.numMap M n.succ = L.sMap M (L.numMap M n)

@[simp]

theorem FirstOrder.Language.realize_mNum {L : Language} {M : Type} [inst : L.MidLang.Structure M] {α : Type} (v : α → M) (n : ℕ) : Term.realize v (L.mNum α n) = L.numMap M n

Numeral terms realize to the numeral map, under any assignment.

@[simp]

theorem FirstOrder.Language.realize_mF {L : Language} {M : Type} [inst : L.MidLang.Structure M] {α : Type} (t : L.MidLang.Term α) (v : α → M) : Term.realize v (L.mF t) = L.fMap M (Term.realize v t)

@[simp]

theorem FirstOrder.Language.realize_mG {L : Language} {M : Type} [inst : L.MidLang.Structure M] {α : Type} (t : L.MidLang.Term α) (v : α → M) : Term.realize v (L.mG t) = L.gMap M (Term.realize v t)

Clause 1: the ω-axioms

noncomputable def FirstOrder.Language.omegaAxioms (L : Language) : L.MidLang.Sentenceω

Clause 1 (omegaAxioms): s is injective, c is not a successor, and every element is a numeral. Together: the numeral map is a bijection ℕ ≃ carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.realize_omegaAxioms {L : Language} {M : Type} [inst : L.MidLang.Structure M] : L.omegaAxioms.Realize M ↔ Function.Injective (L.sMap M) ∧ (∀ (x : M), L.sMap M x ≠ L.numMap M 0) ∧ Function.Surjective (L.numMap M)

Clause-1 realization: injectivity, non-successorhood of c, numeral surjectivity.

theorem FirstOrder.Language.numMap_bijective {L : Language} {M : Type} [inst : L.MidLang.Structure M] (h : L.omegaAxioms.Realize M) : Function.Bijective (L.numMap M)

Clause 1 export: the numeral map of a model of omegaAxioms is bijective.

Clause 2: the bit axiom

noncomputable def FirstOrder.Language.bitAxiom (L : Language) : L.MidLang.Sentenceω

Clause 2 (bitAxiom): every f-value is c or s(c).

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.realize_bitAxiom {L : Language} {M : Type} [inst : L.MidLang.Structure M] : L.bitAxiom.Realize M ↔ ∀ (x : M), L.fMap M x = L.numMap M 0 ∨ L.fMap M x = L.numMap M 1

Clauses 3 and 4: code and default

noncomputable def FirstOrder.Language.codeAxiom (L : Language) [Countable ((l : ℕ) × L.Relations l)] : L.MidLang.Sentenceω

Clause 3 (codeAxiom): for every query q = (R, v), R(numerals of v) ↔ f(numeral (queryEmbedding q)) = s(c).

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.realize_codeAxiom {L : Language} [Countable ((l : ℕ) × L.Relations l)] {M : Type} [inst : L.MidLang.Structure M] : L.codeAxiom.Realize M ↔ ∀ (q : L.RelQuery), (Structure.RelMap (Sum.inl q.fst.snd) fun (i : Fin q.fst.fst) => L.numMap M (q.snd i)) ↔ L.fMap M (L.numMap M (queryEmbedding q)) = L.numMap M 1

noncomputable def FirstOrder.Language.defaultAxiom (L : Language) [Countable ((l : ℕ) × L.Relations l)] : L.MidLang.Sentenceω

Clause 4 (defaultAxiom, the audit's Unit-2 addition): f(numeral n) = c at every coordinate outside the query embedding's range — matching Unit 0's queryCode default.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.realize_defaultAxiom {L : Language} [Countable ((l : ℕ) × L.Relations l)] {M : Type} [inst : L.MidLang.Structure M] : L.defaultAxiom.Realize M ↔ ∀ n ∉ Set.range ⇑queryEmbedding, L.fMap M (L.numMap M n) = L.numMap M 0

Clause 5: the tree diagram

def FirstOrder.Language.treeAtom (L : Language) (n : ℕ) (σ : Fin n → Bool) (τ : Fin n → ℕ) : L.MidLang.Sentenceω

The tree atom at level n: tree n applied to the bit-numerals of σ followed by the numerals of τ.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.treeTuple (L : Language) (M : Type) [inst : L.MidLang.Structure M] (n : ℕ) (σ : Fin n → Bool) (τ : Fin n → ℕ) : Fin (2 * n) → M

The semantic tuple of a tree atom.

Equations

• L.treeTuple M n σ τ i = if h : ↑i < n then L.numMap M (bif σ ⟨↑i, h⟩ then 1 else 0) else L.numMap M (τ ⟨↑i - n, ⋯⟩)

theorem FirstOrder.Language.realize_treeAtom {L : Language} {M : Type} [inst : L.MidLang.Structure M] (n : ℕ) (σ : Fin n → Bool) (τ : Fin n → ℕ) : (L.treeAtom n σ τ).Realize M ↔ Structure.RelMap (Sum.inr (WitnessRel.tree n)) (L.treeTuple M n σ τ)

noncomputable def FirstOrder.Language.treeDiagram (L : Language) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : L.MidLang.Sentenceω

Clause 5 (treeDiagram): every tree n pinned at all numeral tuples according to T n — the atom when the node is in T n, its negation otherwise — including n = 0.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.realize_treeDiagram {L : Language} {M : Type} [inst : L.MidLang.Structure M] (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : (L.treeDiagram T).Realize M ↔ ∀ (n : ℕ) (σ : Fin n → Bool) (τ : Fin n → ℕ), Structure.RelMap (Sum.inr (WitnessRel.tree n)) (L.treeTuple M n σ τ) ↔ (σ, τ) ∈ T n

Clause-5 realization — an iff, not merely preservation: the interpreted tree n holds at a numeral tuple exactly when the node is in T n.

Clause 6: the path axiom

def FirstOrder.Language.pathAxiom (L : Language) : L.MidLang.Sentenceω

Clause 6 (pathAxiom): for every n — including 0 — the length-n prefixes of f and g along the numerals satisfy tree n.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.pathTuple (L : Language) (M : Type) [inst : L.MidLang.Structure M] (n : ℕ) : Fin (2 * n) → M

The semantic path tuple at level n.

Equations

• L.pathTuple M n i = if ↑i < n then L.fMap M (L.numMap M ↑i) else L.gMap M (L.numMap M (↑i - n))

theorem FirstOrder.Language.realize_pathAxiom {L : Language} {M : Type} [inst : L.MidLang.Structure M] : L.pathAxiom.Realize M ↔ ∀ (n : ℕ), Structure.RelMap (Sum.inr (WitnessRel.tree n)) (L.pathTuple M n)

The pulled-back code and the bit-sequence identification

noncomputable def FirstOrder.Language.pulledCode (L : Language) (M : Type) [inst : L.MidLang.Structure M] : L.StructureSpace

The base-reduct code of a mid-language structure, pulled back along the numeral map: the query q holds iff the base relation holds at the corresponding numerals.

Equations

• L.pulledCode M q = if FirstOrder.Language.Structure.RelMap (Sum.inl q.fst.snd) fun (i : Fin q.fst.fst) => L.numMap M (q.snd i) then true else false

theorem FirstOrder.Language.pulledCode_eq_true {L : Language} (M : Type) [inst : L.MidLang.Structure M] (q : L.RelQuery) : L.pulledCode M q = true ↔ Structure.RelMap (Sum.inl q.fst.snd) fun (i : Fin q.fst.fst) => L.numMap M (q.snd i)

theorem FirstOrder.Language.fBit_eq_queryCode {L : Language} [Countable ((l : ℕ) × L.Relations l)] {M : Type} [inst : L.MidLang.Structure M] (homega : L.omegaAxioms.Realize M) (hcode : L.codeAxiom.Realize M) (hdefault : L.defaultAxiom.Realize M) (n : ℕ) : L.fMap M (L.numMap M n) = L.numMap M 1 ↔ queryCode (L.pulledCode M) n = true

The bit-sequence identification (clauses 1, 3, 4): the f-bit at numeral n is 1 exactly when queryCode of the pulled-back base code is true at n.

The bundle

noncomputable def FirstOrder.Language.functionalTheta (L : Language) [Countable ((l : ℕ) × L.Relations l)] (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : L.MidLang.Sentenceω

The functional Θ over the mid-language: all six clauses.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.realize_functionalTheta {L : Language} [Countable ((l : ℕ) × L.Relations l)] {M : Type} [inst : L.MidLang.Structure M] (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : (L.functionalTheta T).Realize M ↔ L.omegaAxioms.Realize M ∧ L.bitAxiom.Realize M ∧ L.codeAxiom.Realize M ∧ L.defaultAxiom.Realize M ∧ (L.treeDiagram T).Realize M ∧ L.pathAxiom.Realize M

Realization of the bundle: all six clause-level semantics.