[FOM] ACA0, PA, PA'
Harvey Friedman
friedman at math.ohio-state.edu
Sat May 10 13:09:46 EDT 2003
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'.
More information about the FOM
mailing list