For the past month I’ve been working through a Japanese introductory logic textbook, one section a day, translating each chapter’s proofs into small snippets of Haskell as I go. I did not expect a textbook from 2000 about propositional and predicate logic to change how I think about why some of my tools hang and others don’t. But somewhere around chapter 7, that’s exactly what happened.

Here is the shape of the argument, stripped of the Japanese and the code.

The free lunch of propositional logic

Propositional logic — the logic of “and,” “or,” “not,” “if-then,” applied to atomic statements with no internal structure — comes with something that feels, at first, like a superpower. Any question you can pose in its language (“is this formula a tautology,” “are these two formulas equivalent,” “does this argument follow validly from its premises”) can be settled by brute force: enumerate every possible assignment of true/false to the atomic statements, check each row, done. If there are n atomic statements, there are 2^n rows. The table is finite, the procedure always terminates, and it always gives you a definite yes or no. This is decidability, and propositional logic has it for free.

It’s worth sitting with why this is possible at all. Truth tables give you an exhaustive search over the whole space of possibilities, and that only works because the space is finite. The moment you can enumerate every case, testing becomes proof — the disagreement between Edsger Dijkstra’s famous remark that testing can show the presence of bugs but never their absence, and this textbook’s confident 2^n-row tables, dissolves once you notice they’re describing the same fact from opposite sides. Dijkstra’s warning is about infinite input spaces, where a test suite is necessarily a sample. A truth table isn’t a sample. It’s a census.

The catch, and it is a serious one, is that this completeness comes from a lack of ambition. Propositional logic can’t talk about individuals, properties of individuals, or relations between them. It can’t express “everyone loves someone” or “there is a path from A to B.” Its entire semantic content is captured by a function from the finite set of atomic truth values to a truth value — which means, however many formulas you can write down, there are only 2^(2^n) genuinely distinct meanings for n atoms to express. The syntax is infinite; the semantics is finite. That gap is exactly the slack that makes exhaustive checking possible.

Where the floor drops out

Predicate logic adds quantifiers (“for all,” “there exists”) and relations between individuals, and this is where the free lunch ends. The moment your language can say things like “for every x there exists a y such that R(x, y)” — the schema underlying claims about paths in a graph, reachability, chains of relationships — the finite semantic content of propositional logic is gone. An individual’s relationships to other individuals can’t be collapsed into a finite table the way a truth assignment can.

What’s striking is how this shows up operationally, not just in a theorem statement. The textbook walks through a proof-search procedure (a tableau method) for testing validity, and it has a structural asymmetry baked into it: the rule for handling an existential quantifier fires once per formula and is done — it introduces one new individual and moves on. The rule for handling a universal quantifier can be re-applied indefinitely, to any individual that shows up in the proof at any point, including individuals generated by later steps. In propositional logic this asymmetry is invisible because the “individuals” are just truth values and there are only 2^n of them; the search always bottoms out. In full predicate logic, a formula like “for all x there exists a y such that R(x,y)” can trigger a chain — introduce an individual to satisfy the existential, apply the universal rule to it, get a new existential obligation, introduce another individual, apply the universal rule again — that has no guaranteed end. This is structurally identical to a Prolog query that keeps trying to satisfy a recursive clause and never backtracks out, and it is not a coincidence: automated theorem provers are built on exactly this kind of search.

This isn’t a flaw in this particular proof method. It’s a symptom of something Alonzo Church and Alan Turing each proved independently in 1936, using entirely different formal tools (Church with the lambda calculus, Turing with what we now call the Turing machine): the question “is this predicate-logic formula valid?” cannot be answered by any algorithm that is guaranteed to halt on every input. This was Hilbert’s Entscheidungsproblem — decision problem — and the answer, arrived at twice from different directions, was no.1 The book’s chapter on this result carries the deliberately reassuring title “Don’t blame the logicians” — the point being that this isn’t a failure of cleverness. A smarter search procedure cannot fix it, because the limitation is a proven mathematical fact about what the class of algorithms can do, not a gap in what’s been tried so far.

The asymmetry that survives

What you’re left with instead of decidability is semi-decidability: if a formula is valid, some search procedure is guaranteed to eventually confirm it and halt. If a formula is invalid, no procedure is guaranteed to tell you so — it might run forever, and a search that has run for a very long time without finding a proof gives you no way to distinguish “this is invalid” from “the proof is still out there.” Gödel’s completeness theorem is what guarantees the “yes” side: the set of valid formulas is recursively enumerable, so systematically enumerating and checking candidate proofs will eventually surface one if it exists.2 Nothing analogous rescues the “no” side, and this isn’t an oversight — it’s provably equivalent to the halting problem. You can encode “does this program halt” as “is this formula valid,” in a way that shows any general validity-decider would also decide halting, which is already known to be impossible.

I found this satisfying rather than defeating, because it names something I keep running into without a name for it. Type inference in a language with a sufficiently expressive type system (higher-rank polymorphism, dependent types) can hang. SMT solvers can hang. Package-version resolvers, which reduce to satisfiability, can hang. In each case there’s a design choice hiding underneath: does the tool stay inside a fragment of logic small enough to guarantee termination, trading away expressive power for a promise that it will always tell you something — or does it take the expressive power and accept that sometimes, in practice, the answer is a timeout? Type-system designers seem to lean toward the first choice more often than the automated-reasoning and logic-programming world does, and I don’t yet have a confident account of why the cultures split that way rather than the field being consistent about it. It might just be that a type checker that occasionally refuses to compile your program is more tolerable than a type checker that occasionally hangs your build.

There’s a second thing worth naming, which the book is careful about throughout: the claim that Turing machines and lambda calculus both capture “the” correct formalization of the informal, pre-theoretic idea of “computation” — the Church-Turing thesis — is called a thesis and not a theorem for a real reason. That two independently-invented formal systems turn out to be equivalent to each other is a theorem, provable inside mathematics. That this shared notion is the right formalization of the fuzzy human concept of “what can be computed” is not something mathematics can verify, because the fuzzy human concept was never itself a mathematical object to begin with. It’s a claim about the world, supported by the fact that every subsequent attempt at formalizing computation — recursive functions, register machines, cellular automata — has landed on the same equivalence class, but it remains, honestly, an inductive claim rather than a proof. I like that the book insists on marking this line rather than blurring it, because the boundary between what’s proven and what’s merely never-yet-refuted is exactly the kind of distinction that’s easy to let slide once a claim has been confirmed often enough.

An open question

The unresolved thing I’m sitting with is practical, not technical. When you know a problem sits behind a wall like this — genuinely undecidable, not just hard — there seem to be exactly two moves available: shrink the language until you’re back in a decidable fragment, or keep the expressive power and manage the risk of non-termination with heuristics, depth limits, and timeouts. Both are legitimate engineering choices, and different communities seem to have made opposite bets by convention rather than by any argument I can point to. I don’t think there’s a single right answer here — but I’d be curious whether anyone has actually formalized why those two cultures split the way they did, rather than it just being how the fields happened to grow up.

  1. Entscheidungsproblem. Wikipedia. Accessed 2026-08-11. ↩

  2. Gödel’s completeness theorem. Wikipedia. Accessed 2026-08-11. ↩