`arithmeticOf`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing
domain: Foundation
line: 17 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing on GitHub at line 17.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  14namespace UniversalForcing
  15
  16/-- The forced arithmetic object of a realization. -/
  17def arithmeticOf (R : LogicRealization) : ArithmeticOf R :=
  18  ArithmeticOf.extracted R
  19
  20/-- **Universal Forcing, first theorem form.**
  21
  22For any two Law-of-Logic realizations, the arithmetic objects extracted from
  23them are canonically equivalent. In this first formal spine the equivalence is
  24the unique equivalence between initial Peano algebras. Later realization
  25modules enrich the interpretation map from each carrier into this invariant
  26arithmetic object. This definition now uses the realization's own internal
  27orbit, not the reference `LogicNat` object. -/
  28noncomputable def arithmetic_invariant
  29    (R S : LogicRealization) :
  30    (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
  31  ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
  32
  33/-- The forced arithmetic of every realization is canonically equivalent to
  34the reference `LogicNat` Peano object. This is the simplest form of the
  35Universal Forcing theorem. -/
  36noncomputable def arith_universal_initial (R : LogicRealization) :
  37    (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  38  R.orbitEquivLogicNat
  39
  40/-- **Universal Forcing Meta-Theorem, abstract spine.**
  41
  42Any two Law-of-Logic realizations have canonically equivalent forced
  43arithmetic objects. -/
  44noncomputable def universal_forcing (R S : LogicRealization) :
  45    (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
  46  ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
  47

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.