Registry · Proposition I.P13 tau-effective formalized

I.P13 — Boolean Recovery

Boolean logic as a quotient of Truth4: collapsing B and N recovers classical two-valued logic. The forgetful map Truth4 -> Bool is a lattice homomorphism.

Book I Part 12 Ch. 48

Dependency Graph

Depends on (2)

I.D21 I.T13

Depended on by (1)

I.P47

Lean Formalization

Module: TauLib.BookI.Logic.BooleanRecovery

Symbol: Tau.Logic.boolean_recovery