Graph axioms: totality and functionality (Craig Layer 3, Unit 5a)

The sentences asserting that the graph relations of a symbol set F really are function graphs: for each f ∈ F, totality ∀ x⃗ ∃ y, G_f(x⃗, y) and functionality ∀ x⃗ y z, G_f(x⃗,y) → G_f(x⃗,z) → y = z, bundled as graphAxioms F — the countable conjunction over F (hence [Countable ↥F]; the sentence does not depend on a choice of proof of countability, and F = ∅ correctly produces a tautology).

Quantifier blocks are forallBlock/existsBlock with the output variable last, matching the graph-relation convention funMap f args = output.

Main Results

• realize_graphTotality / realize_graphFunctionality — the per-symbol semantic gates.
• realize_graphAxioms_iff — realizing the bundle is exactly realizing both gates for every f ∈ F; realize_graphAxioms_union — the semantic union lemma.
• graphExpansion_realizes_graphAxioms — the graph expansion of an actual L-structure satisfies the axioms for every F.
• relationsIn_graphAxioms = graphRelSym L '' F (and functionsIn_graphAxioms = ∅) — the exact occurrence identities.

Unit 5b consumes these to reconstruct an L-structure from any model of graphAxioms F.

The axiom sentences

def FirstOrder.Language.graphTotality {L : Language} {n : ℕ} (f : L.Functions n) : L.graphLanguage.Sentenceω

Totality of the graph relation of f: ∀ x⃗, ∃ y, G_f(x⃗, y) — output variable last.

Equations

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

def FirstOrder.Language.graphFunctionality {L : Language} {n : ℕ} (f : L.Functions n) : L.graphLanguage.Sentenceω

Functionality of the graph relation of f: ∀ x⃗ y z, G_f(x⃗, y) → G_f(x⃗, z) → y = z — one universal block of n + 2 variables, the two output candidates last.

Equations

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

noncomputable def FirstOrder.Language.graphAxioms {L : Language} (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] : L.graphLanguage.Sentenceω

The graph axioms of a symbol set F: totality and functionality of G_f for every f ∈ F, as one countable conjunction. F = ∅ produces a tautology.

Equations

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

Semantic gates

theorem FirstOrder.Language.realize_graphTotality {L : Language} {M : Type} [L.graphLanguage.Structure M] {n : ℕ} (f : L.Functions n) : (graphTotality f).Realize M ↔ ∀ (ws : Fin n → M), ∃ (y : M), Structure.RelMap (GraphRelation.graph f) (Fin.snoc ws y)

Totality realizes to: every argument tuple has an output related by G_f.

theorem FirstOrder.Language.realize_graphFunctionality {L : Language} {M : Type} [L.graphLanguage.Structure M] {n : ℕ} (f : L.Functions n) : (graphFunctionality f).Realize M ↔ ∀ (ws : Fin n → M) (y z : M), Structure.RelMap (GraphRelation.graph f) (Fin.snoc ws y) → Structure.RelMap (GraphRelation.graph f) (Fin.snoc ws z) → y = z

Functionality realizes to: G_f relates each argument tuple to at most one output.

theorem FirstOrder.Language.realize_graphAxioms_iff {L : Language} {M : Type} [L.graphLanguage.Structure M] (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] : (graphAxioms F).Realize M ↔ ∀ (p : ↑F), (graphTotality (↑p).snd).Realize M ∧ (graphFunctionality (↑p).snd).Realize M

The bundle realizes iff both gates realize for every symbol of F.

theorem FirstOrder.Language.realize_graphAxioms_union {L : Language} {M : Type} [L.graphLanguage.Structure M] (F₁ F₂ : Set ((n : ℕ) × L.Functions n)) [Countable ↑F₁] [Countable ↑F₂] : (graphAxioms (F₁ ∪ F₂)).Realize M ↔ (graphAxioms F₁).Realize M ∧ (graphAxioms F₂).Realize M

The semantic union lemma: the axioms of a union are the conjunction of the axioms.

theorem FirstOrder.Language.graphExpansion_realizes_graphAxioms {L : Language} (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] (M : Type) [L.Structure M] : (graphAxioms F).Realize M

The graph expansion of an L-structure satisfies the graph axioms of every symbol set.

Occurrence identities

theorem FirstOrder.Language.relationsIn_graphTotality {L : Language} {n : ℕ} (f : L.Functions n) : BoundedFormulaω.relationsIn (graphTotality f) = {⟨n + 1, GraphRelation.graph f⟩}

theorem FirstOrder.Language.relationsIn_graphFunctionality {L : Language} {n : ℕ} (f : L.Functions n) : BoundedFormulaω.relationsIn (graphFunctionality f) = {⟨n + 1, GraphRelation.graph f⟩}

theorem FirstOrder.Language.relationsIn_graphAxioms {L : Language} (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] : BoundedFormulaω.relationsIn (graphAxioms F) = L.graphRelSym '' F

The exact occurrence identity: the graph axioms of F mention exactly the graph relations of F.

theorem FirstOrder.Language.functionsIn_graphAxioms {L : Language} (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] : BoundedFormulaω.functionsIn (graphAxioms F) = ∅

No function symbol occurs in the graph axioms (the graph language is relational).