Foundation Bool From Logic To Bool Not

The translation theorem

In classical logic, negation is the operation that flips a truth value: true becomes false, and false becomes true. The Recognition Science framework, in its ledger (a discrete record of events), builds a primitive two-sided structure called LogicBool with two constructors, affirm and deny, representing the two bare outcomes of a single distinction. The framework then defines a translation function, toBool, that maps affirm to the Boolean value true and deny to false.

The theorem toBool_not proves that this translation respects negation. If you take any LogicBool value, apply the logical negation operation lnot (which swaps affirm and deny), and then translate the result to Bool, you get the same answer as translating the original value first and then applying the standard Boolean NOT operation. In symbols: toBool (lnot a) = !(toBool a). The proof is by case analysis on the two possible values of a, and each case reduces to a definitional equality.

This is one of several translation theorems in the same file. The framework also proves that the translation is a bijection (a perfect one-to-one correspondence) between LogicBool and Bool, and that it preserves the logical operations of AND and OR. The negation theorem is the third pillar of this translation: it shows that the primitive two-sided structure of a distinction, when viewed through the standard Boolean lens, behaves exactly as classical negation does.

In Recognition Science, this theorem is part of a larger story about how the framework's primitive structures give rise to familiar logical and mathematical objects. The fact that negation translates correctly is a small but necessary step in showing that the framework's basic building blocks are compatible with classical logic. It does not, however, claim anything about the meaning of negation in a broader philosophical sense, nor does it address the question of whether the framework's primitive distinction is the only way to arrive at Boolean logic.

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

/-- The forward map: read `affirm` as `true`, `deny` as `false`. This
is the only reading that sends the meet to `Bool.and` and the join to
`Bool.or` (see the decoy theorems below for why the swapped reading is
rejected). -/
def toBool : LogicBool → Bool
  | affirm => true
  | deny   => false

/-- Negation is the swap of the two sides of the distinction. -/
def lnot : LogicBool → LogicBool
  | affirm => deny
  | deny   => affirm

/-- **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

What this page does not claim

This theorem does not claim that negation has any meaning beyond the formal operation of swapping the two constructors. This theorem does not claim that the framework's LogicBool is the only possible foundation for Boolean logic. This theorem does not claim anything about the philosophical or metaphysical nature of negation itself.

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: