Foundation Bool From Logic To Bool And

The Boolean translation

Boolean logic is the algebra of true and false, the two truth values that underpin computer circuits and mathematical proof. Its basic operations are AND, OR, and NOT: AND returns true only when both inputs are true, OR returns true when at least one input is true, and NOT flips a value. These operations obey a small set of laws, such as AND being commutative and distributive, that together define a Boolean algebra.

In the Recognition Science framework, the starting point is not a set of truth values but a primitive act of distinguishing. A distinction δ has two sides and nothing else: call them affirm and deny. These are the two bare outcomes of making a cut; they carry no numeric content, only the sense of "this side" and "the other side". The framework's ledger, a discrete record of events, begins with such two-sided distinctions.

The framework then shows that this two-sided structure is exactly the Boolean structure. The declaration toBool_and establishes that the framework's AND operation, defined on the two sides of a distinction, translates faithfully to the standard Boolean AND: when the two sides are mapped to true and false, the framework's AND returns true exactly when both inputs are true. The same translation holds for OR and NOT. The two-sided distinction is therefore not merely analogous to Boolean logic; it is a model of it.

The framework proves this translation is a genuine equivalence, not a loose correspondence. The mapping from the two sides to true and false has an inverse, and the two mappings undo each other perfectly. Equality of two sides is the same as equality of their Boolean translations. The framework also rejects two decoy mappings: a constant map that sends every side to true fails to distinguish the two sides, and a swapped map that exchanges true and false fails to preserve AND. Only the faithful translation survives.

The framework's library, a machine-checked collection of formal theorems, verifies these results. What the declaration does not claim is that this translation introduces new logical content. The two sides of a distinction carry no numeric or semantic weight beyond being two distinct outcomes. The framework derives Boolean structure from the mere act of distinguishing, not from any prior assumption about truth values.

/-- **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 theorem (carrier)**: `LogicBool` and `Bool` are in
bijection. The two sides of a single distinction are exactly the two
Boolean values. -/
def equivBool : LogicBool ≃ Bool where
  toFun := toBool
  invFun := fromBool
  left_inv := fromBool_toBool
  right_inv := toBool_fromBool

/-- **Decoy 2 (constant reading rejected)**: the constant-`true` map
collapses both sides of the distinction, so it is not injective and
cannot underlie an equivalence with `Bool`. -/
theorem decoy_constant_bool_map_rejected :
    ¬ Function.Injective (fun _ : LogicBool => true) := by
  intro h
  exact affirm_ne_deny (h rfl)

/-- **Decoy 1 (swapped reading rejected)**: reading `affirm` as `false`
does not turn the meet into Boolean `and`. On the pair `(affirm, deny)`
the meet is `deny` (swapped ↦ `true`), while `false && true = false`.
So the swapped map is not a conjunction homomorphism. -/
theorem decoy_swapped_bool_map_rejected :
    ¬ (∀ a b : LogicBool,
        swappedMap (land a b) = (swappedMap a && swappedMap b)) := by
  intro h
  exact absurd (h affirm deny) (by decide)

What this page does not claim

The declaration does not claim that the two sides of a distinction carry any numeric content. The declaration does not claim to derive Boolean logic from nothing; it starts from the primitive act of distinguishing. The declaration does not claim that the framework's AND operation is the only possible translation, only that it is the faithful one.

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: