[FOM] First-order arithmetical truth

[Harvey Friedman]

On 10/20/06 7:32 PM, "Arnon Avron" <aa at tau.ac.il> wrote:

>But what is so special about PA? The only
> interest in PA is due to the fact that it codifiersd a part of what
> we know to be true about the natural numbers ("the intended model").

We should be able to prove that PA is complete in various relevant senses.

> For many years I maintain that the appropriate language
> for formalizing logic and mathematics is neither the first-order
> language nor the second-order one. The first is too weak for
> expressing what we all understand, the second involves too strong
> ontological commitments. The adequate language
> is something  in the middle: what is called "ancestral logic"
> in Shapiro's book "Foundations without Foundationalism". This logic
> is equivalent to weak second-order logic (as is shown
> in Shapiro's book, as well as in  his chapter in Vol. 1 of the
> 2nd ed. of the Handbook of Philosophical logic).

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 had some particularly convenient proofs using nonstandard
models of basically the same results. He published his after a lead up of
many years of partial results, so not many people knew the situation. His
publication predates my rediscovery.

The whole matter of what is so special about first order logic needs to be
revisited in a much deeper way.

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.

2. Codify this in terms of conditions on a "logic".

3. Prove that any "logic" obeying these conditions is a mere notational
variant of first order logic.

Harvey Friedman