Formal philosophy, end to end
The anthology surveys the formal apparatus of a whole discipline — and that apparatus is exactly what Axioma implements natively. These snippets are distilled from the 39-chapter, 873-assertion book-pass, one theme per part of the book.
Reiter · birds fly, but Tweety doesn't
Default logic computes extensions: "birds fly" fires until "penguins don't" — read off the concept hierarchy by specificity — overrides it. Classical logic can never retract; nonmonotonic reasoning must.
Gödel–Löb · read □ as "it is provable that"
On a GL frame the box distributes (K) — but at the irreflexive world w0, □p holds while p is false: reflection fails. A consistent theory cannot prove its own soundness — Gödel's lesson, model-checked.
Aristotle · the sea-battle tomorrow
Two open futures through the same moment. Ockhamism keeps bivalence by evaluating "there will be a sea-battle" per history; Łukasiewicz gives the contingent future the middle value instead — and excluded middle stops being designated.
Hintikka · the spymaster's knowledge
Knowledge is truth in every scenario compatible with the evidence. The spymaster knows the message came a month ago (true in both scenarios) but not whether the spy defected — genuine ignorance is ¬(Kd ∨ K¬d).
AGM · revision by the Levi identity
A contradiction turns the belief into a glut; revise() ranks retraction candidates least-entrenched first; contracting the guess and keeping the law is the Levi identity — give up the periphery, keep the center.
Davidson · the money-pump
Prefer a to b, b to c, and c to a — and a bookie can march you around the circle taking a euro per trade, forever. Exploitability has a formal signature: the transitive closure of your preferences reaches back to where it started.
von Wright · the O/P/F square
Standard deontic logic as norms on an agent: what is obligatory is thereby permitted (the D axiom), the forbidden is not permitted (the P/F dual) — and Sartre's student can hold two genuine, conflicting duties at once.
Nozick · Newcomb's problem
One payoff matrix, two expected utilities. EDT weights states by how they correlate with your act and one-boxes; CDT holds the already-sealed prediction fixed and two-boxes on dominance. The theories split on the same numbers.
Condorcet · the cycle
Three rational voters, each with a transitive ordering — yet the majority prefers a to b, b to c, and c to a. Society's preference is cyclic though no individual's is, and the choice set comes back empty.
List & Pettit · the discursive dilemma
Three judges, each perfectly consistent, vote proposition-by-proposition on v, b, and the verdict d ↔ (v ∧ b). The SAT engine certifies each judge — and proves the majority's collective judgment is unsatisfiable.
Go deeper
These ten themes are one snippet each from a 39-chapter pass — nonmonotonic reasoning to legal logic, every chapter a runnable script with its claims asserted by expect(...) and its honest gaps on record.