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. The choice outside F is completely irrelevant to every consumer:

• reconstructing a graph expansion preserves all base relations (definitionally) and funMap on every symbol of F (reconstruct_graphExpansion_funMap);
• graph-expanding a reconstruction preserves base relations (definitionally) and the graph relations of F (graphExpansion_reconstruct_relMap_graph);
• therefore formulas whose function support lies in F have identical semantics — the consumer-shaped capstone realize_relationalize_reconstruct, proved from the occurrence-aware congruence realize_congr_symbolsIn, the exact occurrence identity relationsIn_relationalizeFormula, and Unit 4's realize_relationalizeFormula.

noncomputable def FirstOrder.Language.graphValue {L : Language} {M : Type} [Nonempty M] [L.graphLanguage.Structure M] {F : Set ((n : ℕ) × L.Functions n)} [Countable ↑F] (hAx : (graphAxioms F).Realize M) {n : ℕ} (f : L.Functions n) (xs : Fin n → M) : M

The function value extracted from a model of the graph axioms: the totality witness for f ∈ F (unique by functionality), an arbitrary element outside F.

Equations

• FirstOrder.Language.graphValue hAx f xs = if h : ⟨n, f⟩ ∈ F then Classical.choose ⋯ else Classical.arbitrary M

theorem FirstOrder.Language.graphValue_spec {L : Language} {M : Type} [Nonempty M] [L.graphLanguage.Structure M] {F : Set ((n : ℕ) × L.Functions n)} [Countable ↑F] (hAx : (graphAxioms F).Realize M) {n : ℕ} (f : L.Functions n) (h : ⟨n, f⟩ ∈ F) (xs : Fin n → M) : Structure.RelMap (GraphRelation.graph f) (Fin.snoc xs (graphValue hAx f xs))

The extracted value satisfies the graph relation.

theorem FirstOrder.Language.graphValue_unique {L : Language} {M : Type} [Nonempty M] [L.graphLanguage.Structure M] {F : Set ((n : ℕ) × L.Functions n)} [Countable ↑F] (hAx : (graphAxioms F).Realize M) {n : ℕ} (f : L.Functions n) (h : ⟨n, f⟩ ∈ F) (xs : Fin n → M) (y : M) (hy : Structure.RelMap (GraphRelation.graph f) (Fin.snoc xs y)) : y = graphValue hAx f xs

Uniqueness from functionality: anything the graph relation relates to xs is the extracted value.

@[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.

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.

theorem FirstOrder.Language.reconstruct_funMap_graph_iff {L : Language} {M : Type} [Nonempty M] [L.graphLanguage.Structure M] {F : Set ((n : ℕ) × L.Functions n)} [Countable ↑F] (hAx : (graphAxioms F).Realize M) {n : ℕ} (f : L.Functions n) (h : ⟨n, f⟩ ∈ F) (xs : Fin n → M) (y : M) : Structure.funMap f xs = y ↔ Structure.RelMap (GraphRelation.graph f) (Fin.snoc xs y)

For f ∈ F, the reconstructed funMap is characterized by the graph relation.

theorem FirstOrder.Language.graphExpansion_reconstruct_relMap_graph {L : Language} {M : Type} [Nonempty M] [L.graphLanguage.Structure M] {F : Set ((n : ℕ) × L.Functions n)} [Countable ↑F] (hAx : (graphAxioms F).Realize M) {n : ℕ} (f : L.Functions n) (h : ⟨n, f⟩ ∈ F) (v : Fin (n + 1) → M) : Structure.RelMap (GraphRelation.graph f) v ↔ Structure.RelMap (GraphRelation.graph f) v

Graph-expanding a reconstruction preserves the graph relations of F.

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.

Localized round-trip: reconstructing a graph expansion

theorem FirstOrder.Language.reconstruct_graphExpansion_relMap {L : Language} {M : Type} [Nonempty M] [L.Structure M] (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] {n : ℕ} (R : L.Relations n) (v : Fin n → M) : Structure.RelMap R v ↔ Structure.RelMap R v

Reconstructing the graph expansion preserves all base relations — definitionally.

theorem FirstOrder.Language.reconstruct_graphExpansion_funMap {L : Language} {M : Type} [Nonempty M] [L.Structure M] (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] {n : ℕ} (f : L.Functions n) (h : ⟨n, f⟩ ∈ F) (v : Fin n → M) : Structure.funMap f v = Structure.funMap f v

Reconstructing the graph expansion recovers funMap on every symbol of F.