Foundation Logic From Cost

Logic from Cost

In Recognition Science, recognition events carry a forced cost, and the central result is the unique cost function J(x) = (x + 1/x)/2 - 1. This module, LogicFromCost, applies that framework to propositions themselves. A proposition is modeled as a configuration with a positive ratio, and its cost is the defect of that ratio. A proposition is stable when its cost is zero, which happens exactly when its ratio equals 1.

The key theorems establish that consistency is the cheap state. A consistent configuration can achieve zero cost, and any consistent configuration has non-negative cost, with zero cost exactly when the ratio is 1. A contradiction, modeled as a configuration where both P and not-P have ratio 1, cannot have zero total cost; it either has positive cost or sits at the singular point where both ratios are 1. The theorem logic_from_cost_summary packages these facts: consistency can be free, contradictions are costly or singular, and nothing has infinite cost while ratio 1 has zero cost.

The module also shows that the stable states of a pre-logical cost structure form a Boolean algebra, with bitwise AND, OR, and NOT operations matching the classical truth tables. This is the structural analogy: the cost function's minima behave like logical consistency. The philosophical thesis that logic emerges from cost is precisely this, not a claim to derive classical logic itself, which would be circular. The proofs use the ambient classical logic of the formal system as the metalanguage.

THEOREM logic_from_cost_summary · IndisputableMonolith/Foundation/LogicFromCost.lean

THEOREM logic_from_cost_summary · IndisputableMonolith/Foundation/LogicFromCost.lean

THEOREM prelogical_boolean_fragment · IndisputableMonolith/Foundation/LogicFromCost.lean

What this page does not claim

This module does not derive classical logic itself; it uses the ambient classical logic of the formal system as the metalanguage. No claim is made that the philosophical thesis 'logic emerges from cost' is a proof of the nature of logic, only a structural analogy. The module does not connect these logical structures to the empirical predictions of particle masses or the fine-structure constant.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/LogicFromCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: