Registry · Theorem VII.T22 tau-effective formalized

VII.T22 — Single-Address Classical Logic

Within one NF address, excluded middle holds; classical logic valid at the micro scale.

Book VII Part 6 Ch. 66

Dependency Graph

Depends on (1)

I.T12

Depended on by (3)

VII.T23 VII.T24 VII.T26

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.single_address_classical_logic