SatisfiesLawsOfLogic
plain-language theorem explainer
The structure packages the six axioms that a comparison operator on positive reals must obey to encode Aristotelian logic as constraints on a cost function. Researchers deriving arithmetic from functional equations or bootstrapping ordered fields cite it as the central hypothesis that closes the logic-to-arithmetic chain. The declaration is introduced directly as a structure whose six fields are the translated Aristotelian laws plus scale invariance and non-triviality.
Claim. Let $C: (0,∞)×(0,∞)→ℝ$ be a comparison operator. Then $C$ satisfies the laws of logic when it obeys identity ($C(x,x)=0$ for all $x>0$), non-contradiction ($C(x,y)=C(y,x)$), excluded middle (continuity of the uncurried map on positive pairs), scale invariance ($C(λx,λy)=C(x,y)$ for $λ>0$), route independence (the d'Alembert relation $F(xy)+F(x/y)=P(F(x),F(y))$ for a symmetric quadratic polynomial $P$), and non-triviality (there exists $x>0$ with $F(x)≠0$), where $F$ is the derived cost $F(r):=C(r,1)$.
background
A comparison operator is any map $C:(0,∞)×(0,∞)→ℝ$ that returns a real cost for comparing two positive quantities. The derived cost function is obtained by fixing the second argument at the multiplicative identity, producing a function on positive ratios; scale invariance makes this reduction well-defined. The six component properties are identity (zero self-cost), non-contradiction (swap symmetry), excluded middle (continuity on the positive quadrant), scale invariance (ratio-only dependence), route independence (the symmetric d'Alembert composition equals a quadratic polynomial in the individual costs), and non-triviality (the cost is not identically zero).
proof idea
The declaration is the direct packaging of the six named properties into a single Prop; each field is simply the corresponding sibling definition (Identity, NonContradiction, ExcludedMiddle, ScaleInvariant, RouteIndependence, NonTrivial) applied to the given comparison operator. No further lemmas or tactics are invoked.
why it matters
This structure supplies the central hypothesis for the logic-to-arithmetic derivation. It is used to extract an explicit non-trivial generator in ArithmeticFromLogic.generatorOfLawsOfLogic and to witness that the reals support logic in DomainBootstrap.real_supports_logic. In the Recognition framework it translates the Aristotelian laws into the functional-equation setting that forces the J-cost, the Recognition Composition Law, and the subsequent phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 30 of 55)
-
Regularization lifts zero-shot translation by 2.23 BLEU
"We achieve an average improvement of 2.23 BLEU points across 12 language pairs... by designing regularization methods into the standard Transformer model"
-
Entropy maximization plus diffusion yields quantum interference
"the transition probability P(x'|x) ... obtained by maximizing the relative entropy S[P,Q]"
-
Particle paths vary continuously from fluctuating to smooth
"Entropic Dynamics allows for a more generalized sub-quantum dynamics which includes the (NSM) and (BM) limits as special cases."
-
Logic layers let neural nets learn rules and arithmetic
"stacking NLRL layers yields arbitrary CNF/DNF; end-to-end trainable via sigmoid-constrained weights"
-
Between and neighbour predicates characterize reversible languages
"Theorem 15. The syntactic ⋆-semigroup … satisfies exe⋆ = ex⋆e⋆ …"
-
Explicit solutions derived for Levi-Civita equation on monoids
"solutions are abelian except when they blatantly need not be … elementary algebraic manipulations"
-
Sparse autoencoders extract more monosemantic features from language models
"sparse autoencoders to reconstruct the internal activations ... sets of sparsely activating features that are more interpretable and monosemantic"
-
Collision models derive quantum theory and speed bounds
"Our first principle is that every reversible dynamics is implementable through a collision model, i.e. a sequence of fast collisions with an array of identically prepared systems."
-
Diffusion models run evolutionary algorithms via denoising
"xhat0(xt, alpha, t) = 1/Z sum g[f(x)] N(xt; sqrt(alpha t) x, 1-alpha t) x ... sigma t w (mutation term)"
-
Hawkes processes converge to generalized Feller random measures
"Mξ[f] = exp(h[f] ∗ μ) where h solves the convolutional Riccati equation"
-
Neural equilibrium learning beats large models on conservation laws
"f eq = arg min {H(f) : ⟨(1,v,½v·v) f⟩ = (ρ,ρu,ρE)} ... Maxwell–Boltzmann form"
-
High-variance questions boost LLM reasoning training
"expected policy improvement increases with the variance of the final reward, i.e. learnability"
-
Prediction consistency ranks segmentation models without labels
"CTE-NHD = 1 − |{ỹ ≠ ŷ} ∩ (ỹ ∪ ŷ)| / |ỹ ∪ ŷ| (normalised Hamming distance, per-class weighted)"
-
Symmetrized cross-entropy produces unique convex multi-class unhinged loss
"The multi-class unhinged loss is the unique convex, non-trivial, non-increasing, multi-class symmetric loss function satisfying the property of invariance to permutations (up to an additive and a multiplicative constant)."
-
Simple feedback law optimizes albatross soaring in real time
"ESC is a model-free adaptive control strategy which steers the dynamics toward the extremum (maximum/minimum) of an objective function"
-
Poisoned memories steer LLM agents across sessions
"We propose and study sleeper memory poisoning, a delayed attack in which an adversary manipulates external context... to cause the assistant to store a fabricated memory about the user."
-
Sensorimotor rules alone produce collective animal motion
"AICON generates behavior through the dynamic composition of sensorimotor regularities, without directly encoding behavior itself"
-
Logicality-focused training raises LLM physics reasoning performance
"We extract scientific problems from academic literature and sample a high-quality dataset exhibiting strong logicality... two SFT data sampling methods, based on distillation and reasoning style transfer."
-
Refined superposition finds programs if computable ones exist
"We prove completeness in the following sense: if at least one computable program satisfying the given specification exists, we show that the modified calculus finds one."
-
Exponential-log measure keeps dynamic range in drug binding curves
"The logarithmic component corresponds to a thermodynamic term ... exponential component is represented through an inverse normalized concentration term"
-
New model architecture wires concept relationships straight into predictions
"CREAM architecturally embeds (bi)directed concept-concept, and concept to task relationships specified by a human expert, while severing undesired information flows... using StrNN binary masks"
-
Conditions derived for embedding agents' languages into one shared state space
"We define translation operators between two languages which provide a 'best approximation' for the meaning of propositions in the target language subject to its expressive power. ... derive necessary and sufficient conditions for the existence of a joint state space and a joint language"
-
k-automatic sets split into two definability classes in Presburger arithmetic
"Fact 2.15 (Büchi–Bruyère): X k-automatic iff definable in (N,+,Vk)"
-
Extra modalities aid reasoning only via independent paths
"We address this gap through a logic-grounded evaluation framework that categorizes multimodal reasoning into six interaction patterns, varying how facts are distributed across modalities and logically combined."
-
LLMs align validity and plausibility linearly, mixing the two in reasoning
"we construct debiasing vectors that disentangle these concepts"
-
Reverse-policy swap lifts VLM accuracy on rare prompts 14x
"abductive policy eπ(x|y) = π(y|x)p(x)/q(y)"
-
20% of high-entropy tokens drive most VLM attack damage
"token entropy is thus defined as H_t(p_t(w)) = −∑ p_t(w) log p_t(w)"
-
Language tasks mixed into pre-training lift linguistic scores
"L2T transforms raw text into structured input-output pairs to provide explicit linguistic stimulation... Pre-training LMs on a mixture of raw text and L2T data... improves... linguistic competence benchmarks"
-
Logical reward during fine-tuning removes contradictory weather answers
"RLoCo = 1 iff fa_rp = fa and RFormat = 1 (Eq. 2); Self-Contra proportion drops from ~30% (RFT) to ~2% (LoCo-RFT)"
-
RAG models score 93% on facts but 35% on logical coherence
"Grounded in Horn Rules, our approach integrates a backward verification mechanism to systematically evaluate three key reasoning dimensions: Completeness, Conciseness, and Determinateness."