Registry · Remark I.R01 established not_applicable

I.R01 — Axiom Independence

Six countermodel sketches showing K1-K6 are mutually independent: no proper subset entails the remaining axiom.

Book I Part 1 Ch. 4

Dependency Graph

Depends on (6)

I.K1 I.K2 I.K3 I.K4 I.K5 I.K6

Lean Formalization

Module:

Symbol: