ExcludedMiddle
plain-language theorem explainer
A comparison operator on positive reals satisfies excluded middle when its uncurried map is continuous on the open positive quadrant. Researchers deriving the functional equation for logic from Aristotelian laws cite this definition to enforce that every comparison returns a definite real cost with continuous dependence on inputs. The definition is a direct encoding of joint continuity on the domain of positive ratios.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. Then $C$ satisfies excluded middle if $C$ is continuous on $(0,∞) × (0,∞)$.
background
In the LogicAsFunctionalEquation setting a ComparisonOperator is a map from pairs of positive reals to reals that records the cost of comparing two quantities. Scale invariance reduces the two-argument map to a one-argument cost on positive ratios, allowing the four Aristotelian constraints to be stated as functional equations on the multiplicative group ℝ₊. The excluded-middle clause supplies the totality and continuity half of those constraints.
proof idea
The definition is the direct statement that the uncurried comparison function is continuous on the positive quadrant.
why it matters
ExcludedMiddle is one of the five fields of the SatisfiesLawsOfLogic structure and of its continuous counterpart SatisfiesLawsOfLogicContinuous. It supplies the translation lemma that converts the Aristotelian law A ∨ ¬A into joint continuity of the cost map, which is then used to derive the J-functional equation and the reciprocity property. The definition therefore closes the bridge from discrete logic to the continuous multiplicative setting that Recognition Science employs for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.