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)

@[simp]

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

theorem FirstOrder.Language.LopezStd.sMap_std {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (x : ℕ) : L.sMap ℕ x = x + 1

theorem FirstOrder.Language.LopezStd.numMap_std {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (m : ℕ) : L.numMap ℕ m = m

theorem FirstOrder.Language.LopezStd.fMap_std {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (x : ℕ) : L.fMap ℕ x = bif queryCode c x then 1 else 0

theorem FirstOrder.Language.LopezStd.gMap_std {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (x : ℕ) : L.gMap ℕ x = g x

The tree tuple / path tuple extractions

theorem FirstOrder.Language.LopezStd.treeTuple_firstIdx {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (n : ℕ) (σ : Fin n → Bool) (τ : Fin n → ℕ) (i : Fin n) : L.treeTuple ℕ n σ τ (firstIdx n i) = bif σ i then 1 else 0

theorem FirstOrder.Language.LopezStd.treeTuple_secondIdx {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (n : ℕ) (σ : Fin n → Bool) (τ : Fin n → ℕ) (i : Fin n) : L.treeTuple ℕ n σ τ (secondIdx n i) = τ i

theorem FirstOrder.Language.LopezStd.pathTuple_firstIdx {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (n : ℕ) (i : Fin n) : L.pathTuple ℕ n (firstIdx n i) = bif queryCode c ↑i then 1 else 0

theorem FirstOrder.Language.LopezStd.pathTuple_secondIdx {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (n : ℕ) (i : Fin n) : L.pathTuple ℕ n (secondIdx n i) = g ↑i

The standard model satisfies Θ

theorem FirstOrder.Language.LopezStd.standardMid_models {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (hbranch : ∀ (n : ℕ), (fun (i : Fin n) => queryCode c ↑i, fun (i : Fin n) => g ↑i) ∈ T n) : (L.functionalTheta T).Realize ℕ

Lifting to KLang and graph-expanding

theorem FirstOrder.Language.LopezStd.sideEmb_isExpansionOn {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (side : PCSide) : (L.sideEmb side).IsExpansionOn ℕ

sideEmb is an expansion of standardK onto standardMid.

theorem FirstOrder.Language.LopezStd.standardK_models_pc {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (side : PCSide) (hbranch : ∀ (n : ℕ), (fun (i : Fin n) => queryCode c ↑i, fun (i : Fin n) => g ↑i) ∈ T n) : (L.functionalPCSentence side T).Realize ℕ

The forward code and its two properties

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

The forward code: the encoded graph expansion of the standard KLang model (independent of the side).

Equations

• FirstOrder.Language.LopezStd.forwardCode c g T = FirstOrder.Language.StructureSpaceOn.ofStructure (L.KLang.graphExpansion ℕ)

theorem FirstOrder.Language.LopezStd.forwardCode_toStructure {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : (forwardCode c g T).toStructure = L.KLang.graphExpansion ℕ

theorem FirstOrder.Language.LopezStd.forwardCode_mem_modelsOf {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (side : PCSide) (hbranch : ∀ (n : ℕ), (fun (i : Fin n) => queryCode c ↑i, fun (i : Fin n) => g ↑i) ∈ T n) : forwardCode c g T ∈ ModelsOf (L.pcSentence side T)

theorem FirstOrder.Language.LopezStd.codeReduct_forwardCode {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (g : ℕ → ℕ) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : codeReduct (forwardCode c g T) = c

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.