`_ethics_ok`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit
domain: Foundation
line: 78 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit on GitHub at line 78.

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

  75      ≃ ArithmeticFromLogic.LogicNat :=
  76  (StrictLogicRealization.toLightweight strictNarrativeRealization).orbitEquivLogicNat
  77
  78def _ethics_ok :
  79    (StrictLogicRealization.arith strictEthicsRealization).peano.carrier
  80      ≃ ArithmeticFromLogic.LogicNat :=
  81  (StrictLogicRealization.toLightweight strictEthicsRealization).orbitEquivLogicNat
  82
  83/-! ## Strict metaphysical package -/
  84
  85noncomputable example (R : StrictLogicRealization) :
  86    (StrictLogicRealization.arith R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  87  (StrictLogicRealization.toLightweight R).orbitEquivLogicNat
  88-- #print axioms Metaphysical.strict_metaphysical_ground_unique
  89--   propext, Quot.sound
  90
  91end AxiomAudit
  92end Strict
  93end UniversalForcing
  94end Foundation
  95end IndisputableMonolith

papers checked against this theorem

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