[hist-analytic] Glory

Jlsperanza at aol.com Jlsperanza at aol.com
Sat Dec 26 22:15:50 EST 2009

I wrote

>I would like to drop a few points about the nature  of 'proof-theory' of 
the type that R. B. Jones seems to be >defending on this  and other fora. 
Indeed, my main point is a query (to Jones or his 'ilk'!).  

and wish to thank some useful offlist leads.

For starters, there  are a few distinctions to be made. The main one is to 
qualify the above in  connection with "formal proof". 

--- May I share some running commentary  on the wiki entry on 'formal 
proof'. My query related to 'computerised proof  technology'. It seems that a 
computer can not and will not 'skip' a step. So why  do we _allow_ that 
non-computers do it? Indeed Grice once remarked, as I recall  -- in Aspects of 
Reason -- that the less inferential steps one displays  explicitly, the more 
'rational' one will be accounted as being. 

But  since I titled this "Glory" i.e. Humpty Dumpty's 'a nice knockdown 
argument' --  only in the phrase, said smugly, and to Alice, only:

"There's _glory_ for you".

I was wondering if we can treat 'prove' as a  factive, alla 'know'.

So, we can say, 'the computer proved it', because,  well, the computer, as 
per computerised proof technology never skipped a step.  But if humans do, 
can we say that they _have_ proved (or as Americans may  prefer, proven) it? 

Where _is_ the proof of the pudding?

Is that  the exception that proves the rule?

Grice remarks of this topologist he  knew who was regarded with something 
near veneration, "yet, everytime he wanted  to display a proof, either there 
was at least one mistake, or a lapse in the  sequencing" (words to that 
perlocutionary effect).

In similar contexts,  Grice would seem to have thought that Chomsky's rule 
derivations (for the  formation of well-formed sentences) are _so_ complex 
that we cannot assume the  human brain 'processes' them, and yet we _can_ 
produce well-formed  transformations of well-formed sentences.

I would think Grice, when  challenged about the psychological _unreality_ 
of the 'precise' proof, would  recourse to the concept of 'deeming' which 
became of favourite of his later  philosophy. We can _deem_ a proof to have 
taken place. 

But I don't think  the writers of wiki will agree.

wiki starts by _defining_ a formal proof  (or 'derivation') as
          "a finite sequence  of sentences 
          (called wff in the  case of a formal language) 
          each of which is an 
          or follows from the  preceding sentences 
          in the sequence  by a rule of inference. 
          The last sentence in  the sequence is a 
         of a formal system."
"The theorem is a SYNTACTIC consequence of all the well-formed  formulas 
preceding it in the proof."
     (emphasis mine. JLS)
"For a wff to qualify as part of a proof, it must be the result of applying 
 a rule of the deductive apparatus of some formal system to the  previous 
wffs in the proof sequence."

"Formal proofs [can be] constructed with THE HELP OF  COMPUTERS in 
interactive theorem proving."
"Significantly, these proofs can be checked AUTOMATICALLY, also by  
-- where automatically may mean, also, 'algorithmically', or in virtue of  
the existence of an algorithm or decision procedure, I don't know.
wiki continues:

"CHECKING formal proofs is usually simple,  whereas FINDING proofs 
(AUTOMATED theorem PROVING) is generally  computationally hard."
I wonder if the above refers to 'abduction' vs. deduction. When I did logic 
 -- never mind taught it -- I found that one was given some more freedom in 
 FINDING a proof. Some exercises were pretty silly, in that they provided 
you the  premise and the conclusion (or last sentence in the sequence) and 
motivated you  to _prove_ it. Indeed, compared to that, which requires SOME 
imagination -- and  more so if you are NOT given the conclusion -- _checking_ 
a proof seems like a  piece of, er, pudding.

The wiki entry then defines a 'formal language' as 

"a set of finite sequences of SYMBOLS."
(cfr. Grice, cited in Strawson's obit, "If you can't put it in symbols,  
it's not worth saying") (I'm still struggling to provide for that the best  
symbolic notation possible).
"Such a language", the wiki entry goes on, "can be defined without  
reference to any meanings of any of its expressions; it can exist before any  
interpretation is assigned to it – that is, before it has any meaning."
Point taken; it is syntactic. But 'rules of inference' alla Gentzen  
_usually_ seem to have a justification in terms of their intuitive reflection of  
'ordinary-language' inferences. I cannot see how one can device (or even 
care to  device) a rule of inference alla introduction or elimination of any 
logical  constant unless one is in some way 'reconstructing' the intuitively 
valid  inferences. 
The necessity of defining a formal language is obvious for, as the wiki  
entry goes,
"Formal proofs are expressed in some formal language."

"A formal grammar (also called formation rules) is a precise  description 
of the wff of a formal language."
"It is synonymous with the set of strings over the alphabet of the formal  
language which constitute well formed formulas."
"A formal system (also called a logical CALCULUS, or a logical system)  
consists of a formal language together with a deductive apparatus (also called 
a  deductive system). The deductive apparatus may consist of a set of  
transformation rules (also called inference rules) or a set of axioms, or have  
both. A formal system is used to derive one expression from one or more other 
It's amazing how well-versed was Grice in all this and circa 1967, i.e.  
before moving to "Formalistic America" (S. Chapman in her bio of _Grice_ in a  
rather irritating way has a whole chapter entitled, "American formalism" as 
if  this were the property of Americans!). More amazing is to think that by 
1969 he  was able to quote from Boolos, Parsons, Myro, and Mates in his 
"System" in the  festschrift for Quine. And by the same time, perhaps the end 
of it all was that  hurtful remark by Putnam, "who, of all people," Grice 
confides in his  "Prejudices and predilections" "complained that I was too 
---- Myro once relabelled Grice's System as "System G" -- in manuscripts  
made available to me by Sally Haslanger. And I have personally managed to 
expand  Myro's system G into a 'highly powerful", as I proudly describe it, or  
alternatively, "hopefully possible" -- the idea is that it should 
abbreviate as  "h. p." -- So that I get
    System G(hp)
-- where hp is for 'herbert paul' that is. Oddly I was recently told that  
'hp' can mean not just 'hire purchase' but a type of sauce. My friend Donal  
McEvoy having recently compiled for my delectation a little limerick:
       There once was a philosopher  Grice
Who when asked did he think H.P.  (*)  nice?
Replied, "I'm not  sure
Of your saucy implicature -
       I'll get back  to you when I've  thought twice."

(* In England a most famous version of brown or "Daddy's" sauce is  "H.P. 
Sauce". [Hence "saucy implicature"]).

wiki continues:

"An interpretation of a formal SYSTEM or CALCULUS"
Grice liked 'calculus' as when he said that he only really showed some  
interest, in "Prejudices and Predilections" for 'first-order predicate 
calculus'  'with identity', he hastens to add.
"is the assignment of meanings to the SYMBOLS, and truth-values to the  
sentences of a formal system. The study of interpretations is called formal  
"Giving an interpretation is synonymous with constructing a model."

'deduction', in The Cambridge Dictionary of Philosophy,  

External links
"A Special Issue on Formal Proof". Notices of the  American Mathematical 
Society. December 2008.  http://www.ams.org/notices/200811/.  
2πix.com: Logic Part of a series  of articles covering mathematics and 

In many publications Grice did want to go 'over the top' -- which is the  
_norm_ with formal proof, and proceed step by step. Notably in Aspects of 
Reason  when he tries to reconstruct Shropshire's reasoning to the effect that 
the soul  is immortal.
(out of the premise that if you behead a chicken it runs for some five  
On the other hand, he would refer to 'implicit' reasoning. For Grice, to  
'reason' when it comes to non-computers, involves a _causal_ link. There must 
be  an intention to infer, and the intention that there is a VALID passage 
from  datum to claim via a warrant (to use Toulmin's terminology) should 
play a causal  role in the entertaining of a conclusion. I once shared this 
with Stich, and I  don't know if it was the weather or what (it was at 
Campinas) but he said,  smugly, "Preposterous" (implicating that Griceans don't know 
the first thing  about causal roles in hard-core cognitive science).
So it's EXPLICIT reasoning we are talking here. R. Warner, who edited  
Aspects of Reason, makes the distinction explicit. As Warner notes, it would be  
bold to consider that the following is an explicit piece of reasoning. Or a 
 piece of explicit reasoning:
   Everybody loves my baby but my baby don't love nobody but  me
   Therefore, I am my baby.
On the other hand, it can be made explicit as follows:
   1. Everybody loves my baby (Ass.)
   2. My baby don't love nobody but me (Ass.)
   3. My baby is included in the class of everybody. 
   4. My baby loves my baby (From 1 and 3)
   5. Therefore, I am my baby
Etc. (It's best the way Warner has it in non-formal prose, along the lines, 
 "Everybody loves my baby but my baby don't love nobody but me, but since 
my baby  is included in 'everybody', this yields that my baby loves my baby. 
Now, since  my baby don't love nobody my baby, I am my baby."
Another who was for formal proof was D. F. Pears. He would like to have  
people discussing hard pieces of reasoning with him. One was cautious, "I  
wouldn't like to risk my reputation by entering in such a difficult  
argumentation with you". To which Pears replied, "But honestly, who cares about  your 
reputation?" As the obit reads, "always intent on the philosophic, not the  
personal, nub."

J. L. Speranza

More information about the hist-analytic mailing list