Documentation

InfinitaryLogic.Methods.WellOrdering.Constants

Constant coding for the undefinability of well-ordering (issue #12, commit 1) #

The L[[ℕ]] kernel indexes its constants by ℕ. Marker's construction needs two disjoint countable families — the rational constants d_q (q : ℚ) carrying the positive order diagram, and the Henkin constants c_n consumed by the fair enumeration's witness requests. Per the frozen audit (D3): rationals at 2 * Encodable.encode q, Henkin constants at 2 * n + 1 — parity keeps the families disjoint without choosing an arbitrary ℚ ≃ ℕ.

This commit is the coding layer only: the two index functions, their injectivity, their disjointness, and the term/sentence-level wrappers over the kernel's constTerm/constTermS.

source
def FirstOrder.Language.ratConstIdx (q : ℚ) :
ℕ

The kernel index of the rational constant d_q.

Equations
Instances For
    source
    def FirstOrder.Language.henkinConstIdx (n : ℕ) :
    ℕ

    The kernel index of the n-th Henkin constant.

    Equations
    Instances For
      source
      theorem FirstOrder.Language.ratConstIdx_injective :
      Function.Injective ratConstIdx
      source
      theorem FirstOrder.Language.henkinConstIdx_injective :
      Function.Injective henkinConstIdx
      source
      theorem FirstOrder.Language.ratConstIdx_ne_henkinConstIdx (q : ℚ) (n : ℕ) :
      ratConstIdx q ≠ henkinConstIdx n

      The two constant families are disjoint (even vs odd indices).

      source
      def FirstOrder.Language.ratConstTerm {L : Language} (q : ℚ) :
      (L.withConstants ℕ).Term Empty

      The rational constant d_q as a closed L[[ℕ]]-term.

      Equations
      Instances For
        source
        def FirstOrder.Language.ratConstTermS {L : Language} (q : ℚ) :
        (L.withConstants ℕ).Term (Empty ⊕ Fin 0)

        The rational constant d_q in the sentence-term context.

        Equations
        Instances For
          source
          @[simp]
          theorem FirstOrder.Language.ratConstTerm_relabel_inl {L : Language} (q : ℚ) :
          Term.relabel Sum.inl (ratConstTerm q) = ratConstTermS q