`universalGround`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.MetaphysicalRealization on GitHub at line 34.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  31
  32/-- The universal forcing theorem supplies a canonical metaphysical-ground
  33structure in the neutral, structural sense. -/
  34noncomputable def universalGround : MetaphysicalGround where
  35  sourceName := "Universal generator of distinguishability"
  36  identifies_arithmetic := fun R => R.orbitEquivLogicNat
  37  invariant := fun R S => ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
  38
  39/-- The metaphysical-ground identification is unique up to the same canonical
  40arithmetic equivalence supplied by Universal Forcing. -/
  41noncomputable def metaphysical_ground_unique (R : LogicRealization) :
  42    (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  43  R.orbitEquivLogicNat
  44
  45end MetaphysicalRealization
  46end UniversalForcing
  47end Foundation
  48end IndisputableMonolith

papers checked against this theorem

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