[FOM] Are first-order languages adequate for mathematics?

[Arnon Avron]

On Sat, Oct 21, 2006 at 01:31:27PM -0400, Harvey Friedman wrote:
 
> We should be able to prove that PA is complete in various 
> relevant senses.

The only sense I find plausible is to prove that PA
is equivalent in strength to some *natural* axiomatization
of the natural nunbers within a natural (necessarily
incomplete) system for ancestral logic.

 This is a good opprtunity to correct something I wrote in a 
previous message. I suggested
that the special importance that people attach to PA is due
to its being a natural first-order approximation to
the second-order Dedkind-Peano axioms. Actually, it
is not. Peano's axioms are in a (second-order) language in
which the only primitives are a constant 0 and a unary function
S for the successor operation. Accordingly, the *natural* first-order
approximation is the one obtained by replacing the second-order
induction axiom by the first-order induction schema
*in the same language*. However, this really natural system turned out
to be too weak. One cannot define addition (which is the repeated
application of the successor function) in that system. So +
is added to the signature. Still too weak: multiplication
(which is the repeatedapplication of the addition operation)
still cannot be defined. So \times is added too. Luckily,
Goedel has found out that this process need not go for ever,
but by some miracle can be stopped at this unnatural stage.

  Things become clearer in the context of logics with 
operations TC_n for constructing the transitive closure of 
definable 2n-relations. FOL({0,S})+TC_2 suffices for defining all
recursive functions. So does FOL({0,S}+TC_1+addition (but addition
cannot be defined in FOL({0,S}+TC_1). On the other hand,
in the framework of Feferman's FS_0 (where the intended 
structure is the set of S_expresions generated from 0
using a pairing function), FOL({0, <_,_>})+TC_1 does suffice 
for getting all finitary inductive definitions, recursive functions
etc (all these results are proved in my paper: 
"Transitive Closure and the mechanization of Mathematics"
In  the book "Thirty Five Years of Automating Mathematics"
(F. Kamareddine, ed.), 149-171, Kluwer Academic Publishers, 2003).

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

These results are certainly very interesting from a pure 
mathematical point of view. However, the properties that 
characterize FOL according to them are (in my opinion)
proprties which make FOL *inadequate* for the foundations
of mathematics. Skolem-Lowenheim theorem is an unwellcome
result which leads to Skolem paradox, and from there to the 
destructive idea that all the basic concepts of mathematics
are relative. The compactness theorem, in turn, implies 
that no structure which  is constructed by a simple inductive
process can fully be characterized. Now even a dedicated formalist
should be able to identify  valid formal proofs, and so should 
use inductive definitions and reasoning (It seems that Sazonov
disagrees, but I was never able to understand his explnations
concerning this obvious point). Hence FOL cannot be sufficient
even for  formalist foundations of mathematics (in fact FOL
is not even sufficient for its own metatheory!)
 A remark: the compactness theorem is necessarily true
for any logic which has an effective sound and complete 
axiomatization. Having the latter is no doubt a virtue 
for a logic. The compactness theorem for itself is not. So again:
the only advantage of FOL is the fact that it is effectively
axiomatizable. It is definitely a very big advantage, but
using  it for FOM only because of it is like looking for the
lost coin where the light is.

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

As I said, the only thing I can see that it does, which 
the alternate logics I suggest do not, is to have an effective 
axiomatization. The lack of this for ancestral logic
can be compensated by using an incomplete axiomatic
system for this logic which is sound, natural, and
strong enough for developing usual mathematics.
 
  On the other hand I can point to several things that 
ancestral logic does for foundations of mathematics that FOL
does not: It provides a categorical axiomatization
of the natural numbers (and similar structures) without
introducing problematic objects like infinite sets, and
finitary inductive reaoning is a part of its logical aparatus
(can one overemphasize the importance of finitary inductive 
reasoning to foundations of mathematics?). Another result proved
in my paper cited above which is relevant here is the fact
that a relation on the set of S-expressions (Feferman's V_0)
is r.e. *if and only if* it is definable by some formula
in the language which is based on 0, a pairing function,
equality, disjunction, conjunction and TC_1. It is also
possible to prove that a relation on N is r.e. iff it is
definable by some formula in the language based on
0, S, equality, disjunction, conjunction and TC_2,
or 1, +, equality, disjunction, conjunction and TC_1
(in all cases one may add the existential quantifier,
but not negation, implication, or the universal quantifier).
I am not acquainted with any exact correspondence of this
type that FOL (or other languages) can provide.

 Finally, another indication of the special place this logic 
has is the equivalence shown in Shapiro's book "Foundation
without Foundationalism" of the following four logics
(that seem at first sight to be very different from each other):

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.

Arnon Avron




Ancestral logic
Weak second-order logic
omega-logic
FOL+ the quantifier "there exist infinitely many".o


Arnon Avron