Re: Ken Regan • The Shapes of Computations

There are several issues of computation shape and proof style that raise their heads already at the logical ground level of boolean functions and propositional calculus.  From what I’ve seen, there are three dimensions of variation that appear most prominent at this stage:

• Insight Proofs vs. Routine Proofs
• Model-Theoretic Methods vs. Proof-Theoretic Methods
• Equational (Information-Preserving) Proofs vs.
  Implicational (Information-Reducing) Proofs

More later, after I dig up some basic examples …