[FOM] ACA0, PA, PA'

[Dean Buckner]

Harvey,

Many thanks for your considerable patience, which I fear is to be
tested again.

Perhaps I didn't understand the concept of "interpretation".  I
understand it as a kind of translation.  If I assent to a proposition
expressed in one language, then I assent to exactly the same
proposition expressed in another language.  Since I agree that grass is
green, then even if a SerboCroat sentence is not meaningful to me, I agree
to what it expresses, so long as it expresses the proposition that grass is
green.  I agree to anything interpretable as something I agree with.

You write:
> 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.

Not at all.  I agree that ACA0 is meaningful.  Even "directly" meaningful!
Of course it means or says something.  I just don't agree with what it says,
that's all.

You say:
> 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'.
>

and also
> 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'.

Who said I accepted PA'?  If it really is possible to interpret certain
existential statements in ACA0 in PA', and if I don't agree with those
statements, then I won't agree with their interpretation either.  Obviously.

I wrote
> >There need be no term in NL [i.e. natural language system]
> >that corresponds to "{x in N: x is not in f(x)}".

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

I'm totally confused by that.  If this set existence principle is a theorem
of ACA0, then can't it also be interepreted as a theorem of PA'?  That's
what I thought you were saying.  And, whatever that theorem is, I don't
agree with it.

You wrote in a previous posting
>PA' ... has no axiom of infinity. However, some predicates on the
>natural numbers are introduced by definition as I indicated. But
>these predicates are NOT used as objects.

They are predicates, so they are objects!  Obviously you can't escape the
force of Cantor's Theorem by turning sets into predicates or some analogue
of that.  My problem, which seems to puzzle you, is based precisely on an
objection to predicates, in particular the idea that we can rewrite "grass
is green" in any of the following ways

    grass satisfies the predicate "is green"
    grass falls under the concept <is green>

or anything similar like that.  Indeed, your presentation of PA' as
containing the following definitions

R(0) if and only if A.
R(n+1) if and only if B(n,R|<=n).

suggests that we are sneakily introducing nasty objects by the back door.
What entity is referred to by the noun phrase "R|<=n"?

Your idea that I accept PA' is based on the fact I accept some sort of
induction.  Does it follow that we cannot accept induction unless we accept
predicates/concept/sets?  I'm very sceptical of that.


What would actually help this discussion a great deal are examples of actual
mathematical proofs that require the extension (of PA into PA') that you
describe.  I will try and prove these without making any assumptions about
sets, concepts, predicates or their analogues.  If I cannot, we've
established something pretty important, and I will shut up.

Dean