The laws are choices, not necessities
Every logic here adds a value to the classical two. A gap (om / ?ᵏ in Kleene K3, ?ᵇ in FDE) is a sentence that is neither true nor false; a glut (⊤⊥ᵇ) is one that is both. The values are literals: what the interpreter prints is valid source, so ⊤⊥ᵇ, ?ⁱ, ½ł can be typed straight back (constructors like belnap("both") remain the dynamic form; each logic's grid is Belnap.values etc.). What counts as valid then depends on the designated set — the values that count as "true enough." Use designated(v) to decide validity: it returns a real Boolean and knows each logic's designated set, so a forall over the value grid is the truth-table method — and if v branches by the same set. Snippets are lifted from the Priest Non-Classical Logic book pass.
Excluded middle — Kleene K3 drops it, LP keeps it
p ∨ ¬p is a classical tautology. K3 designates only {true}, so a gap escapes it — p ∨ ¬p is undesignated when p is unknown, and the law fails. LP designates {true, both}, so a glut makes it hold — same tables, opposite designated set, opposite verdict.
A glut is both true and false — and survives negation
The paraconsistent value belnap("both") is designated (a glut is true-enough), and negating it leaves it unchanged: ¬(both) = both. So a contradiction p ∧ ¬p at a glut point is designated on both sides — the seed of paraconsistency, where a contradiction need not detonate.
Explosion & disjunctive syllogism die under LP
Classically, a contradiction entails everything (ex contradictione quodlibet). In LP it does not: at p = both, both p and ¬p are designated while q stays false — premises true-enough, conclusion not. The same glut sinks disjunctive syllogism (p∨q, ¬p ⊢ q), paraconsistency's famous cost.
Double-negation elimination fails — Gödel G3, the intuitionist gap logic
Intuitionism treats a proposition as true only once it is proved, so a proof of ¬¬p is weaker than a proof of p. In Gödel G3, ¬¬p → p is not valid (at p = unknown it comes out undesignated) — and excluded middle falls with it. But the provable half, p → ¬¬p, still stands. That asymmetry is exactly intuitionist negation.
Gluts at possible worlds — no modal explosion
A Kripke world can assign an atom an FDE value, not just a bit. Here w0 makes p a glut and q false; □ and ◇ range over accessible worlds, designation-aware. The glut survives negation, and necessarily p holds while necessarily q does not — a contradiction at a world does not manufacture q. Paraconsistency survives the modal layer.
What breaks, where, and why
The same classical law survives in one logic and dies in another — and the reason is always the same two dials: the extra value (gap or glut) and the designated set. Axioma exposes both, so the truth-table method becomes a one-line forall.
Excluded middle p∨¬p — a gap (om) is undesignated, so the law escapes at the unknown point.
Excluded middle survives — LP designates {true, both}, so a glut keeps every classical tautology.
Explosion and disjunctive syllogism — the glut both makes the premises designated while the conclusion stays false.
Double-negation elimination and excluded middle — but the provable half p→¬¬p stands. Intuitionist negation, exactly.
Paraconsistency — a glut at a world makes □p designated without forcing □q. No modal explosion.
None of this is a bug in classical logic — it is what happens when you relax bivalence on purpose. Different applications (partial information, inconsistent databases, constructive proof) want different laws to hold, and Axioma lets you run each choice and read the consequences off the screen.
Run the whole book pass
Priest's An Introduction to Non-Classical Logic runs chapter by chapter in the sweep — K3, Ł3, FDE, G3, and the many-valued modal worlds. Fork it, change the designated set, add a value, and watch the laws move.