Reconstruction and the code-class equality (issue #10, Unit 3b)

The converse of Unit 3a: reconstruct the functional KLang-structure from a model of the PC sentence, read a branch off it, and land the base reduct back in B — the only place IsomorphismInvariant is consumed. The endpoints:

• pcClass_subset (needs invariance) — codeReduct '' ModelsOf (pcSentence side T) ⊆ B;
• subset_pcClass (Unit 3a, no invariance) — B ⊆ codeReduct '' ModelsOf (pcSentence side T);
• pcClass_eq (needs invariance) — the code-class equality codeReduct '' ModelsOf (pcSentence side T) = B.

instance FirstOrder.Language.instCountableFunctionsOfRelational {L : Language} [L.IsRelational] : Countable ((n : ℕ) × L.Functions n)

theorem FirstOrder.Language.pcClass_subset {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) (hinv : IsomorphismInvariant B) : codeReduct '' ModelsOf (L.pcSentence side T) ⊆ B

Converse gate (pcClass_subset): the base reducts of the PC class lie in B. This is the sole consumer of IsomorphismInvariant.

theorem FirstOrder.Language.pcClass_eq {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) (hinv : IsomorphismInvariant B) : codeReduct '' ModelsOf (L.pcSentence side T) = B

The code-class equality (needs invariance): the base reducts of the PC class are exactly B.