FTH0093canonicalv1earned_topos_non_boolean (theorem)
/-- [I.P27] The earned topos E_τ is non-Boolean. A Boolean topos has Ω = {0, 1} (two truth values). Our Ω_τ has FOUR truth values (T, F, B, N). The complement law ¬¬p = p holds in Boolean topoi but fails in E_τ: ¬¬B = ¬N = B, which works, but the issue is that B and N are distinct from T and F. The explosion barrier (I.T13) gives a direct witness: B ⟹ F is not T (it's N), so material implication doesn't validate ex falso quodlibet. -/
Formalization
Identifiers
Aliases & legacy IDs
earned_topos_non_booleanearned-topos-non-booleanTauLib.BookI.Topos.EarnedTopos::earned_topos_non_booleanRelease lines
corpus_v2corpus_v3_workingVersion & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.