Restricted induction principle

[Paul Blain Levy]

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
>
>