`metaphysical_ground_unique`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

  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.