How To Succeed In Proof Business Without Really Trying

Re: R.J. LiptonSurely You Are Joking?

Comment 1

Even at the mailroom entry point of propositional calculus, there is a qualitative difference between insight proofs and routine proofs.  Human beings can do either sort, as a rule, but routinizing insight is notoriously difficult, so the clerical routines have always been the ones that lend themselves to the canonical brands of canned mechanical proofs.

Just by way of a very choice example, consider the Praeclarum Theorema (Splendid Theorem) noted by Leibniz, as presented in cactus syntax here:

I’ll discuss different ways of proving this in the comments that follow.

Comment 2

The proof given via the link above is the sort that a human, all too human was able to find without much trouble.  You can see that it exhibits a capacity for global pattern recognition and analogical pattern matching — manifestly aided by the use of graphical syntax — that marks the human knack for finding proofs.  When I first set to work developing a Simple Propositional Logic Engine (SPLE) those were the aptitudes I naturally sought to emulate.  Alas, I lacked the metaptitude for that.

Comment 3

For my next proof of the Praeclarum Theorema I give an example of a routine proof, the sort of proof that a machine with all its blinkers on can be trained to derive simply by following its nose, demanding as little insight as possible and exploiting the barest modicum of tightly reigned-in look-ahead.

This entry was posted in Algorithms, Animata, Artificial Intelligence, Automatic Theorem Proving, Boolean Algebra, Boolean Functions, C.S. Peirce, Cactus Graphs, Computational Complexity, Graph Theory, Logic, Logical Graphs, Minimal Negation Operators, Model Theory, Peirce, Praeclarum Theorema, Proof Theory, Propositional Calculus, Visualization and tagged , , , , , , , , , , , , , , , , , , . Bookmark the permalink.

2 Responses to How To Succeed In Proof Business Without Really Trying

  1. Re: “The proof given via the link above […] exhibits a capacity for global pattern recognition and analogical pattern matching — manifestly aided by the use of graphical syntax — that marks the human knack for finding proofs.”  I’d say that chemical interactions, or what happens into a living cell, have the same, at least apparent, characteristics.  Because molecules don’t need sorting and branch predictors.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.