required

formal source

  93/-- A linearly ordered field is **Logic-supported** when a comparison
  94operator on it satisfies the four Aristotelian conditions plus scale
  95invariance and distinguishability. We package the ordered-field
  96structure required to even *state* these conditions. -/
  97structure LogicSupported (K : Type*) [Mul K] [Zero K] [One K] [LT K] where
  98  zero_lt_one_in_K : (0 : K) < 1
  99  C : ComparisonOperatorOn K
 100  identity : IdentityOn C
 101  non_contradiction : NonContradictionOn C
 102  scale_invariant : ScaleInvariantOn C
 103  distinguishability : DistinguishabilityOn C
 104
 105/-- **Bootstrap theorem (named-hypothesis form)**: a linearly ordered
 106field on which the Law of Logic is supported and which is Archimedean
 107and conditionally complete is canonically isomorphic to `ℝ` as an
 108ordered field. The Archimedean and conditional-completeness
 109hypotheses are the analytic content the Law of Logic does not on its
 110own provide; they are named here as inputs.
 111
 112The conclusion is the existence of an order-preserving ring
 113isomorphism with `ℝ`. -/
 114theorem bootstrap_to_real
 115    (K : Type*) [ConditionallyCompleteLinearOrderedField K]
 116    (_ : LogicSupported K) :
 117    Nonempty (K ≃+*o ℝ) :=
 118  ⟨LinearOrderedField.inducedOrderRingIso K ℝ⟩
 119
 120/-- **Idempotence**: `ℝ` itself is a Logic-supported domain (witnessed
 121by any of the comparison operators we already have over `ℝ`). The
 122bootstrap theorem then says nothing new on `ℝ`, but on any other
 123candidate ordered field it forces an isomorphism to `ℝ`. -/
 124def real_supports_logic
 125    (C : LogicAsFunctionalEquation.ComparisonOperator)
 126    (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C) :