LogicSupported
LogicSupported packages the minimal ordered-field data and comparison-operator axioms needed to state the Law of Logic on an arbitrary linearly ordered field K. Researchers deriving the reals from logic axioms cite it to isolate the Aristotelian conditions plus scale invariance and distinguishability from the separate Archimedean and completeness hypotheses. The declaration is a plain structure definition that simply bundles the field instances, the operator, and the four required properties with no further proof steps.
claimA linearly ordered field $K$ is Logic-supported when $0<1$ holds in $K$, a comparison operator $C:K→K→K$ exists, and $C$ satisfies: identity ($C(x,x)=0$ for all $x>0$), non-contradiction ($C(x,y)=C(y,x)$ for all $x,y>0$), scale invariance ($C(λx,λy)=C(x,y)$ for all $x,y,λ>0$), and distinguishability (there exist $x,y>0$ with $C(x,y)≠0$).
background
The module DomainBootstrap isolates the comparison-operator domain that carries the Law of Logic. A comparison operator is simply any map $C:K→K→K$ on a linearly ordered field; the four Aristotelian conditions are then expressed as the predicates IdentityOn, NonContradictionOn, ScaleInvariantOn and DistinguishabilityOn (all defined in the same file). These predicates are the generic-field versions of the functional equation studied in LogicAsFunctionalEquation. The module doc states that the Law of Logic on an ambient field plus Archimedean and Dedekind-completeness forces that field to be canonically isomorphic to ℝ; LogicSupported is the packaging that makes the Law-of-Logic hypotheses explicit while leaving the analytic hypotheses named separately.
proof idea
The declaration is a structure definition whose fields are exactly the required instances and predicates; no tactics or lemmas are applied. It is a one-line wrapper that collects zero_lt_one_in_K together with the four named predicates on the comparison operator C.
why it matters in Recognition Science
LogicSupported supplies the hypothesis for the bootstrap theorems bootstrap_to_real and bootstrap_closure, which conclude that any such K is order-isomorphic to ℝ. The module doc identifies this as the step that closes the chicken-and-egg loop between the Law of Logic and the recovered real line. It therefore sits at the interface between the functional-equation formulation of logic and the classical characterization of ℝ as the unique Archimedean conditionally complete ordered field.
scope and limits
- Does not assert that any concrete field satisfies the packaged conditions.
- Does not include Archimedean or conditional-completeness hypotheses.
- Does not construct or exhibit the order-isomorphism to ℝ.
- Does not derive the comparison operator from the functional equation; it only packages the required properties.
Lean usage
theorem example (K : Type*) [ConditionallyCompleteLinearOrderedField K] (h : LogicSupported K) : Nonempty (K ≃+*o ℝ) := bootstrap_to_real K hformal statement (Lean)
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 `ℝ`. -/