def
definition
def or abbrev
arithmeticOf
show as:
view Lean formalization →
formal statement (Lean)
17def arithmeticOf (R : LogicRealization) : ArithmeticOf R :=
proof body
Definition body.
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. -/
used by (32)
-
categorical_arithmetic_invariant -
bool_arithmetic_invariant -
bool_peano_surface -
modular_arithmetic_invariant -
ordered_arithmetic_invariant -
physics_arithmetic_invariant -
arithmetic_invariant -
arith_universal_initial -
continuous_positive_ratio_arithmetic_invariant -
peano_surface -
universal_forcing -
biology_arith_equiv_nat -
categorical_arith_equiv_logicNat -
continuous_arith_equiv_logicNat -
discrete_arith_equiv_logicNat -
ethics_arith_equiv_nat -
arith_continuous_equiv_arith_discrete -
arith_universal_initial' -
universal_forcing -
universal_peano_surface -
MetaphysicalGround -
metaphysical_ground_unique -
universalGround -
modular_arithmetic_invariant -
music_arith_equiv_nat -
narrative_arith_equiv_nat -
forcedArithmetic_isNNO -
order_arithmetic_invariant -
positiveRatio_strict_equiv_existing -
arith