universal_forcing

formal source

  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
  48/-- The continuous positive-ratio realization has the same forced arithmetic
  49as every other realization. -/
  50noncomputable def continuous_positive_ratio_arithmetic_invariant
  51    (C : LogicAsFunctionalEquation.ComparisonOperator)
  52    (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C)
  53    (S : LogicRealization.{0, 0}) :
  54    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)).peano.carrier
  55      ≃ (arithmeticOf S).peano.carrier :=
  56  ArithmeticOf.equivOfInitial
  57    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)) (arithmeticOf S)
  58
  59/-- The Peano surface is available for the forced arithmetic of every
  60realization. -/
  61theorem peano_surface (R : LogicRealization) :
  62    ArithmeticOf.PeanoSurface (arithmeticOf R) :=
  63  ArithmeticOf.extracted_peanoSurface R
  64
  65end UniversalForcing
  66end Foundation
  67end IndisputableMonolith