From: MoeBlee on
On Mar 3, 10:42 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> MoeBlee <jazzm...(a)hotmail.com> writes:
> > But isn't ACA_0 a theory not compatible in strength with PA rather
> > than a theory weaker or equal to PA?
>
> Nope. ACA_0 aka elementary analysis is a conservative extension of PA.

Okay, conservative extension. I don't know how that would leave my
conjecture that PA is not enough for analysis. I guess it would depend
on how that conjecture is more exactly stated. But still, it seems
something must be added to PA (even if only by conservative extension)
to get analysis cooking? No?

MoeBlee
From: Aatu Koskensilta on
MoeBlee <jazzmobe(a)hotmail.com> writes:

> Okay, conservative extension. I don't know how that would leave my
> conjecture that PA is not enough for analysis.

Your original comment was about adequacy for physics. Feferman has
proposed that all mathematics needed, in a strictly logical sense, in
physics can be formalized in theories proof-theoretically reducible to
primitive recursive arithmetic. As for analysis, it may or may not be
that PA is not enough, depending on just what we have in mind.

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: MoeBlee on
On Mar 3, 11:05 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> MoeBlee <jazzm...(a)hotmail.com> writes:
> > Okay, conservative extension. I don't know how that would leave my
> > conjecture that PA is not enough for analysis.
>
> Your original comment was about adequacy for physics. Feferman has
> proposed that all mathematics needed, in a strictly logical sense, in
> physics can be formalized in theories proof-theoretically reducible to
> primitive recursive arithmetic. As for analysis, it may or may not be
> that PA is not enough, depending on just what we have in mind.

Hmm, "proof-theoretically reducible". Here my ignorance in proof
theory is hurting me.

So, help me out, am I not right that "proof-theoretically reducible to
PRA" is some distance from PRA itself?

MoeBlee
From: Aatu Koskensilta on
MoeBlee <jazzmobe(a)hotmail.com> writes:

> So, help me out, am I not right that "proof-theoretically reducible to
> PRA" is some distance from PRA itself?

Consider two theories T and S. We say that T is proof-theoretically
reducible to S w.r.t a class G of statements (e.g. arithmetical
statements) if there's a recursive function f for which the following
hold:

1. If x is (the code of) a proof, in T, of a statement A in the class
G, then f(x) is (the code of) a proof of A in S.

2. The above (1) is provable in S.

Feferman's argues that there are theories T in which we can develop all
the mathematics needed (in a strictly logical sense) for physics that
are proof-theoretically reducible to primitive recursive arithmetic
(w.r.t arithmetical statements, and hence certainly any experimentally
relevant statements).

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: MoeBlee on
On Mar 3, 11:52 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:

> Consider two theories T and S. We say that T is proof-theoretically
> reducible to S w.r.t a class G of statements (e.g. arithmetical
> statements) if there's a recursive function f for which the following
> hold:
>
>  1. If x is (the code of) a proof, in T, of a statement A in the class
>     G, then f(x) is (the code of) a proof of A in S.
>
>  2. The above (1) is provable in S.
>
> Feferman's argues that there are theories T in which we can develop all
> the mathematics needed (in a strictly logical sense) for physics that
> are proof-theoretically reducible to primitive recursive arithmetic
> (w.r.t arithmetical statements, and hence certainly any experimentally
> relevant statements).

Thanks. You've said 'in a strictly logical sense' a few times. Would
you amplify what you mean by that in this context?

MoeBlee