Logic you can run

The analytic tradition, formalized

Analytic philosophy bets that clarity is computable. These snippets are distilled from the full tutorial and the 243-assertion book-pass.

Frege · logicism — ℕ from ∅

Numbers as sets built from the empty set: 0 := {}, successor n ∪ {n}. Russell's paradox shows naive comprehension cannot stand unguarded.

Frege's quantifiers & Barbara

Regiment “all” and “some”, then ask the syllogistic engine whether Barbara is valid — with a countermodel when it is not.

Russell · the King of France

the(set) is existence + uniqueness + predication. France's extent is empty → the description fails to denote (om), and “is bald” comes out false, not nonsense.

Frege · belief opacity

Lois believes Superman can fly but not Clark — co-referring names are not interchangeable in belief contexts.

Aristotle · the syllogistic

Before predicate logic, inference was the syllogism. valid_syllogism decides — and names the mood.

K3 vs LP · excluded middle

p ∨ ¬p is a classical tautology — but Kleene K3 rejects it when p is unknown; LP keeps it. Bivalence is a choice.

Vienna Circle · verificationism

diagnose sorts the meaningful from Carnap's Scheinsätze — “the Absolute…” is pseudo, not false.

Quine · web of belief

Conclusions rest on a corporate body of statements — retract one premise and what survives may re-derive from an alternate path. forget_cascade is the TMS hook.

Kripke · contingent identity

At the actual world, “the morning star” and “the evening star” co-refer — but across accessible worlds they can diverge, so identity is contingent, not necessary.