Restricted induction principle
Paul Blain Levy
p.b.levy at cs.bham.ac.uk
Sun Jun 14 00:50:03 EDT 2020
Correction:
On 13/06/2020 21:10, Paul Blain Levy wrote:
> Hi,
>
> I'm puzzled about the strength of a restricted induction principle in
> subsystems of second order arithmetic.
>
> Recall that, for a formula of the form Forall x,X. P(n,x,X), the
> ordinary induction principle is as follows:
>
> Forall x,X. P(0,x,X) and
>
> Forall n. ( (Forall X. P(n,x,X)) => (Forall X. P(n+1,x,X)) ) implies
>
> Forall n,x,X. P(n,x,X).
The restricted induction principle I want to consider is the following
*inference rule*.
[Cf. Parsons "On n-quantifier induction", which distinguishes between
induction axiom schemes and induction inference rules.]
From
>
> Forall x,X. P(0,x,X) and
>
> Forall n, X. ( (Forall x,y. P(n,x,{z | Q(n,x,X,y,z) })) => P(n+1,x,X) )
infer
>
> Forall n. Forall x,X. P(n,x,X).
>
> My questions are as follows.
>
> Q1. Take ACA_0 extended with restriction induction for arithmetical P
> and Q. Is this stronger than ACA_0? In particular, can it prove
> Con(PA)?
>
> Q2. Take RCA_0 extended with restricted induction for P and Q that
> are Delta_0(PRA), i.e. that contain only restricted quantifiers but
> may use all primitive recursive functions. Is this stronger than
> RCA_0? In particular, can it prove Con(PRA)?
>
> I suspect the answer to Q1 is yes but I have no idea about Q2.
>
> Paul
>
>
More information about the FOM
mailing list