Assembly and graph translation: the PC sentence (issue #10, Unit 2b)

The side-parametric functional sentence — functionalTheta mapped into the tagged KLang along the left or right witness embedding — and its relationalized PC form

pcSentence side T = graphAxioms (sideFunsSet side) ⊓ relationalizeFormula (functionalPCSentence side T).

Acceptance gates (audit v2, Unit 2b):

• graphExpansion_realizes_pcSentence — graph expansions of functional models satisfy the PC sentence;
• reconstruct_realizes_functionalPCSentence — reconstruction from any model of the PC sentence satisfies the functional sentence;
• functionsIn_pcSentence — the PC sentence has no function symbols;
• relationsIn_pcSentence_subset — its relation symbols lie in the graph images of base symbols plus that side's tagged witness symbols;
• the support lemmas discharge the occurrence_intersection_base hypotheses directly, and pcSentence_relationsIn_inter is the two-presentation intersection bound.

Sides

inductive FirstOrder.Language.PCSide : Type

The two PC presentations.

• left : PCSide
• right : PCSide

def FirstOrder.Language.sideEmb (L : Language) : PCSide → (L.MidLang →ᴸ L.KLang)

The side embedding: base symbols in place, the witness copy tagged left or right.

Equations

• L.sideEmb FirstOrder.Language.PCSide.left = (FirstOrder.Language.LHom.id L).sumMap FirstOrder.Language.LHom.sumInl
• L.sideEmb FirstOrder.Language.PCSide.right = (FirstOrder.Language.LHom.id L).sumMap FirstOrder.Language.LHom.sumInr

def FirstOrder.Language.sideWitnessFuns (L : Language) : PCSide → Set ((n : ℕ) × L.KLang.Functions n)

That side's tagged witness function symbols.

Equations

• L.sideWitnessFuns FirstOrder.Language.PCSide.left = L.leftFuns
• L.sideWitnessFuns FirstOrder.Language.PCSide.right = L.rightFuns

def FirstOrder.Language.sideWitnessRels (L : Language) : PCSide → Set ((n : ℕ) × L.KLang.Relations n)

That side's tagged witness relation symbols.

Equations

• L.sideWitnessRels FirstOrder.Language.PCSide.left = L.leftRels
• L.sideWitnessRels FirstOrder.Language.PCSide.right = L.rightRels

def FirstOrder.Language.sideFunsSet (L : Language) (side : PCSide) : Set ((n : ℕ) × L.KLang.Functions n)

The function symbols a side may mention: base plus its witness copy.

Equations

• L.sideFunsSet side = L.baseFuns ∪ L.sideWitnessFuns side

instance FirstOrder.Language.instCountableElemSigmaNatFunctionsKLangSideFunsSet {L : Language} [Countable ((n : ℕ) × L.Functions n)] (side : PCSide) : Countable ↑(L.sideFunsSet side)

theorem FirstOrder.Language.sideEmb_onFunction_mem {L : Language} (side : PCSide) (p : (n : ℕ) × L.MidLang.Functions n) : ⟨p.fst, (L.sideEmb side).onFunction p.snd⟩ ∈ L.baseFuns ∪ L.sideWitnessFuns side

Every mid-language function symbol lands in base-or-side.

theorem FirstOrder.Language.sideEmb_onRelation_mem {L : Language} (side : PCSide) (p : (n : ℕ) × L.MidLang.Relations n) : ⟨p.fst, (L.sideEmb side).onRelation p.snd⟩ ∈ L.baseRels ∪ L.sideWitnessRels side

Every mid-language relation symbol lands in base-or-side.

The side-parametric functional sentence and its support

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

The side-parametric functional PC sentence: functionalTheta mapped into the tagged language along the side's embedding — defined once, instantiated twice.

Equations

• L.functionalPCSentence side T = FirstOrder.Language.BoundedFormulaω.mapLanguage (L.sideEmb side) (L.functionalTheta T)

theorem FirstOrder.Language.functionsIn_functionalPCSentence {L : Language} [Countable ((l : ℕ) × L.Relations l)] (side : PCSide) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : BoundedFormulaω.functionsIn (L.functionalPCSentence side T) ⊆ L.baseFuns ∪ L.sideWitnessFuns side

theorem FirstOrder.Language.relationsIn_functionalPCSentence {L : Language} [Countable ((l : ℕ) × L.Relations l)] (side : PCSide) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : BoundedFormulaω.relationsIn (L.functionalPCSentence side T) ⊆ L.baseRels ∪ L.sideWitnessRels side

The PC sentence

noncomputable def FirstOrder.Language.pcSentence (L : Language) [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] (side : PCSide) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : L.KLang.graphLanguage.Sentenceω

The PC sentence of a side: that side's graph axioms conjoined with the relationalized functional sentence.

Equations

• L.pcSentence side T = FirstOrder.Language.BoundedFormulaω.and (FirstOrder.Language.graphAxioms (L.sideFunsSet side)) (FirstOrder.Language.relationalizeFormula (L.functionalPCSentence side T))

theorem FirstOrder.Language.realize_pcSentence_iff {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] {N : Type} [L.KLang.graphLanguage.Structure N] (side : PCSide) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : (L.pcSentence side T).Realize N ↔ (graphAxioms (L.sideFunsSet side)).Realize N ∧ Sentenceω.Realize (relationalizeFormula (L.functionalPCSentence side T)) N

Realizing the PC sentence splits into the two conjuncts.

theorem FirstOrder.Language.graphExpansion_realizes_pcSentence {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] {M : Type} [Nonempty M] [instM : L.KLang.Structure M] (side : PCSide) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (hreal : (L.functionalPCSentence side T).Realize M) : (L.pcSentence side T).Realize M

Gate (a): the graph expansion of a functional model satisfies the PC sentence.

theorem FirstOrder.Language.reconstruct_realizes_functionalPCSentence {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] {N : Type} [Nonempty N] [L.KLang.graphLanguage.Structure N] (side : PCSide) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (hAx : (graphAxioms (L.sideFunsSet side)).Realize N) (hrel : Sentenceω.Realize (relationalizeFormula (L.functionalPCSentence side T)) N) : (L.functionalPCSentence side T).Realize N

Gate (b): the reconstruction of any model of the PC sentence's conjuncts satisfies the functional sentence.

theorem FirstOrder.Language.functionsIn_pcSentence {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] (side : PCSide) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : BoundedFormulaω.functionsIn (L.pcSentence side T) = ∅

Gate (c): the PC sentence has no function symbols.

theorem FirstOrder.Language.relationsIn_pcSentence {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] (side : PCSide) (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : BoundedFormulaω.relationsIn (L.pcSentence side T) ⊆ L.KLang.relSym (L.sideFunsSet side) (L.baseRels ∪ L.sideWitnessRels side)

Gate (d): the PC sentence's relation symbols lie in the graph images of the base symbols plus that side's tagged witness symbols.

theorem FirstOrder.Language.pcSentence_relationsIn_inter {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] (T₀ T₁ : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : BoundedFormulaω.relationsIn (L.pcSentence PCSide.left T₀) ∩ BoundedFormulaω.relationsIn (L.pcSentence PCSide.right T₁) ⊆ L.KLang.relSym L.baseFuns L.baseRels

Gate (e): the two presentations' relation symbols meet only in graph images of base symbols — no witness symbol survives.