Re: Ken Regan • The Shapes of Computations

The most striking example of a “Primitive Insight Proof” (PIP❢) known to me is the Dawes–Utting proof of the Double Negation Theorem from the CSP–GSB axioms for propositional logic.  There is a graphically illustrated discussion at the following location:

• Logical Graphs • Double Negation

I cannot hazard a guess what order of insight it took to find that proof — for me it would have involved a whole lot of random search through the space of possible proofs, and that’s even if I got the notion to look for one in the first place.

There is of course a much deeper order of insight into the mathematical form of logical reasoning that it took C.S. Peirce to arrive at his maximally elegant 4-axiom set.