The graph universe of a source fragment

The countable-signature, not-necessarily-relational endpoint of the source-fragment adapter (issue #19), by relationalization applied before the proof system.

Constructions

• relationalizeTagged — the sigma-level relationalization of a tagged formula.
• relationalizeTheory — the relationalized theory.
• Fragment.functionSupport F — the function symbols occurring in members of F; countable for countable F, which is what graphAxioms needs.
• Fragment.graphFragment F hF — the Henkin closure of the relationalized members together with the graph axioms of the support; a fragment of graphLanguage L.
• Fragment.graphUniverse F hF — its constants-expanded universe.
• Fragment.graphTheory F hF T — the relationalized theory with the graph axioms, mapped into the constants expansion.

The countability parameter hF is not optional: graphAxioms is a countable conjunction over the support.

Endpoint

Fragment.exists_countable_model_of_aconsistent_graphUniverse: a theory in a countable fragment whose graph theory is consistent in the graph universe has a countable L-model. Both symbol sigmas of L are assumed countable (graphLanguage_countable_relations, with the graph language infrastructure); L need not be relational. This is not the unrestricted arbitrary-language endpoint. No derivation-level relationalization is attempted: consistency is hypothesised over the graph language, and the theorem is named for that hypothesis.

The translations

def FirstOrder.Language.relationalizeTagged {L : Language} : (n : ℕ) × L.BoundedFormulaω Empty n → (n : ℕ) × L.graphLanguage.BoundedFormulaω Empty n

The sigma-level relationalization.

Equations

• FirstOrder.Language.relationalizeTagged ⟨n, φ⟩ = ⟨n, FirstOrder.Language.relationalizeFormula φ⟩

def FirstOrder.Language.relationalizeTheory {L : Language} (T : L.Theoryω) : L.graphLanguage.Theoryω

The relationalized theory.

Equations

• FirstOrder.Language.relationalizeTheory T = FirstOrder.Language.relationalizeFormula '' T

Function support

def FirstOrder.Language.Fragment.functionSupport {L : Language} (F : L.Fragment) : Set ((n : ℕ) × L.Functions n)

The function symbols occurring in members of a fragment.

Equations

• F.functionSupport = ⋃ p ∈ F.toSet, p.snd.functionsIn

theorem FirstOrder.Language.Fragment.functionsIn_subset_functionSupport {L : Language} {F : L.Fragment} {n : ℕ} {φ : L.BoundedFormulaω Empty n} (h : ⟨n, φ⟩ ∈ F) : φ.functionsIn ⊆ F.functionSupport

theorem FirstOrder.Language.Fragment.functionSupport_countable {L : Language} {F : L.Fragment} (hF : F.toSet.Countable) : F.functionSupport.Countable

The graph fragment, universe and theory

noncomputable def FirstOrder.Language.Fragment.graphSeed {L : Language} (F : L.Fragment) (hF : F.toSet.Countable) : Set ((n : ℕ) × L.graphLanguage.BoundedFormulaω Empty n)

The seed of the graph fragment: the relationalized members and the graph axioms.

Equations

• F.graphSeed hF = FirstOrder.Language.relationalizeTagged '' F.toSet ∪ {⟨0, FirstOrder.Language.graphAxioms F.functionSupport⟩}

noncomputable def FirstOrder.Language.Fragment.graphFragment {L : Language} (F : L.Fragment) (hF : F.toSet.Countable) : L.graphLanguage.Fragment

The graph fragment: the Henkin closure of the seed, a fragment of graphLanguage L.

Equations

• F.graphFragment hF = FirstOrder.Language.Fragment.henkinClosure (F.graphSeed hF)

noncomputable def FirstOrder.Language.Fragment.graphUniverse {L : Language} (F : L.Fragment) (hF : F.toSet.Countable) : Set (L.graphLanguage.withConstants ℕ).Sentenceω

The graph universe: the constants-expanded universe of the graph fragment.

Equations

• F.graphUniverse hF = (F.graphFragment hF).withNatConstantsSentences

noncomputable def FirstOrder.Language.Fragment.graphTheory {L : Language} (F : L.Fragment) (hF : F.toSet.Countable) (T : L.Theoryω) : (L.graphLanguage.withConstants ℕ).Theoryω

The graph theory of T: the relationalized theory with the graph axioms of the support, mapped into the constants expansion.

Equations

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

Connecting facts

theorem FirstOrder.Language.Fragment.graphSeed_countable {L : Language} {F : L.Fragment} (hF : F.toSet.Countable) : (F.graphSeed hF).Countable

theorem FirstOrder.Language.Fragment.graphFragment_countable {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] {F : L.Fragment} (hF : F.toSet.Countable) : (F.graphFragment hF).toSet.Countable

The graph fragment is countable when both symbol sigmas are.

theorem FirstOrder.Language.Fragment.henkinClosed_graphUniverse {L : Language} (F : L.Fragment) (hF : F.toSet.Countable) : HenkinClosed (F.graphUniverse hF)

The graph universe satisfies the closure interface.

theorem FirstOrder.Language.Fragment.relationalizeTheory_union_axioms_subset_sentenceSlice {L : Language} {F : L.Fragment} (hF : F.toSet.Countable) {T : L.Theoryω} (hT : T ⊆ F.sentenceSlice) : relationalizeTheory T ∪ {graphAxioms F.functionSupport} ⊆ (F.graphFragment hF).sentenceSlice

The relationalized theory and the graph axioms lie in the graph fragment's sentence slice.

theorem FirstOrder.Language.Fragment.graphUniverse_countable {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] {F : L.Fragment} (hF : F.toSet.Countable) : (F.graphUniverse hF).Countable

The graph universe is countable when both symbol sigmas are.

theorem FirstOrder.Language.Fragment.graphTheory_subset_graphUniverse {L : Language} {F : L.Fragment} (hF : F.toSet.Countable) {T : L.Theoryω} (hT : T ⊆ F.sentenceSlice) : F.graphTheory hF T ⊆ F.graphUniverse hF

The graph theory lies in the graph universe.

theorem FirstOrder.Language.Fragment.functionsIn_subset_functionSupport_of_mem_sentenceSlice {L : Language} {F : L.Fragment} {T : L.Theoryω} (hT : T ⊆ F.sentenceSlice) {φ : L.Sentenceω} (hφ : φ ∈ T) : BoundedFormulaω.functionsIn φ ⊆ F.functionSupport

Every source sentence's function support lies in the support covered by the graph axioms.

The endpoint

theorem FirstOrder.Language.Fragment.exists_countable_model_of_aconsistent_graphUniverse {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] {F : L.Fragment} (hF : F.toSet.Countable) {T : L.Theoryω} (hT : T ⊆ F.sentenceSlice) (hcons : AConsistent (F.graphUniverse hF) (F.graphTheory hF T)) : ∃ (M : Type) (x : L.Structure M) (_ : Nonempty M) (_ : Countable M), T.Model M

Countable model existence over the graph universe (countable signature, not necessarily relational). A theory inside a countable fragment whose graph theory is AConsistent in the graph universe has a countable model, as an L-structure: the kernel runs over the relational graph language, the constants are forgotten, and the source structure is reconstructed from the graph model through the graph axioms. The theorem is named for its hypothesis; no consistency is transported across relationalization.