FOM: "Consistent":Three Questions.

[Vladimir Sazonov]

Robert Tragesser wrote:

> [1] TECHNICAL QUESTION.
>         Is there an example of,  or can one prove the existence of,  a
> theory framed in a higher order classical logic [or at least a logic so
> understood that the class of semantical logical consequences and the
> class of syntactic consequences do not coincide;  but hopefully the
> logic and the theory would be nontrivial wrt my question] that is
>         (a) inconsistent,
>         (b) a contradiction is not derivable.


As an "example" of a theory in which "the class of semantical logical
consequences and the class of syntactic consequences do not coincide"
I could recall Parikh's formalization of feasible numbers. His theory
is *practically* contradiction-free and corresponding axioms and
derivable theorems have some intuitive meaning (not always traditional).
(Actually, this theory contains PA.) However, this theory has *no*
model in the ordinary sense of model theory. Therefore it has no
"semantical logical consequences" (unlike "syntactic" ones) if we
understand this traditionally.

Actually, the above question seems to me not very clear but,
nevertheless,
crucial one. We should be more careful with the terms "consistent",
"contradiction", "semantics", "meaning" etc. I am not sure that I
understand what Robert Tragesser means by "consistent" in contrast
to "contradiction-free". I would say that it is "having an intuitive
meaning". I hope that it is clear that I do not consider the above
example as a *real* answer to the above TECHNICAL QUESTION (which is,
by my opinion, not so technical!). It is only a related illustration.

>         I am still wondering if for example supplying the upper
> half-plane model for Bolyai-Lobach. geometry does not _fundamentally_
> (from the point of view of the mathematical achievement or effect) show
> B-L geometry to be "consistent" more in the sense of "consistent with
> mathematics",  that is,  it does bring B-L geometry fully into the fold
> of mathematics.  Hanging out here (if I may speak colloquially) is the
> thought that in a fundamental sense,  consistency proofs ought to lend
> mathematical signficance to a subject whose mathematical significance is
> in doubt.  (Whereas one can worry over the significance of just
> supplying indirectly -- as in Go"del's completeness proof -- a model in
> the natural numbers that has no striking mathematical significance.)

It might seem that *only* after construction of
a model for B-L geometry by using some mathematically well-established
notions and techniques this geometry became mathematically meaningful.
Of course I agree that this step was extremely important. However, much
more important was the first act of "belief" that B-L geometry has
an *intuitive* meaning. Finding a model inside the "ordinary"
mathematics
was essentially a technical problem. I remember a lecture of Prof.
A.D.Alexandrov (a geometrician) where he told that Lobachevsky actually
almost had a model to his geometry because he worked also in terms of
corresponding arithmetization or was very close to that. Probably if
he could *realize* the question of finding a model as important one
he would resolve it easily. But he actually was fascinated by "living"
in that *imaginary world* and by discovering geometrical facts "true"
in that world. Thus, even without any proof that a formal system is
contradiction-free or has a *mathematical model* we may have a very
reasonable mathematical activity. Just deduce formally and compare the
results with your intuition! As I once wrote to fom, the question of
*mathematical semantics*, however very important, is secondary one in
comparison with some naive, may be extremely informal intuition closely
"intertwined" with a formal theory. Anyway, what is "mathematical"
semantics of ZFC? Strictly speaking there is no "mathematical" semantics
in an absolute sense of this word at all. It is always relative. We have
various formal systems and translations between them preserving
admissibility of formal proof rules.

>        Of course,  what I driving me is the great discomfort I've always
> felt with mathematics that is too logic driven,  perhaps because I place
> a great value on understanding in some full or perhaps melodramatic
> sense.

I feel no discomfort with "too logic driven" or "too formal" at all.
This is the very nature of mathematics! Just consider only those formal
systems having intuitive ("melodramatic" or *any* other) meaning.


Vladimir Sazonov