[FOM] First Order Logic/status

[Harvey Friedman]

FOL (through its practically driven variants) is the only appropriate
vehicle for the foundations of mathematics. I doubt if many people would
disagree with this. The only issue is how to go about carefully formulating
just what this means.

I wrote:

>> We should be able to prove that PA is complete in various
>> relevant senses.
> 
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 wrote:

>> We rediscovered the simple semantic conditions on a "logic"
>> that forces it  to be semantically equivalent to first
>> order logic - it is due to Per
>> Lindstrom. 
> 
I also wrote that these results don't get at the heart of the matter of what
FOL is doing for foundations. That is what is missing. And I have no doubt
whatsoever that one will come to the same conclusion. That FOL (and variants
driven by practical considerations) is the unique way to go about
foundations of mathematics.

I wrote:
> 
>> We should be able to
>> 
>> 1. Analyze with extreme care just what first order logic does for
>> foundations of mathematics. It does things that are not done
>> by the kind of
>> alternate logics you are discussing.
> 
Avron wrote:
> 
> Ancestral logic
> Weak second-order logic
> omega-logic
> FOL+ the quantifier "there exist infinitely many"
> 
> Equivalences of this sort is perhaps the main reason
> all (or most) of us believe in CT.
> 

All of these "logics" are useful for FOM only in so far as they are, in
actual applications to FOM, merely notational variants of FOL. The
fundamental entity is still FOL. Using the word "logic" for them has
primarily served to cause confusion. OF COURSE, from a semantic point of
view, there is no confusion, and these are clearly meaningful entites of
interest independently of FOL. But still, from a semantic point of view, it
would be best to use the word "semantic system" or "semantic framework"
rather than "logic".

Once again, I emphasize that confusion about the status of FOL is merely an
artifact of not being sufficiently careful about analyzing just what job a
"logic" is supposed to do - and can be expected to do - for foundations of
mathematics. 

One can obviously pack various mathematical ideas into the "logic". Taking
this to the extreme would be to simply blur the distinction between "logic"
and "axioms/rules for mathematics", by even calling ZFC the "logic"!

When taken to that extreme, it looks and sounds like a ridiculous use of the
word "logic". 

There is really no point in taking just some mathematical ideas - and not
others - and throwing them into the "logic".

On the other hand, if you have hardly anything - say propositional logic
only - then the "logic" doesn't do the job it is supposed to do for
foundations of mathematics. Specifically, one cannot use it to "formalize
mathematics". 

Therefore one is led to the notion of the "logic" being neutral to subject
matter, putting the non neutral stuff outside the "logic", e.g., into the
axioms for mathematics.

This leads to a notion of "full substitutability" which FOL satisfies.
However, presumably, anything parading as a "logic" that has "full
substitutability" is reducible to FOL in the sense appropriate for this
discussion.

Harvey Friedman