[FOM] ACA0, PA, PA'

[Harvey Friedman]

Reply to Buckner 9:39AM 5/10/03.

>
>Thanks for your posting.  The technique you use (in your parable about the
>two friends) is well-known to philosophers.

Since you know this, I cannot understand how this failure of 
communication could occur.

We have three systems: PA, PA', ACA0. You have accepted PA and even 
PA' as directly meaningful. We agree that you do not agree that ACA0 
is directly meaningful.

I stated this theorem:

1. There is an interpretation of ACA0 into PA'.

And this fact:

2. Much of real analysis can be directly and naturally developed in 
ACA0, since ACA0 directly talks about infinite sets of natural 
numbers, and has fairly strong set existence principles.

So this provides the kind of workaround for your complaints about 
ACA0. What is the problem?

Also, let me state the following result:

3. ACA0 is a conservative extension over PA. I.e., every sentence in 
the language of PA (i.e., without any sets of natural numbers) that 
is provable in ACA0 is already provable in PA.


>
>My point is that there are other ways of quantifying.  If I am right, there
>is a formal system underlying natural language (call this NL) which uses
>plural reference and quantification.  This can do without certain objects
>implied to exist by ACA0 and PA*.

What is PA*? Do you mean PA'?

The whole point of the interpretation of ACA0 into PA' was to work 
around your view that ACA0 talks about objects that you do not 
accept. You have already indicated that you accept all objects that 
PA refers to. Since PA' doesn't  refer to any *objects* beyond those 
that PA refers to, you have no problem with PA'.

>Thus ACA0 is not necessarily conservative
>over NL.

ACA0 is a conservative extension of PA', and since you accept PA', it 
is a conservative extension of NL.

>I understand this means ACA0 does not prove any theorems that NL
>does not prove (given a suitable translation or "interpretation" of the
>theorems of course).

There are two results relevant here.

i. There is an interpretation of the language of ACA0 into the 
language of PA' that can be spelled out, even if it is long and 
complicated and subtle, where: any theorem of ACA0 becomes a theorem 
of PA' under this interpretation.

ii. Any theorem of ACA0 that does not mention sets is already a theorem of PA.

>And it's clear that ACA0 (for example) must have
>theorems that NL does not have, since it allows us to proves the existence
>of certain sets (e.g. the set {0}) that NL does not.  (Forgive me if I have
>not understood that point).

The relevant fact is that ACA0 states propositions that PA' cannot 
state, since the language of ACA0 is not included in the language of 
PA'.
>
>In particular, there will be some analogue of Cantor's Theorem in ACA0, that
>establishes the existence of an infinite set
>
>  {x in N: x is not in f(x)}

Yes, that is a theorem provided one is using the usual treatment of 
functions from N into subsets of N, or infinite sequences of subsets 
of N, as:

subsets of N in ACA0.

Such treatments are entirely standard.

>
>This, as I have pointed out very mnay times on FOM, is an existence proof.
>We really do need to prove that an object referred to by the curly bracket
expression exists. 

This is provided by the axioms of ACA0.

>... But there need be no such analogue in NL.  There need be no term in NL
>that corresponds to "{x in N: x is not in f(x)}".

That's the whole point. In PA or even in PA' we cannot even state 
this set existence principle, let alone prove it.

However, the point is that we have results i and ii above.

>Which leads to the
>following
>
>CONJECTURE: is there a system whose axioms support real analysis, but which
>do not support the existence of the objects required for Cantor's Theorem
>(i.e. objects such as {x in N: x is not in f(x)}, or any analogue thereof)?

This is a question, not a conjecture.

The answer to your question obviously depends on just what you mean 
by "support". If "support" allows for interpretation, then I have 
already answered this in the affirmative by "ACA0 is interpretable in 
PA'". ACA0 directly supports real analysis, directly supports the 
existence of the objects required for Cantor's Theorem, but PA' does 
not support the existence of the objects required for Cantor's 
Theorem.

However, there are many other ways to interpret your question that 
seem interesting. It is not clear which, if any, you have in mind.

I. There may be a way of doing a substantial amount of real analysis 
directly without the notion of infinite sequence of real numbers. Of 
course, you will find direct talk of infinite sequences of real 
numbers in every real analysis book published in the last n years.

II. There may be a way of doing a substantial amount of real analysis 
directly with the notion of infinite sequence of real numbers, and 
where the usual basic results like "every infinite sequence of real 
numbers omits some real number" are covered, yet covered without the 
usual set existence axioms, or usual real number constructions.

III. There may be a way of doing a a substantial amount of real 
analysis directly with the concepts of real number and infinite 
sequence of real numbers, but without any infinite sets, where the 
existence principles for real numbers used are not a slavish 
imitation of set existence principles.

There are several other combinations of ideas like this that can be proposed.

All such projects have unclear outcomes, but require deep time 
intensive investigations, and are expected to proliferate into many 
deep time intensive subprojects. There are a lot of projects with 
these properties in f.o.m. In particular, there are a lot of projects 
in f.o.m. with these properties that seem likely to have a bigger 
payoff than these, and so my personal priorities lie elsewhere.

I was hoping that you were going to be completely satisfied by the 
interpretation approach, where the smooth and reasonably full 
development is conducted in ACA0, with its fairly strong set 
existence principles, yet ACA0 is interpreted in PA' - and you accept 
PA'.

>
>If the conjecture is true, every object, including every real number, that
>is generated by NL will lie WITHIN the range of some counting function f.
>I.e. every object would be "countable".  This would effectively be a
>solution of CH.

None of this is relevant to CH (continuum hypothesis) as stated by 
Cantor or by Hilbert in his first problem.

>
>In summary, are we absolutely certain that there is not some more limited
>set of assumptions that would suffice for "ordinary mathematics", but not
>suffice for the theorem that the reals are uncountable?

You should focus on the most elementary noncommittal statement of 
"reals are uncountable". This seems to be

"every infinite sequence of real numbers omits some real number".

Avoid cardinality, avoid the set of all real numbers, avoid functions 
with domain the real numbers, etcetera.

Obviously the statement

"every infinite sequence of real numbers omits some real number"

is considered by mathematicians today to be part of "ordinary mathematics".

However, I have no doubt that some interesting kind of restricted 
form of real analysis could be done without getting involved in 
infinite sequences of real numbers. The delicate question is: just 
how much?

>It's absolutely
>certain that using plural quantification we can do without certain axioms.
>Are we certain that these very axioms are not also the ones that generate
>Cantor's Theorem?  Has this ever been proved or examined?  By whom?

I can't respond to this question without seeing some real indication 
of just what axioms you are talking about.

And what does "generate" mean? Are you talking about a system in 
which infinite sequences of real numbers are being discussed, for 
otherwise you cannot even state

"every infinite sequence of real numbers omits some real number".

I close by repeating that: I was hoping that you were going to be 
completely satisfied by the interpretation approach, where the smooth 
and reasonably full development is conducted in ACA0, with its fairly 
strong set existence principles, yet ACA0 is interpreted in PA' - and 
you accept PA'.