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, Artificial Intelligence, Boolean Functions, C.S. Peirce, Cactus Graphs, Graph Theory, Logic, Logical Graphs, Minimal Negation Operators, Peirce, Propositional Calculus, Theorem Proving 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 )

w

Connecting to %s