a fork of Lean 4 (v4.28.0) implementing a true paraconsistent type-theoretic kernel — the principle of explosion — "ex falso quodlibet" — is disabled at the kernel level.
belnap-logic paraconsistent-logic imscriptive imscribe imscribing-grammar dialetheia paraconsistent-lean4 paraconsistent-kernel four-logic
-
Updated
Jun 4, 2026 - Lean