Foundation Bool From Logic Eq Iff To Bool Eq

The two-sided cut

A distinction is a cut with two sides and nothing else. Think of a single line drawn on a page: everything is either on one side or the other, with no third option. The Recognition Science framework builds its account of logic from this primitive act of distinguishing. It calls the two bare outcomes affirm (this side) and deny (the other side), and it treats them as carrying no numeric or semantic content beyond being the two sides of one cut.

The framework's machine-checked library of formal theorems proves that this two-sided structure is exactly the familiar Boolean structure. The declaration eq_iff_toBool_eq states the central fact: two sides of a distinction are the same side if and only if they map to the same Boolean value. The proof is short and constructive. If the sides are equal, applying the translation function to both sides gives equal Booleans. Conversely, if the two Booleans are equal, applying the inverse translation to both sides recovers the original sides, which must then be equal.

This is not a loose analogy. The library defines a translation from the two sides to the standard Boolean type (true for affirm, false for deny), and an inverse translation back. It then proves both round-trips: translating to Boolean and back returns the original side, and translating from Boolean and back returns the original Boolean. Together these establish a full equivalence between the two-sided structure and the Boolean type. The framework also proves that the usual logical operations on its two sides, negation, conjunction, and disjunction, behave exactly like their Boolean counterparts under this translation.

What the declaration does not claim is just as important. It does not claim that the two sides are numbers, or that they carry any quantitative content. It does not claim that the act of distinguishing is itself a physical process. It does not claim that this equivalence is the only way to build Boolean logic. It establishes a structural fact about a primitive distinction: its two sides are exactly the two Boolean values, nothing more and nothing less.

/-- Transfer principle: an equation in `LogicBool` holds iff it holds
under `toBool`. -/
theorem eq_iff_toBool_eq {a b : LogicBool} : a = b ↔ toBool a = toBool b := by
  constructor
  · exact congrArg toBool
  · intro h
    have := congrArg fromBool h
    rwa [fromBool_toBool, fromBool_toBool] at this

theorem fromBool_toBool : ∀ a : LogicBool, fromBool (toBool a) = a := by
  intro a; cases a <;> rfl

theorem toBool_fromBool : ∀ b : Bool, toBool (fromBool b) = b := by
  intro b; cases b <;> rfl

/-- **Recovery (negation)**: the swap of sides is Boolean `not`. -/
theorem toBool_not (a : LogicBool) : toBool (lnot a) = !(toBool a) := by
  cases a <;> rfl

/-- **Recovery (conjunction)**: the meet is Boolean `and`. -/
theorem toBool_and (a b : LogicBool) :
    toBool (land a b) = (toBool a && toBool b) := by
  cases a <;> cases b <;> rfl

/-- **Recovery (disjunction)**: the join is Boolean `or`. -/
theorem toBool_or (a b : LogicBool) :
    toBool (lor a b) = (toBool a || toBool b) := by
  cases a <;> cases b <;> rfl

What this page does not claim

The two sides carry no numeric content; the theorem does not assign numbers to affirm and deny. The theorem does not claim that the act of distinguishing is a physical process. The equivalence does not claim to be the only way to construct Boolean logic.

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/BoolFromLogic.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: