[FOM] First Order Logic/status

[Harvey Friedman]

On 10/27/06 6:16 AM, "Arnon Avron" <aa at tau.ac.il> wrote:

>> When I wrote this, what I clearly had in mind is that, e.g., there is no
>> simple sentence in the language of PA that is undecided in PA. There will be
>> a number of (difficult) results of this kind.
> 
> I suggest to wait till they are found before we
> derive any  conclusion from them.

We can already derive conclusions from what is generally believed. What is
generally believed may be very hard to prove, however. Here is what is
generally believed:

***Under any reasonable measure of complexity of sentences in the language
of PA, any sentence or scheme in the language of PA of modest complexity is
either provable or refutable in PA.***
 
> Again, I find it very difficult to refute the arguments you
> have brought so far for this belief of yours. However, I do agree that
> *up to now*  there are *no* results (except Goedel's completeness theortem)
> that show that FOL is doing much for the foundations
> of mathematics, or that it is "the unique way". On the other
> hand there are many results that show that not only it is
> not the "unique" way: it is not a way at all. For me, just
> the fact that one should go beyond FOL even in order to describe
> and reason about the *syntax* of FOL (to say nothing about
> its proof theory)  makes it clear that it cannot be sufficient
> for the foundations of mathematics. Suggesting so only
> inevitably leads to people thinking that there is even no unique
> structure of the natural numbers, and so that mathematics
> can have no foundations at all.

The job FOL does for the foundations of mathematics is to make a clear
distinction between the logical part of mathematics and the nonlogical part
of mathematics. I claim that this distinction is well worth making and that
there is a sense in which only FOL and practically driven variants
accomplish this. 

We definitely need some theorems about this setup. I expect that they will
be forthcoming. 

Under FOL, we have a standard working foundations of math in the form of
ZFC. This, on top of FOL, constitutes a very modest amount of complexity.
ALSO: we know through proof assistants that theorem proving can be made
entirely practical, in that one can actually create files of reasonable size
that are formal proofs of very serious theorems. People have created such
files. 

There will be a theorem to the effect that if we substantially weaken FOL,
then one cannot accomplish all this. Since we can, in fact, accomplish all
this using FOL, we see that FOL has a special status here. I see no point in
opening the door to any substantial extension of FOL, as there appears to be
no place to draw the line.

> At least Ancestral logic is more than only a semantic framework. It
> has natural proof systems too. They are incomplete - but so is
> also PA, and yet you seem to think that PA is natural and important
> for foundations of mathematics.

PA is important for reasons quite different than FOL. PA is essentially
complete (results have not been obtained on this yet).

*I simply do not have the time now to try to answer your many reasonable
questions. I hope to revisit this matter in a more thorough way at a later
time.*  
 
> To me it seems clear that the thinking process that leads
> from "on" to "above", or from "child of" to "descendant", and the
> inductive reasaoning that this process involves, are no less
> neutral than "for all" or "exists". It is completely universal.
> Now in a non-mathematical discourse it is usually expressed
> by the words "and so on", or by what I call the logic of "...".
> Ancestral logic captures exactly this, and so is (in my opinion)
> no less neutral than FOL.

I would be interested in going down this path if I saw any indication that
there are not many more such things that you or people with your viewpoint
would latter say are "neutral" or "completely universal". E.g., why not the
notion of set of things, or finite set of things?

To me, we are all better off cutting the pie where we normally cut it. It is
probably no coincidence that if you cut the pie differently, pushing more
into "logic", then we lose complete axiomatizability. but I agree that I
don't yet know how to argue in a convincing way that we MUST NOT give up
complete axiomatizability. One can make the argument, but can we make the
argument more compelling?
>  
> And FOL does not do the job either. Again: it is inadeqate for dealing
> with the most basic concepts of mathematics: the natural numbers,
> strings of symbols, formal proofs, etc.

What you describe there is not the job of FOL. E.g., set theory is not the
job of FOL, nor is the theory of integers and of real numbers.

Harvey Friedman