[FOM] First Order Logic/status

[Arnon Avron]

On Tue, Oct 24, 2006 at 10:00:59PM -0400, Harvey Friedman wrote:

> FOL (through its practically driven variants) is the only appropriate
> vehicle for the foundations of mathematics. >

I should admit that I cannot refute any of the arguments
you gave so far for this very assertive declaration...

> I doubt if many people would  disagree with this. 

Unfortunately, I have never found a fact of this sort as a sufficient
reason to accept something as true. Do you have a better argument?

> >> 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 suggest to wait till they are found before we 
derive any  conclusion from them.
 
> 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.

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.

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

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.
 
  As for ancestral logic being "merely a notational variant of FOL"
(in "actual applications to FOM"), can you explain in what sense?
TC cannot be defined in FOL. But you know this of course - so
obviously you have something different on your mind here. What?

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

I perfectly agree that the word "logic" is frequently used in a careless
way, and it is often confused with what you call "semantic framework"
(which is, I guess, a formal language +  some semantics for it).
In general, a logical system consists of a (formal) language,
and   consequence relations defined on its (either semantically or
proof-theoretically, or even by some other method). These 
consequence relation(s) should be closed under uniform substitions.
(I guess this is what you meant by "full substitutability". Again
I perfectly agree that this is an absolutely necessary criterion,
even though it is somewhat vague. The notion of "substitution" of
formulas used in first-order languages is not identical 
to that used in propositional languages - and I do not
know any general, language-independent definition of
"full substitutability").  ZFC fails even this test.

 Now I agree also that to deserve the name LOGIC even this is not 
enough. A real logic should indeed, as you say below (and I cannot
agree more), be neutral to subject matter. So it seems that the
main thing we dont agree about is what concepts are "neutral".
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. 
   

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

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. 

  The *minimal* requirement from a logic that does the job is that
it provides all the means for defining and reasoning without
which one cannot even start to talk about formal systems
and proofs. Ancestral logic is the minimal logic that meets
this condition, and it is understood, accepted and used by 
everyone (whatever her/his philosophical views are). Hence it
should be a part of any logic for FOM (or any other discipline).

 Let me add that I know
no stronger logic that is also understood, accepted and used by
everyone. Thus at least I cannot accept second-order "logic" as a logic,
because I am not a platonist, while the quantification
in 2nd order logic involves ontological commitments
to a definite world of sets (or "properties" or whatever).
This means, first of all, that 2nd-order logic is *not* neutral. 
For me it is also not reliable enough, because I am not sure
what are the entities it talks about.

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

I do not know what is this sense. Can you elaborate? Thus ancestral
logic has "full substitutability" (if I understand correctly
what you mean by this. If not - please explain this notion),
and it is not reducible to FOL in any sense that *I* would
find appropriate for this discussion.

Arnon Avron