FOM: contradiction-free vs consistent

[Stephen G Simpson]

Robert Tragesser 18 Feb 1999 20:53:06 writes:
 > What can be said in general for logics in which Go"del's completeness
 > theorem fails,  about theories in those logics which
 > (A) have no model,  but
 > (B) an explicit logical contradiction is not derivable?

G"odel's completeness theorem holds for all theories in the predicate
calculus, i.e. what has sometimes been called first-order logic.
Hence, the logics that Tragesser is asking about are necessarily
beyond the pale of the predicate calculus.  Moreover, although logics
other than the predicate calculus have been studied occasionally, the
predicate calculus is far and away the most important logic for f.o.m.

This last remark is based on what might be called `the logicist
thesis'.  (I seem to remember that Martin Davis has referred to this
as `Hilbert's Thesis'.)  The gist of the logicist thesis is that, once
a mathematician makes all of his primitive notions and non-logical
assumptions fully explicit, it will then be possible to express these
assumptions as formulas of the predicate calculus, and all of the
mathematician's informal proofs concerning those notions will then be
expressible by corresponding formal proofs within the predicate
calculus.

It seems to me that there is a very large amount of of evidence for
the logicist thesis, and no evidence against it.  For instance, set
theory is formalized and axiomatized as a theory in the --
first-order! -- predicate calculus.  Since all of core mathematics
(algebra, analysis, topology, ...) can be formalized in set theory, it
follows that the logicist thesis holds for core mathematics.  In
addition, the work in foundations of geometry by Euclid, Hilbert,
Tarski, ... shows that geometrical reasoning can be formalized
directly in (first-order) predicate calculus, without going through
set theory.  Even so-called second-order theories (e.g. second-order
arithmetic, as in my book `Subsystems of Second Order Arithmetic', see
<http://www.math.psu.edu/simpson/sosoa>) are actually two-sorted
first-order theories, so the logicist thesis also applies to that
entire body of work in f.o.m.

 > Bill Tait and Eliot Mendelsohn provided contrived theories (as in
 > the appendix the the new edition of Mendelsohn); one wonders if
 > there are "real" theories.

I have no idea what contrived or real theories satisfying (A) and (B)
Tragesser is referring to.  However, since all such theories
necessarily fall outside the pale of the predicate calculus, their
actual or potential relevance to f.o.m. needs to be explained.

 > The last seems to me an important Friedman type question.

Why?  All of Friedman's independence results are with respect to
specific theories in the predicate calculus.

 > It does seem that w..r.t. Bolyai-Lob. geometry, "conmsistency"
 > meant finding an interpretation in significant/current/substantial
 > mathematics, which integrated B-L geometry into mathematics in a
 > significant/fruitful way, such as the upper-half plane model
 > vividly does.

This remark of Tragesser isn't in agreement with the current
understanding of the meaning of the concept `consistency'.  The
current understanding is that, to establish the consistency of
Bolyai-Lobachevski geometry or any other mathematical theory, it
suffices to exhibit a model of it.  This could be any model
whatsoever.  If in addition the model is `natural' or `significant' in
some sense (e.g. the upper half plane model), then that's a bonus.

My recollection of the history here is that the first model of B-L
geometry to be discovered was also a natural model in this sense.
(Was it the upper half plane model?)  Thus, as a matter of historical
fact, both consistency of B-L and the existence of a natural model of
B-L were established at the same time.  But it's wrong to identify
these two conclusions as equivalent to each other.  Perhaps this is
the source of Tragesser's perplexity.

 > Is this now an irrelevant sense of "consistency"

To identify `consistency' with `having a natural model' is not so much
irrelevant as it is incorrect and confusing.

 > or does the activity "integrating significanlty into accepted
 > mathematics" have no interest now?

When a theory has some sort of natural model, that is of course
interesting.  But to conflate this notion with consistency will lead
to endless confusion.

 > Reverse mathematics gives us much surprising information about
 > _logical equivalences_ and or especially _logical equivelences
 > mod..._ But it does seem that we do not understand very well in
 > f.o.m. what is lost through these equivalences (when one
 > substitutes one for the other). . .crudely called the inensional
 > content

I'm well aware of this limitation of reverse mathematics.  However, a
similar criticism applies to any mathematical classification project
whatsoever.  If x and y fall into one class while z falls into a
different class, then one can always ask for a finer classification
scheme.  However, this does not invalidate the original scheme.

-- Steve