The standard functional model and the forward presentation (issue #10, Unit 3a)

The graph-language code reduct along the base embedding, and the standard functional expansion on ℕ built from a base code c and a branch g:

• c^M = 0, s^M = succ (so numMap = id);
• f^M n = 1 exactly when queryCode c n = true;
• g^M = g;
• base relations read off c;
• tree n interpreted by T n, with false outside bit-coded first halves.

Forward acceptance gate (subset_pcClass): c ∈ B → ∃ d, codeReduct d = c ∧ d ∈ ModelsOf (pcSentence side T) — without IsomorphismInvariant.

The code reduct

def FirstOrder.Language.codeReduct {L : Language} (d : L.KLang.graphLanguage.StructureSpace) : L.StructureSpace

The base-language code reduct of a graphLanguage (KLang L)-code: read each base query through the graph-language image G_base(Sum.inl R) of the base relation.

Equations

• FirstOrder.Language.codeReduct d q = d ⟨⟨q.fst.fst, FirstOrder.Language.GraphRelation.base (Sum.inl q.fst.snd)⟩, q.snd⟩

theorem FirstOrder.Language.codeReduct_toStructure {L : Language} [L.IsRelational] {d : L.KLang.graphLanguage.StructureSpace} {l : ℕ} (R : L.Relations l) (v : Fin l → ℕ) : Structure.RelMap R v ↔ Structure.RelMap (GraphRelation.base (Sum.inl R)) v

Compatibility with decoded structures: the reduct code's relations are the base graph relations of the decoded structure.

The standard functional structure

def FirstOrder.Language.LopezStd.decodeBit (m : ℕ) : Bool

Decode a {0,1}-valued numeral back to a bit.

Equations

• FirstOrder.Language.LopezStd.decodeBit m = decide (m = 1)

theorem FirstOrder.Language.LopezStd.decodeBit_cond (b : Bool) : decodeBit (bif b then 1 else 0) = b

def FirstOrder.Language.LopezStd.firstIdx (n : ℕ) (i : Fin n) : Fin (2 * n)

The first-half Fin (2n) index of i : Fin n.

Equations

• FirstOrder.Language.LopezStd.firstIdx n i = ⟨↑i, ⋯⟩

def FirstOrder.Language.LopezStd.secondIdx (n : ℕ) (i : Fin n) : Fin (2 * n)

The second-half Fin (2n) index of i : Fin n.

Equations

• FirstOrder.Language.LopezStd.secondIdx n i = ⟨n + ↑i, ⋯⟩

noncomputable def FirstOrder.Language.LopezStd.wFun {L : Language} [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) {k : ℕ} : WitnessFun k → (Fin k → ℕ) → ℕ

The witness function interpretation on ℕ: c ↦ 0, s ↦ succ, f ↦ the query bit, g ↦ the branch.

Equations

• FirstOrder.Language.LopezStd.wFun c g FirstOrder.Language.WitnessFun.c x_3 = 0
• FirstOrder.Language.LopezStd.wFun c g FirstOrder.Language.WitnessFun.s a = a 0 + 1
• FirstOrder.Language.LopezStd.wFun c g FirstOrder.Language.WitnessFun.f a = bif FirstOrder.Language.queryCode c (a 0) then 1 else 0
• FirstOrder.Language.LopezStd.wFun c g FirstOrder.Language.WitnessFun.g a = g (a 0)

def FirstOrder.Language.LopezStd.wRel (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) {k : ℕ} : WitnessRel k → (Fin k → ℕ) → Prop

The witness (tree) relation interpretation on ℕ: tree n decodes the first half as bits, the second half as τ, and asks membership in T n.

Equations

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

@[reducible]

noncomputable def FirstOrder.Language.LopezStd.standardMid {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : L.MidLang.Structure ℕ

The standard MidLang L-structure on ℕ from a code c, branch g, tree T.

Equations

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

@[reducible]

noncomputable def FirstOrder.Language.LopezStd.standardK {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : L.KLang.Structure ℕ

The standard KLang L-structure on ℕ: both witness copies interpreted identically, so its reduct along either side's embedding is standardMid.

Equations

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

Reductions of the semantic maps in the standard model

The tree tuple / path tuple extractions

The standard model satisfies Θ

Lifting to KLang and graph-expanding

The forward code and its two properties

The forward presentation

theorem FirstOrder.Language.subset_pcClass {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {B : Set L.StructureSpace} (side : PCSide) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (hT : ∀ (c : L.StructureSpace), c ∈ B ↔ ∃ (g : ℕ → ℕ), ∀ (n : ℕ), (fun (i : Fin n) => queryCode c ↑i, fun (i : Fin n) => g ↑i) ∈ T n) : B ⊆ codeReduct '' ModelsOf (L.pcSentence side T)

Forward gate (subset_pcClass): if T characterizes B by branches (Unit 0), then every code of B is the base reduct of a model of the PC sentence. No IsomorphismInvariant.