Documentation

InfinitaryLogic.Admissible.Barwise.HenkinClosure

The Henkin closure of a set of formulas #

The producer side of the source-fragment adapter (issue #19): a closure operator that turns any set of formulas into a fragment with a Fragment.HenkinBasis, so that the v4.5.0 endpoint Fragment.exists_countable_model_of_aconsistent_withConstants applies without supplying the basis by hand.

henkinBasisSeed L   -- falsum, the equality template, every relation template
henkinClosure S     := negationClosure (S ∪ henkinBasisSeed L)

Fragment.negationClosure (generic, Lomega1omega/NegationClosure.lean) supplies component and negation closure; the seed supplies the atoms. Countability needs the relation-symbol sigma countable in addition to S, because the seed contains one template per symbol. The exact HF regression henkinClosure (hfFragment L).toSet = hfFragment L fixes the operator on the finitary fragment.

The construction is purely syntactic externally. Admissibility enters only when internalizing that construction and showing its codes remain inside the admissible language. No fragment structure gains a field.

The seed #

source
def FirstOrder.Language.Fragment.henkinBasisSeed (L : Language) :
Set ((n : ℕ) × L.BoundedFormulaω Empty n)

The Henkin basis seed: falsum, the equality template at arity two, and the relation template of every symbol at its arity.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem FirstOrder.Language.Fragment.henkinBasisSeed_countable {L : Language} [Countable ((l : ℕ) × L.Relations l)] :
    (henkinBasisSeed L).Countable
    source
    theorem FirstOrder.Language.Fragment.henkinBasisSeed_subset {L : Language} {A : L.Fragment} (hB : A.HenkinBasis) :
    henkinBasisSeed L ⊆ A.toSet

    A fragment with a Henkin basis contains the seed.

    The closure #

    source
    def FirstOrder.Language.Fragment.henkinClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) :
    L.Fragment

    The Henkin closure: the negation closure of S together with the seed.

    Equations
    Instances For
      source
      theorem FirstOrder.Language.Fragment.subset_henkinClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) :
      S ⊆ (henkinClosure S).toSet
      source
      theorem FirstOrder.Language.Fragment.generated_le_henkinClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) :
      generated S ≤ henkinClosure S
      source
      theorem FirstOrder.Language.Fragment.negationClosed_henkinClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) :
      (henkinClosure S).NegationClosed
      source
      theorem FirstOrder.Language.Fragment.henkinBasis_henkinClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) :
      (henkinClosure S).HenkinBasis

      The closure has a Henkin basis.

      source
      theorem FirstOrder.Language.Fragment.henkinClosure_le {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {A : L.Fragment} (hSA : S ⊆ A.toSet) (hB : A.HenkinBasis) :
      (henkinClosure S).toSet ⊆ A.toSet

      The Henkin closure is below every fragment with a basis containing S.

      source
      theorem FirstOrder.Language.Fragment.henkinClosure_toSet_eq {L : Language} {A : L.Fragment} (hB : A.HenkinBasis) :
      henkinClosure A.toSet = A

      A fragment with a basis is its own Henkin closure.

      source
      theorem FirstOrder.Language.Fragment.henkinClosure_countable {L : Language} [Countable ((l : ℕ) × L.Relations l)] {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (hS : S.Countable) :
      (henkinClosure S).toSet.Countable

      Countability: the seed contributes one template per relation symbol.

      source
      theorem FirstOrder.Language.Fragment.henkinClosure_hfFragment {L : Language} :
      henkinClosure L.hfFragment.toSet = L.hfFragment

      The HF regression, exact: the finitary fragment is its own Henkin closure.

      The endpoint with the basis discharged #

      source
      theorem FirstOrder.Language.Fragment.henkinClosed_withNatConstantsSentences_henkinClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) :
      HenkinClosed (henkinClosure S).withNatConstantsSentences

      The constants-expanded universe of a Henkin closure is Henkin-closed.

      source
      theorem FirstOrder.Language.Fragment.exists_countable_model_of_aconsistent_henkinClosure {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (hS : S.Countable) {T : L.Theoryω} (hT : T ⊆ (henkinClosure S).sentenceSlice) (hcons : AConsistent (henkinClosure S).withNatConstantsSentences (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' T)) :
      ∃ (M : Type) (x : L.Structure M) (_ : Nonempty M) (_ : Countable M), T.Model M

      Countable model existence over the Henkin closure of a countable set. The v4.5.0 source-fragment endpoint with the basis discharged by the closure. The consistency hypothesis is over the constants-expanded universe of the full closure, a larger permission set than the minimal interface HenkinClosedMin needs: the closure conveniently produces full closure, and the weaker interface permits weaker evidence, but nothing here transports consistency from a smaller universe to this one.