FOM: second-order logic is a myth

[Stephen G Simpson]

Jacques Dubucs 23 Feb 1999 03:21:24 writes:
 > What is "widely recognized among the f.o.m. searchers" is a point
 > of sociology, from which nothing follows except sociology.

No.  The points that I made were mathematical and logical, not
sociological.  My postings (22 Feb 1999 16:16:41 and 23 Feb 1999
20:18:42) and the posting of Martin Davis (22 Feb 1999 14:36:21)
concerned scientific/mathematical/logical aspects of or facts about
second-order logic.

Scientific Fact 1: It has not been fruitful to try to study the
structure of V_2 (= the set of second-order validities) as a whole,
except in the context of set theory and the set-theoretic independence
phenomenon.

Scientific Fact 2: It has been much more fruitful to study
proof-theoretic and model-theoretic aspects of various systems of
two-sorted (first-order!) predicate calculus inspired by something
like V_2.

These scientific facts are elaborated in the postings referenced
above.  We may provocatively summarize these facts as follows:  Down
with V_2!  Up with (first-order) predicate calculus!

I claim that these slogans are a fair summary of recent f.o.m.
research in this area.  For Dubucs to try to dismiss these facts and
slogans as mere sociology is an error.

 > ... this wide majority is not unanimity: 

Unanimity is not to be expected.  Even the most well-established
scientific facts can be disputed.  In our post-modern culture,
well-established facts are *routinely* disputed.

 > look for example at Shapiro's remarkable book "Foundations Without
 > Foundationalism. A Case for Second-Order Logic" (Oxford: Clarendon
 > Press, 1991).

Just today I got Shapiro's book from the library.  I haven't yet read
it.  At first glance, it appears to be a blend of some well-known
technical information about second-order logic with some kind of
strange Quinean attack on `foundationalism', i.e., mathematical
certainty.  From the preface:

   I believe that at least some reluctance for higher-order logic is
   related to remnants of what may be called *foundationalism* -- the
   vieew that it is possible and desirable to reconstruct mathematics
   on a secure basis, one maximally immune to rational doubt. ...
   Foundationalism, as understood here, has few proponents today, and
   for good reason. ... some theorists were even willing to cripple
   mathematics to make it stand on a supporting foundation.  Against
   this, I urge a thorough rejection of foundationalism. ...

I am among the `few proponents' of foundationalism.

Judging from a glance at Shapiro's book, I think it's something like
Reuben Hersh's book, but with more attention to the literature of
mathematical logic.  Perhaps I'll have more to say about it later.

Incidentally, Stewart Shapiro is here on FOM, so he is more than
welcome to join the discussion.

Dubucs:
 > I can't consider mathematical pieces as Henkin's famous 1950 paper
 > "Completeness in the theory of types" (JSL, XV-1950, 81-91) as
 > contributions to mythology.

I don't understand the thrust of this remark.  Henkin's 1950 paper
supports my (standard) view of the matter, not the continental or
pro-second-order view.  The underlying point of Henkin's paper is that
higher-order logic is best viewed in terms of plain, old,
garden-variety, first-order, predicate calculus.  When this is done,
the Henkin completeness theorem for higher-order logic immediately
falls out, as a corollary of the G"odel/Henkin completeness theorem
for predicate calculus.  Martin Davis explained this in 22 Feb 1999
14:36:21.

 > Let E Hilbert's second-order system, and B a geometrical truth
 > (i.e. a sentence which is true in the unique model of E). ...  is
 > there, yes or no, a set of formal (recursive) rules such that,
 > starting from E, one arrives to B by means of a finite number of
 > applications of the rules ?

No.  The nonexistence of such a set of rules follows from (a variant
of) the well-known fact that V_2 is not recursively enumerable.

It also follows, in a different way, from the well-known fact that the
class of statements that Dubucs refers to as `geometrical truths' is
much too broad to be geometrically relevant.  In particular, this
class includes virtually all interesting set-theoretic truths.  For
example, it includes either the continuum hypothesis or its negation,
depending on our assumptions about the underlying universe of sets.
For this reason alone, most geometers would agree with me that Dubucs'
notion of `geometrical truth' is wildly incorrect.

 > If it's the case, could you present this set of rules to FOM's
 > readers ? 

It's not the case.

 > If it's not the case, where is your vindication ?

My vindication is in my FOM postings cited above.

 > It's very amusing to be taken here as the average continental
 > philosopher. 

Is Dubucs a continental philosopher?  I don't assume that he is one.
He mentioned continental philosophers in his posting of 16 Feb 1999
09:48:52, and that was my point of reference.

 > My first posting (Feb 11) was just designed to denounce abusive
 > claims concerning irreducibility of geometry to logic.

I wasn't sure what your point was in that posting.  I still don't
really know what you are getting at.  In particular, I'm still not
sure where you stand on the issue of reducibility of geometrical
reasoning to logical reasoning.  

I say, based on powerful evidence, that geometrical reasoning *is*
reducible to logical reasoning, in an appropriate sense.  What do you
say?

 > ... the whole debate is somehow polluted by an indetermination
 > affecting the very notion of logic.

If the `notion of logic' is ambiguous, let's try to clarify or
disambiguate it.  In my opinion, we wouldn't lose much by restricting
it to predicate calculus, i.e. what Shapiro calls first-order
logic.  What do you think?

 > As regards your "logicist" thesis, I find the designation very
 > misleading.  ...

I have now agreed to call it `Hilbert's Thesis', following Martin
Davis 22 Feb 1999 22:38:39.

 > ... I can't anyway imagine an extension of it to geometry.

Why not?  What about Tarski's elementary geometry?  

Also, to take an alternative approach to this, there is a well-known
standard way of defining the real number system within
Zermelo-Fraenkel set theory, and on this basis we can formalize
everything we want about manifolds, differential geometry, etc., all
within Zermelo-Fraenkel set theory.

Do you deny that this is an extension of Hilbert's Thesis (what I
previously called the logicist thesis) to geometry?

 > The "logicization" of geometry is that: building a system of axioms
 > which describe precisely, rigourously, completely and without
 > "intuitive" or unanalyzed residue the structure of space. That's
 > Hilbert immortal achievement.

Hilbert made an important contribution, but he didn't have the last
word on the subject.  There are other `logicizations' of geometry:
Tarski's elementary geometry; the reconstruction of geometry within
ZFC; etc.  Hilbert's system is not so rigorous as these.  Like all
systems based on V_2, Hilbert's system conceals some unstated
assumptions.

 > Now, "logicization" as you conceive it would require also that the
 > geometrical truths (the sentences that are true in this
 > well-defined structure) are mechanically derivable from the axioms
 > which describe the structure.  This second requirement is beyond
 > reach. 

No, this is not beyond reach.  For example, it's the case for Tarski's
elementary geometry.

 > It arises from a too narrow concept of logic, according which the
 > only genuine logic is the first-order one.

I disagree.  First-order logic is perfectly adequate for logicization
of geometry.

-- Steve