Documentation

LeanPool.InfinitaryLogic.Methods.Interpolation.GraphReconstruction

Reconstructing functions from a model of the graph axioms (Craig Layer 3, Unit 5b) #

From any nonempty graphLanguage L-structure satisfying graphAxioms F, a full (noncomputable) L.Structure: for f ∈ F the function value is the totality witness (unique by functionality), outside F an arbitrary element; every base relation is copied directly.

The results are deliberately localized to F — global round-trip structure identities are false outside F, and nothing downstream needs them. Graph-expanding a reconstruction preserves the graph relations of F; therefore formulas whose function support lies in F have identical semantics. The consumer-shaped capstone realize_relationalize_reconstruct follows from the occurrence-aware congruence realize_congr_symbolsIn, the exact occurrence identity relationsIn_relationalizeFormula, and Unit 4's realize_relationalizeFormula.

source
@[reducible]
noncomputable def FirstOrder.Language.reconstructStructure {L : Language} {M : Type} [Nonempty M] [L.graphLanguage.Structure M] (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] (hAx : (graphAxioms F).Realize M) :
L.Structure M

The reconstructed L-structure: functions from graphValue, base relations copied.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem FirstOrder.Language.reconstruct_relMap_base {L : Language} {M : Type} [Nonempty M] [L.graphLanguage.Structure M] {F : Set ((n : ℕ) × L.Functions n)} [Countable ↑F] (hAx : (graphAxioms F).Realize M) {n : ℕ} (R : L.Relations n) (v : Fin n → M) :
    Structure.RelMap R v ↔ Structure.RelMap (GraphRelation.base R) v

    Base relations are copied directly — definitionally.

    source
    theorem FirstOrder.Language.realize_relationalize_reconstruct {L : Language} {M : Type} [Nonempty M] [L.graphLanguage.Structure M] {F : Set ((n : ℕ) × L.Functions n)} [Countable ↑F] {α : Type} (hAx : (graphAxioms F).Realize M) {n : ℕ} (φ : L.BoundedFormulaω α n) (hφ : φ.functionsIn ⊆ F) (v : α → M) (xs : Fin n → M) :
    (relationalizeFormula φ).Realize v xs ↔ φ.Realize v xs

    The capstone (consumer-shaped): for formulas whose function support lies in F, the relationalized formula in the ambient graph structure realizes exactly as the original formula in the reconstruction. The choice outside F never enters.