FOM: contradiction-free vs consistent

[Vladimir Sazonov]

Stephen G Simpson wrote:
>
> 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?

I mention an example of such a theory below.

> 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.

Yes. But do you predict that this will be the case forever?  
It seems we should not restrict or fix once and for all the 
present logical background of mathematics.

> 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.

As an evidence "against" (which, of course, does not negate the 
"very large amount of evidence for the logicist thesis" with 
which I mostly agree) it may be considered the formal theory of 
feasible numbers about which I wrote to FOM. This actually gives 
an example for (A) and (B) above. Of course, it is impossible to 
formalize the "set" of feasible numbers F in the framework of 
the ordinary FOL. 

What about G"odel's completeness theorem for the logic 
underlying F (which is at least based on the *ordinary* language 
of FOL)? There exists no first order model for the above theory 
of F in the traditional sense of this word. However, the "set" 
of feasible numbers F (which is of course a vague collection) is 
intuitively (even almost really) existing!

On the other hand, instead of G"odel's completeness theorem we 
could adopt the principle of thought (which seems Lobachevsky 
and Bolyai successfully used):

	if there is no formal contradiction in a (natural)
	theory 	T then we can *imagine* a model of T.

G"odel's theorem requires having some sufficiently rich supply 
of possible models. We may have or not have it at the moment.  
ZFC gives a very rich such supply and framework for the 
contemporary model theory, but we may need more.  Probably some 
extension of this supply is possible so that we will have a 
"legal" (in some extended sense) model for F and even 
corresponding version of G"odel's completeness theorem will 
be proved. This situation is somewhat analogous (however, the 
difference is very essential) to that with intuitionistic logic 
and corresponding extension of the class of classical models to 
Kripke models.

.......

>  > 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.

Indeed, could you Robert (or anybody else) please describe these 
theories. Anyway, this does not seem to be something well-known.  
(Unfortunately I also have problems with getting materials via 
my institute library.)

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.

Yes, it is necessary. As to feasibility theory, there have been
some discussion in FOM. Here probably instead of f.o.m. we should
tell about possible foundations of computer science (f.o.c.s.)
and complexity theory (f.o.c.t.) considered as parts of mathematics
where feasibility is (or potentially may be) especially important. 
Thus, as I understand, complexity theory arose exactly from the 
practical necessity to have feasibile computations. 

.......

> 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.

I agree. Moreover, I would replace here also the word "natural" 
by "legal" (i.e. a model in a precise mathematical sense).  
Therefore, I conclude, "consistent" = "contradiction-free" is 
essentially syntactical notion (which is of course usually related 
with some *informal* semantics).  Existence of a "natural" or even 
"legal" model is a secondary issue (a "bonus", if any). 
Identifying informal semantics with "legal" one also "leads to 
endless confusion".


Vladimir Sazonov