The shared-symbol decoder (issue #10, Unit 5a)

Craig separation returns a sentence over the shared vocabulary of the two PC presentations, namely symbSublang of the intersections of their occurrence sets. Unit 2b's pcSentence_relationsIn_inter already proves that this intersection contains only graph images of base relation symbols, so the separator can be decoded straight back into L — no detour through KLang L or backTranslateFormula is needed.

Contents:

• sharedLang — the Craig shared language, exactly as craig_pcSeparation_relational returns it for the two side sentences;
• exists_base_of_mem_relSym — under L.IsRelational, every symbol of relSym (KLang L) (baseFuns L) (baseRels L) is GraphRelation.base (Sum.inl R) for a base relation R of the same arity (the baseFuns branch is vacuous);
• sharedToBase : sharedLang L T₀ T₁ →ᴸ L — the decoder, with sharedToBase_onRelation_spec recovering the shared symbol from its base preimage;
• realize_sharedToBase — the semantic square: for every graph code d, a shared sentence holds in the sublanguage reduct of d iff its decoding holds in codeReduct d.

The shared language

@[reducible, inline]

noncomputable abbrev FirstOrder.Language.sharedLang (L : Language) [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (T₀ T₁ : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : Language

The Craig shared language of the two PC presentations: the two-sorted sublanguage of graphLanguage (KLang L) generated by the intersections of their occurrence sets — exactly the language over which craig_pcSeparation_relational produces its separator.

Equations

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

Decoding a shared relation symbol

theorem FirstOrder.Language.exists_base_of_mem_relSym {L : Language} [L.IsRelational] {n : ℕ} {r : L.KLang.graphLanguage.Relations n} (h : ⟨n, r⟩ ∈ L.KLang.relSym L.baseFuns L.baseRels) : ∃ (R : L.Relations n), r = GraphRelation.base (Sum.inl R)

Under L.IsRelational the base-generated graph symbols are exactly the base images: the graphRelSym '' baseFuns branch of relSym is empty, so every member is GraphRelation.base (Sum.inl R) at the same arity.

noncomputable def FirstOrder.Language.sharedToBase (L : Language) [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (T₀ T₁ : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) : L.sharedLang T₀ T₁ →ᴸ L

The shared-symbol decoder sharedLang L T₀ T₁ →ᴸ L: the shared language has no function symbols (the graph language is relational), and each shared relation symbol is the graph image of a unique base relation symbol, which the decoder returns.

Equations

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

theorem FirstOrder.Language.sharedToBase_onRelation_spec {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (T₀ T₁ : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) {n : ℕ} (r : (L.sharedLang T₀ T₁).Relations n) : ↑r = GraphRelation.base (Sum.inl ((L.sharedToBase T₀ T₁).onRelation r))

The decoder recovers the shared symbol: its base image is the symbol itself.

The semantic square

theorem FirstOrder.Language.sharedToBase_isExpansionOn {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (T₀ T₁ : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (d : L.KLang.graphLanguage.StructureSpace) : (L.sharedToBase T₀ T₁).IsExpansionOn ℕ

The decoder is an expansion from the sublanguage reduct of a graph code onto its base code reduct: shared relations are read the same way on both sides.

theorem FirstOrder.Language.realize_sharedToBase {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (T₀ T₁ : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (θ₀ : (L.sharedLang T₀ T₁).Sentenceω) (d : L.KLang.graphLanguage.StructureSpace) : θ₀.Realize ℕ ↔ Sentenceω.Realize (BoundedFormulaω.mapLanguage (L.sharedToBase T₀ T₁) θ₀) ℕ

The semantic square (the Unit-5a gate): a shared sentence holds in the sublanguage reduct of a graph code exactly when its decoding along sharedToBase holds in the code reduct. This is what lets the Craig separator be read as an L-sentence about base codes.