Abduction

The third inference type, beside induction and deduction: generating a novel explanatory hypothesis for a singular phenomenon. Deduction guarantees truth from premises. Induction finds patterns that generalise across data. Abduction invents a cause — and it is the only one of the three that produces premises rather than consuming them (llms-cant-jump).

For this spoke’s purposes the useful framing is Einstein’s cycle: sense experience → jump → axioms → deduction → theorems → verification against experience. Cluster E has been documenting the mechanization of the deduction arrow (lean-theorem-prover, alphaproof, tla-plus). Abduction is the arrow before it, and nothing in the corpus mechanizes it.

Manipulative abduction

llms-cant-jump adopts Magnani et al. (2009)‘s manipulative abduction: hypotheses produced by embodied simulation — thinking by doing, intervening in a mental model rather than watching one. Einstein’s falling observer is the worked example. The distinction from ordinary abduction is intervention: the jump comes from asking what would happen if I cut the cable, not from observing elevators.

This splits the capability into two stages, which is what makes it tractable rather than mystical: imagine an observation via simulation, then derive an explanation from it. Zahavy’s argument is that ARC-AGI tests only the second — sparse grids requiring a logical leap, with no physical manipulation anywhere in the task — so a benchmark widely read as measuring the creative leap measures half of it.

Why it matters to the mechanizing-reasoning lineage

This lineage runs Leibniz → Hilbert → Gödel → Lean: the ambition to make reasoning mechanical, and the successive discoveries of what won’t go. Abduction is a new entry in that ledger and a different kind of obstacle. Gödel’s is a limit on what formal systems can prove about themselves. This one is claimed to be a limit on architecture rather than logic — a system without sensory grounding can’t originate the axioms — which means, unlike Gödel’s, it comes with a proposed remedy: action-controllable world models supplying the simulation.

Whether that remedy works is unsettled and the paper is a position paper. Recorded as the current boundary of the programme rather than as a proof.

Related

llms-cant-jump · alphaproof · lean-theorem-prover · tom-zahavy · synthesis