Encyclopedia Foundation Foundation Logic From Cost Mp From Cost And Logic

ARTICLE 4 claims 4 theorems

Foundation Logic From Cost Mp From Cost And Logic

A machine-checked theorem shows that in one formal model, contradictions carry positive cost, while consistent statements can be free.

Verify this page

The cost of contradiction

In classical logic, a contradiction is a statement that cannot be true. The Recognition Science framework asks what happens when truth is not assumed but earned: a proposition is assigned a cost, a number measuring how hard it is to maintain that proposition as a stable configuration. The framework's central theorem, mp_from_cost_and_logic, proves three facts about this cost structure: nothing has infinite cost, a contradiction cannot have zero total cost, and at least one consistent statement does have zero cost.

The first fact, that nothing is infinitely expensive, is a statement about the cost function's behavior near zero. For any finite bound, there is a small enough positive ratio whose cost exceeds that bound. The second fact is the heart of the matter: a contradiction, defined as a configuration where both a proposition and its negation are asserted, cannot have zero total cost. The third fact provides the counterpoint: a consistent configuration, where a proposition is asserted without its negation, can achieve zero cost.

The declaration does not claim that classical logic itself is derived. The proof runs inside a classical metalanguage, using the ambient logic to reason about the object-level cost assignments. The philosophical thesis that logic emerges from cost is a structural analogy, not a derivation of logic from nothing. The theorem shows that within this formal model, cost-minimizing configurations behave like logically consistent ones.

What the theorem establishes is a precise correspondence: the cost structure has minima that mirror logical consistency, and contradictions are excluded from those minima. This is a bridge from the framework's cost-based foundations to the reality of logical structure, but it is a bridge built within an existing logical system, not a replacement for one.

THEOREM mp_from_cost_and_logic · IndisputableMonolith/Foundation/LogicFromCost.lean
mp_from_cost_and_logic · IndisputableMonolith/Foundation/LogicFromCost.lean:277 
/-- **MP FROM COST + LOGIC**

    The Meta-Principle "Nothing cannot recognize itself" now has
    two derivations:

    1. **Cost derivation**: J(0⁺) = ∞, so "nothing" is infinitely expensive
    2. **Logic derivation**: "Nothing exists" = contradiction, which is expensive

    Both derivations converge on the same conclusion:
    Existence (something rather than nothing) is the cost-minimizing state.

    This is the unification: cost and logic are the same structure.
    The cost landscape IS the logical landscape.
    What minimizes J IS what is logically consistent. -/
theorem mp_from_cost_and_logic :
    -- Nothing is infinitely expensive (cost derivation)
    (∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x) ∧
    -- Contradictions can't have zero total cost
    (∀ c : ContradictionConfig,
      contradiction_cost c > 0 ∨ IsLogicalContradiction c) ∧
    -- Something (ratio = 1) has zero cost
    defect 1 = 0 :=
  ⟨nothing_cannot_exist, contradiction_positive_cost, defect_at_one⟩
THEOREM mp_from_cost_and_logic · IndisputableMonolith/Foundation/LogicFromCost.lean
mp_from_cost_and_logic · IndisputableMonolith/Foundation/LogicFromCost.lean:277 
/-- **MP FROM COST + LOGIC**

    The Meta-Principle "Nothing cannot recognize itself" now has
    two derivations:

    1. **Cost derivation**: J(0⁺) = ∞, so "nothing" is infinitely expensive
    2. **Logic derivation**: "Nothing exists" = contradiction, which is expensive

    Both derivations converge on the same conclusion:
    Existence (something rather than nothing) is the cost-minimizing state.

    This is the unification: cost and logic are the same structure.
    The cost landscape IS the logical landscape.
    What minimizes J IS what is logically consistent. -/
theorem mp_from_cost_and_logic :
    -- Nothing is infinitely expensive (cost derivation)
    (∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x) ∧
    -- Contradictions can't have zero total cost
    (∀ c : ContradictionConfig,
      contradiction_cost c > 0 ∨ IsLogicalContradiction c) ∧
    -- Something (ratio = 1) has zero cost
    defect 1 = 0 :=
  ⟨nothing_cannot_exist, contradiction_positive_cost, defect_at_one⟩
THEOREM contradiction_positive_cost · IndisputableMonolith/Foundation/LogicFromCost.lean
contradiction_positive_cost · IndisputableMonolith/Foundation/LogicFromCost.lean:117 
/-- **THEOREM 1**: Contradictions cannot have zero total cost.

    If both P and ¬P are stable (cost 0), then both ratios must be 1.
    But complementary ratios with r * s = 1 have r = s = 1 only when
    both equal 1. And if P is true at ratio 1, ¬P cannot also be true.

    More fundamentally: the complementarity constraint r * (1/r) = 1
    means if defect(r) = 0 (so r = 1), then defect(1/r) = defect(1) = 0 too.
    But this is only possible if both assertions coexist at ratio 1,
    which is a logical contradiction. -/
theorem contradiction_positive_cost (c : ContradictionConfig) :
    contradiction_cost c > 0 ∨ (c.ratio_P = 1 ∧ c.ratio_notP = 1) := by
  by_cases h : c.ratio_P = 1
  · -- If ratio_P = 1, then ratio_notP = 1 (from complementarity)
    have hnotP : c.ratio_notP = 1 := by
      have := c.complementary
      rw [h] at this
      simp at this
      exact this
    right
    exact ⟨h, hnotP⟩
  · -- If ratio_P ≠ 1, then defect(ratio_P) > 0
    left
    unfold contradiction_cost
    -- defect(x) = 0 ↔ x = 1, so if x ≠ 1 and x > 0, defect(x) > 0
    have hdef_ne : defect c.ratio_P ≠ 0 := by
      intro heq
      have := (defect_zero_iff_one c.ratio_P_pos).mp heq
      exact h this
    have hdef_nonneg : defect c.ratio_P ≥ 0 := defect_nonneg c.ratio_P_pos
    have hdef : defect c.ratio_P > 0 := lt_of_le_of_ne hdef_nonneg (Ne.symm hdef_ne)
    linarith [defect_nonneg c.ratio_notP_pos]
THEOREM consistent_zero_cost_possible · IndisputableMonolith/Foundation/LogicFromCost.lean
consistent_zero_cost_possible · IndisputableMonolith/Foundation/LogicFromCost.lean:193 
/-- **THEOREM 4**: Consistent configurations can have zero cost.

    Unlike contradictions, a single proposition can stabilize at ratio = 1.
    This is the minimum-cost state for a proposition. -/
theorem consistent_zero_cost_possible :
    ∃ c : ConsistentConfig, consistent_cost c = 0 := by
  use ⟨True, 1, by norm_num⟩
  unfold consistent_cost
  exact defect_at_one

What this page does not claim

This theorem does not derive classical logic itself; it uses classical logic to prove a fact about cost-minimizing configurations. The theorem does not claim that all consistent statements are free, only that at least one is. The theorem does not establish that contradictions are impossible, only that they cannot have zero cost.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND