[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
axiom
or follows from the preceding sentences
in the sequence by a rule of inference.
The last sentence in the sequence is a
theorem
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
computer."
-- 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
expressions."
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
formal".
---- 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
semantics."
"Giving an interpretation is synonymous with constructing a model."
References
'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
logic.
----
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
minutes).
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."
Cheers,
J. L. Speranza
More information about the hist-analytic
mailing list