How To Succeed In Proof Business Without Really Trying

Post   : How To Succeed In Proof Business Without Really Trying
URL    : http://inquiryintoinquiry.com/2013/07/15/how-to-succeed-in-proof-business-without-really-trying/
Posted : July 15, 2013 at 12:00 am
Author : Jon Awbrey

Re: Surely You Are Joking?
At: http://rjlipton.wordpress.com/2013/07/14/surely-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:

• Praeclarum Theorema
   http://inquiryintoinquiry.com/2008/10/05/praeclarum-theorema/

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 out trying to
develop a Simple Propositional Logic Engine (SPLE) 'n' didn't, 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.

• Praeclarum Theorema : Proof by Case Analysis-Synthesis Theorem (CAST)
   http://intersci.ss.uci.edu/wiki/index.php/Propositional_Equation_Reasoning_Systems#Praeclarum_theorema_:_Proof_by_CAST

-- 

academia: http://independent.academia.edu/JonAwbrey
my word press blog: http://inquiryintoinquiry.com/
inquiry list: http://stderr.org/pipermail/inquiry/
mwb: http://www.mywikibiz.com/Directory:Jon_Awbrey
oeiswiki: http://www.oeis.org/wiki/User:Jon_Awbrey
facebook page: https://www.facebook.com/JonnyCache