Mathematics Boolean Algebra From Rs

Boolean algebra from recognition

Boolean algebra is the mathematics of truth values: true and false, combined with operations like AND, OR, and NOT. It is the logic that underpins digital circuits and computer programs. In its simplest finite form, the Boolean algebra on a set of n bits has 2^n possible states, and the full set of operations on those states is much larger. The classical object here is the algebra on three bits, which has exactly 2^3 = 8 states, often pictured as the vertices of a cube.

The five canonical Boolean operations are AND, OR, NOT, NAND, and NOR. These five are the standard building blocks: NAND and NOR are each alone sufficient to express every Boolean function, a fact known since the 1913 work of Henry Sheffer. The algebra on three bits has eight atoms, the minimal nonzero elements from which every other element is built. The number 8 = 2^3 is the same 2^3 that counts the states, which is why the cube picture works.

In Recognition Science, the framework models a discrete record of recognition events as a lattice, and it identifies the three-bit lattice with the Boolean algebra above. The framework's machine-checked library of formal theorems contains a module that establishes the basic counts: there are exactly five canonical Boolean operations, and the lattice has exactly eight atoms, equal to 2^3. These are proved by direct computation in the library, with no unproved assumptions. The module packages these two facts into a single certificate that the three-bit recognition lattice is a Boolean algebra.

What this establishes in plain language is that the basic structure of recognition, when restricted to three bits, has the same shape as classical Boolean logic. The five operations and eight atoms are not chosen arbitrarily; they are the exact counts that the library proves. This is a small but concrete bridge between the framework's notion of recognition and the standard mathematics of logic, showing that the two agree on this finite structure.

theorem boolOpCount : Fintype.card BoolOp = 5 := by decide

theorem atomCount_eq_8 : atomCount = 8 := by decide

theorem atoms_eq_2cubeD : atomCount = 2 ^ 3 := rfl

What this page does not claim

This does not claim that all Boolean algebras arise from recognition. This does not claim that the five operations are the only possible Boolean operations. This does not claim that the module proves the full structure of Boolean algebra, only the counts of operations and atoms.

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/Mathematics/BooleanAlgebraFromRS.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: