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:
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.
manifests a type of formal degeneracy (loss of generality) compared with the three-point universe 
equals the number of “off-diagonal” pairs, those of the form 
so the two-point case exhibits symmetries that will be broken as soon as one adds another element to the universe.
yields exactly nine individual dual relatives or ordered pairs of universe elements:
![\left( \begin{matrix} \mathrm{I\!:\!I} & \mathrm{I\!:\!J} & \mathrm{I\!:\!K} \\[4pt] \mathrm{J\!:\!I} & \mathrm{J\!:\!J} & \mathrm{J\!:\!K} \\[4pt] \mathrm{K\!:\!I} & \mathrm{K\!:\!J} & \mathrm{K\!:\!K} \end{matrix} \right)](https://s0.wp.com/latex.php?latex=%5Cleft%28+%5Cbegin%7Bmatrix%7D++%5Cmathrm%7BI%5C%21%3A%5C%21I%7D+%26+%5Cmathrm%7BI%5C%21%3A%5C%21J%7D+%26+%5Cmathrm%7BI%5C%21%3A%5C%21K%7D++%5C%5C%5B4pt%5D++%5Cmathrm%7BJ%5C%21%3A%5C%21I%7D+%26+%5Cmathrm%7BJ%5C%21%3A%5C%21J%7D+%26+%5Cmathrm%7BJ%5C%21%3A%5C%21K%7D++%5C%5C%5B4pt%5D++%5Cmathrm%7BK%5C%21%3A%5C%21I%7D+%26+%5Cmathrm%7BK%5C%21%3A%5C%21J%7D+%26+%5Cmathrm%7BK%5C%21%3A%5C%21K%7D++%5Cend%7Bmatrix%7D+%5Cright%29&bg=ffffff&fg=000000&s=1&c=20201002)
dual relatives over this universe of discourse, since each one is formed by choosing a subset of the nine ordered pairs and then “aggregating” them, forming their logical sum, or simply regarding them as a subset. Taking the square array of ordered pairs as a backdrop, any one of the 
dual relatives may be represented by a square matrix of binary values, a value of 
occupying the place of each ordered pair that belongs to the subset and a value of 
occupying the place of each ordered pair that does not belong to the subset in question.
are tabulated below according to the following plan:
off-diagonal matrices are shown in the rest of the display, arranged in rank order by increasing numbers of 
and decreasing numbers of 
suppressing the fixed zeroes along the diagonals to make the changing patterns of 
and 
is equal to the binomial coefficient 
or 
The values of 
are given by the row of 
Inquiry Into Inquiry 