Re: Ken Regan • The Shapes of Computations

The insight it takes to find a succinct axiom set for a theoretical domain falls under the heading of abductive or retroductive reasoning, a knack as yet refractory to computational attack, but once we’ve lucked on a select‑enough set of axioms we can develop theorems which afford a more navigable course through the subject.

For example, back on the range of propositional logic, it takes but a few pivotal theorems plus the lever of mathematical induction to derive the Case Analysis-Synthesis Theorem (CAST) that affords a bridge between proof‑theoretic methods demanding a modicum of insight and model‑theoretic methods able to be run routinely.