The functional witness language (issue #10, Unit 1 part 1)

Marker's τ* (Lemma 4.23), as a functional language per audit v2 (D4, graph-translation route): a constant c, unary functions s, f, g, and a 2n-ary tree relation at every n — including tree 0 (the nullary S₀; Marker starts at positive lengths, but admitting level 0 lets the path sentence assert it while the pinning sentence of a branchless tree refutes it, so the empty analytic set yields an inconsistent PC sentence with no special case).

Contents: the language with explicit countability instances for both symbol sigma-types; actual numeral terms numTerm n (c, s c, s (s c), …) with their map-language, occurrence, and realization lemmas; the common tagged language KLang L = L.sum (WitnessLang.sum WitnessLang) with named embeddings for the base, left witness, and right witness symbols; the tagged symbol-image sets; and their pairwise disjointness (the combinatorial half of the Unit-1 occurrence gate).

inductive FirstOrder.Language.WitnessFun : ℕ → Type

Function symbols of the witness language: the zero c and the unary s, f, g.

• c : WitnessFun 0
• s : WitnessFun 1
• f : WitnessFun 1
• g : WitnessFun 1

inductive FirstOrder.Language.WitnessRel : ℕ → Type

Relation symbols of the witness language: one 2n-ary tree relation at every level, including the nullary tree 0.

• tree (n : ℕ) : WitnessRel (2 * n)

def FirstOrder.Language.WitnessLang : Language

The functional witness language (Marker's τ*, audit v2 D4).

Equations

• FirstOrder.Language.WitnessLang = { Functions := FirstOrder.Language.WitnessFun, Relations := FirstOrder.Language.WitnessRel }

instance FirstOrder.Language.instCountableSigmaNatFunctionsWitnessLang : Countable ((n : ℕ) × WitnessLang.Functions n)

instance FirstOrder.Language.instCountableSigmaNatRelationsWitnessLang : Countable ((n : ℕ) × WitnessLang.Relations n)

Numeral terms

def FirstOrder.Language.numTerm (α : Type) : ℕ → WitnessLang.Term α

The numeral terms: numTerm 0 = c, numTerm (n+1) = s (numTerm n).

Equations

• FirstOrder.Language.numTerm α 0 = FirstOrder.Language.func FirstOrder.Language.WitnessFun.c Fin.elim0
• FirstOrder.Language.numTerm α n.succ = FirstOrder.Language.func FirstOrder.Language.WitnessFun.s ![FirstOrder.Language.numTerm α n]

theorem FirstOrder.Language.functionsIn_numTerm {α : Type} (n : ℕ) : (numTerm α n).functionsIn ⊆ {⟨0, WitnessFun.c⟩, ⟨1, WitnessFun.s⟩}

The numeral terms mention only c and s.

theorem FirstOrder.Language.onTerm_numTerm_zero {α : Type} {L' : Language} (φ : WitnessLang →ᴸ L') : φ.onTerm (numTerm α 0) = func (φ.onFunction WitnessFun.c) Fin.elim0

Map-language commutation, zero case.

theorem FirstOrder.Language.onTerm_numTerm_succ {α : Type} {L' : Language} (φ : WitnessLang →ᴸ L') (n : ℕ) : φ.onTerm (numTerm α (n + 1)) = func (φ.onFunction WitnessFun.s) ![φ.onTerm (numTerm α n)]

Map-language commutation, successor case.

theorem FirstOrder.Language.realize_numTerm {α : Type} {M : Type u_1} [inst : WitnessLang.Structure M] (v : α → M) (n : ℕ) : Term.realize v (numTerm α n) = (fun (x : M) => Structure.funMap WitnessFun.s ![x])^[n] (Structure.funMap WitnessFun.c Fin.elim0)

Realization of the numeral terms: the n-fold s-iterate of c.

The common tagged language and its named embeddings

@[reducible, inline]

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

The common tagged language: the base plus two tagged witness copies.

Equations

• L.KLang = L.sum (FirstOrder.Language.WitnessLang.sum FirstOrder.Language.WitnessLang)

def FirstOrder.Language.baseEmb (L : Language) : L →ᴸ L.KLang

The base-symbol embedding.

Equations

• L.baseEmb = FirstOrder.Language.LHom.sumInl

def FirstOrder.Language.leftWitnessEmb (L : Language) : WitnessLang →ᴸ L.KLang

The left-witness embedding.

Equations

• L.leftWitnessEmb = FirstOrder.Language.LHom.sumInr.comp FirstOrder.Language.LHom.sumInl

def FirstOrder.Language.rightWitnessEmb (L : Language) : WitnessLang →ᴸ L.KLang

The right-witness embedding.

Equations

• L.rightWitnessEmb = FirstOrder.Language.LHom.sumInr.comp FirstOrder.Language.LHom.sumInr

Tagged symbol-image sets and their disjointness

def FirstOrder.Language.baseFuns (L : Language) : Set ((n : ℕ) × L.KLang.Functions n)

Base function symbols inside KLang L.

Equations

• L.baseFuns = Set.range fun (p : (n : ℕ) × L.Functions n) => ⟨p.fst, L.baseEmb.onFunction p.snd⟩

def FirstOrder.Language.baseRels (L : Language) : Set ((n : ℕ) × L.KLang.Relations n)

Base relation symbols inside KLang L.

Equations

• L.baseRels = Set.range fun (p : (n : ℕ) × L.Relations n) => ⟨p.fst, L.baseEmb.onRelation p.snd⟩

def FirstOrder.Language.leftFuns (L : Language) : Set ((n : ℕ) × L.KLang.Functions n)

Left-witness function symbols inside KLang L.

Equations

• L.leftFuns = Set.range fun (p : (n : ℕ) × FirstOrder.Language.WitnessLang.Functions n) => ⟨p.fst, L.leftWitnessEmb.onFunction p.snd⟩

def FirstOrder.Language.leftRels (L : Language) : Set ((n : ℕ) × L.KLang.Relations n)

Left-witness relation symbols inside KLang L.

Equations

• L.leftRels = Set.range fun (p : (n : ℕ) × FirstOrder.Language.WitnessLang.Relations n) => ⟨p.fst, L.leftWitnessEmb.onRelation p.snd⟩

def FirstOrder.Language.rightFuns (L : Language) : Set ((n : ℕ) × L.KLang.Functions n)

Right-witness function symbols inside KLang L.

Equations

• L.rightFuns = Set.range fun (p : (n : ℕ) × FirstOrder.Language.WitnessLang.Functions n) => ⟨p.fst, L.rightWitnessEmb.onFunction p.snd⟩

def FirstOrder.Language.rightRels (L : Language) : Set ((n : ℕ) × L.KLang.Relations n)

Right-witness relation symbols inside KLang L.

Equations

• L.rightRels = Set.range fun (p : (n : ℕ) × FirstOrder.Language.WitnessLang.Relations n) => ⟨p.fst, L.rightWitnessEmb.onRelation p.snd⟩

theorem FirstOrder.Language.leftFuns_inter_rightFuns (L : Language) : L.leftFuns ∩ L.rightFuns = ∅

Left/right witness function symbols are disjoint.

theorem FirstOrder.Language.leftRels_inter_rightRels (L : Language) : L.leftRels ∩ L.rightRels = ∅

Left/right witness relation symbols are disjoint.

theorem FirstOrder.Language.baseFuns_inter_leftFuns (L : Language) : L.baseFuns ∩ L.leftFuns = ∅

Base and left-witness function symbols are disjoint (likewise below for the right copy, by the same Sum.inl/Sum.inr clash).

theorem FirstOrder.Language.baseRels_inter_leftRels (L : Language) : L.baseRels ∩ L.leftRels = ∅

theorem FirstOrder.Language.baseFuns_inter_rightFuns (L : Language) : L.baseFuns ∩ L.rightFuns = ∅

theorem FirstOrder.Language.baseRels_inter_rightRels (L : Language) : L.baseRels ∩ L.rightRels = ∅