Let $\sf PA$ denote the theory of natural numbers with constants $(0, 1)$ and binary operators $(+,\times)$ based on the first-order predicate calculus with equality, having the following axioms, where the last one is the axiom schema of induction yielding an axiom for each wff $\Phi(a)$:

• $a+0=a$
• $a\times1=a$
• $a+(b+c)=(a+b)+c$
• $a\times(b+c)=a\times b+a\times c$
• $a+c=b+c\implies a=b$
• $a+1\ne0$
• $\forall a\,\left(\Phi(a)\implies\Phi(a+1)\right)\implies\left(\Phi(0)\implies\Phi(c)\right)$

Note that $\sf PA$ is powerful enough to introduce Gödel numbering for its own formulae and define the predicate for their provability in $\sf PA$.

Let's use $\sf ZFC$ as a meta-theory to reason about $\sf PA$ and its extensions defined below, and furthermore assume $\sf ZFC$ is consistent.

For any recursively axiomatizable theory $\sf T$, that contains $\sf PA$ as its fragment, define $\sf T^+$ to be a new theory obtained from $\sf T$ by adjoining the following axiom schema yielding an axiom for each wff $\Phi$:

• $\left(\Phi\ \text{is provable in}\ \sf T\right)\implies\Phi$

Note that $\sf T^+$ can prove consistency of $\sf T$, thus, if $\sf T$ is consistent, $\sf T^+$ is stronger than $\sf T$.

Let $\alpha$ range over recursive ordinals, i.e. $\alpha\in\omega_1^{CK}$. Define the countable transfinite sequence of theories $\sf PA_\alpha$ such that:

• $\sf PA_0$ is $\sf PA$
• $\sf PA_{\alpha+1}$ is $\sf PA_\alpha^+$
• for a limit ordinal $\alpha$, $\sf PA_\alpha$ is the theory whose set of axioms is the union of sets of axioms of all $\sf PA_\beta$, where $\beta<\alpha$

Apparently, each of $\sf PA_\alpha$ is recursively axiomatizable. I also believe each of them is consistent, but do not yet see how to prove it.

Question 1: Can we prove it?

Question 2: Does any of $\sf PA_\alpha$ contain a theorem that is not provable in $\sf ZFC$ (when properly translated to the language of set theory, with natural numbers represented as finite von Neumann ordinals, and operators $(+,\times)$ as ordinal addition and multiplication)? If so, what's the least $\alpha$ with this property?

Let $\sf PA$ denote the theory of natural numbers with constants $(0, 1)$ and binary operators $(+,\times)$ based on the first-order predicate calculus with equality, having the following axioms, where the last one is the axiom schema of induction yielding an axiom for each wff $\Phi(a)$:

• $a+0=a$
• $a\times1=a$
• $a+(b+c)=(a+b)+c$
• $a\times(b+c)=a\times b+a\times c$
• $a+c=b+c\implies a=b$
• $a+1\ne0$
• $\forall a\,\left(\Phi(a)\implies\Phi(a+1)\right)\implies\left(\Phi(0)\implies\Phi(c)\right)$

Note that $\sf PA$ is powerful enough to introduce Gödel numbering for its own formulae and define the predicate for their provability in $\sf PA$.

Let's use $\sf ZFC$ as a meta-theory to reason about $\sf PA$ and its extensions defined below, and furthermore assume $\sf ZFC$ is consistent.

For any recursively axiomatizable theory $\sf T$, that contains $\sf PA$ as its fragment, define $\sf T^+$ to be a new theory obtained from $\sf T$ by adjoining the following axiom schema yielding an axiom for each wff $\Phi$:

• $\left(\Phi\ \text{is provable in}\ \sf T\right)\implies\Phi$

Note that $\sf T^+$ can prove consistency of $\sf T$, thus, if $\sf T$ is consistent, $\sf T^+$ is stronger than $\sf T$.

Let $\alpha$ range over recursive ordinals, i.e. $\alpha\in\omega_1^{CK}$. Define the countable transfinite sequence of theories $\sf PA_\alpha$ such that:

• $\sf PA_0$ is $\sf PA$
• $\sf PA_{\alpha+1}$ is $\sf PA_\alpha^+$
• for a limit ordinal $\alpha$, $\sf PA_\alpha$ is the theory whose set of axioms is the union of sets of axioms of all $\sf PA_\beta$, where $\beta<\alpha$

Apparently, each of $\sf PA_\alpha$ is recursively axiomatizable. I also believe each of them is consistent, but do not yet see how to prove it.

Question 1: Can we prove it?

Question 2: Does any of $\sf PA_\alpha$ contain a theorem that is not provable in $\sf ZFC$ (when properly translated to the language of set theory, with natural numbers represented as finite von Neumann ordinals, and operators $(+,\times)$ as ordinal addition and multiplication)? If so, what's the least $\alpha$ with this property?

Update: As pointed out in the comments below, my "definition" of the transfinite sequence $\sf PA_\alpha$ is not really a definition because we have some wiggle room in choosing a specific ordinal notation at limit points (I do not yet completely understand how exactly it can affect the strength of theories in the sequence, but I've started to read a book on this topic — Thanks!). But I believe we still can define the set $\mathcal T$ of all possible transfinite sequences constructed this way (although it is not a singleton set). So, each of my questions can be restated as "Is it the case for at least one sequence in $\mathcal T?$ Is it the case for all sequences in $\mathcal T?$"

Let $\sf PA$ denote the theory of natural numbers with constants $(0, 1)$ and binary operators $(+,\times)$ based on the first-order predicate calculus with equality, having the following axioms, where the last one is the axiom schema of induction yielding an axiom for each wff $\Phi(a)$:

• $a+0=a$
• $a\times1=a$
• $a+(b+c)=(a+b)+c$
• $a\times(b+c)=a\times b+a\times c$
• $a+c=b+c\implies a=b$
• $a+b=0\implies a=0\land b=0$
• $\forall a\,\left(\Phi(a)\implies\Phi(a+1)\right)\implies\left(\Phi(0)\implies\Phi(c)\right)$

Note that $\sf PA$ is powerful enough to introduce Gödel numbering for its own formulae and define the predicate for their provability in $\sf PA$.

Let's use $\sf ZFC$ as a meta-theory to reason about $\sf PA$ and its extensions defined below, and furthermore assume $\sf ZFC$ is consistent.

For any recursively axiomatizable theory $\sf T$, that contains $\sf PA$ as its fragment, define $\sf T^+$ to be a new theory obtained from $\sf T$ by adjoining the following axiom schema yielding an axiom for each wff $\Phi$:

• $\left(\Phi\ \text{is provable in}\ \sf T\right)\implies\Phi$

Note that $\sf T^+$ can prove consistency of $\sf T$, thus, if $\sf T$ is consistent, $\sf T^+$ is stronger than $\sf T$.

Let $\alpha$ range over recursive ordinals, i.e. $\alpha\in\omega_1^{CK}$. Define the countable transfinite sequence of theories $\sf PA_\alpha$ such that:

• $\sf PA_0$ is $\sf PA$
• $\sf PA_{\alpha+1}$ is $\sf PA_\alpha^+$
• for a limit ordinal $\alpha$, $\sf PA_\alpha$ is the theory whose set of axioms is the union of sets of axioms of all $\sf PA_\beta$, where $\beta<\alpha$

Apparently, each of $\sf PA_\alpha$ is recursively axiomatizable. I also believe each of them is consistent, but do not yet see how to prove it.

Question 1: Can we prove it?

Question 2: Does any of $\sf PA_\alpha$ contain a theorem that is not provable in $\sf ZFC$ (when properly translated to the language of set theory, with natural numbers represented as finite von Neumann ordinals, and operators $(+,\times)$ as ordinal addition and multiplication)? If so, what's the least $\alpha$ with this property?

Let $\sf PA$ denote the theory of natural numbers with constants $(0, 1)$ and binary operators $(+,\times)$ based on the first-order predicate calculus with equality, having the following axioms, where the last one is the axiom schema of induction yielding an axiom for each wff $\Phi(a)$:

• $a+0=a$
• $a\times1=a$
• $a+(b+c)=(a+b)+c$
• $a\times(b+c)=a\times b+a\times c$
• $a+c=b+c\implies a=b$
• $a+1\ne0$
• $\forall a\,\left(\Phi(a)\implies\Phi(a+1)\right)\implies\left(\Phi(0)\implies\Phi(c)\right)$

Note that $\sf PA$ is powerful enough to introduce Gödel numbering for its own formulae and define the predicate for their provability in $\sf PA$.

Let's use $\sf ZFC$ as a meta-theory to reason about $\sf PA$ and its extensions defined below, and furthermore assume $\sf ZFC$ is consistent.

For any recursively axiomatizable theory $\sf T$, that contains $\sf PA$ as its fragment, define $\sf T^+$ to be a new theory obtained from $\sf T$ by adjoining the following axiom schema yielding an axiom for each wff $\Phi$:

• $\left(\Phi\ \text{is provable in}\ \sf T\right)\implies\Phi$

Note that $\sf T^+$ can prove consistency of $\sf T$, thus, if $\sf T$ is consistent, $\sf T^+$ is stronger than $\sf T$.

Let $\alpha$ range over recursive ordinals, i.e. $\alpha\in\omega_1^{CK}$. Define the countable transfinite sequence of theories $\sf PA_\alpha$ such that:

• $\sf PA_0$ is $\sf PA$
• $\sf PA_{\alpha+1}$ is $\sf PA_\alpha^+$
• for a limit ordinal $\alpha$, $\sf PA_\alpha$ is the theory whose set of axioms is the union of sets of axioms of all $\sf PA_\beta$, where $\beta<\alpha$

Apparently, each of $\sf PA_\alpha$ is recursively axiomatizable. I also believe each of them is consistent, but do not yet see how to prove it.

Question 1: Can we prove it?

Question 2: Does any of $\sf PA_\alpha$ contain a theorem that is not provable in $\sf ZFC$ (when properly translated to the language of set theory, with natural numbers represented as finite von Neumann ordinals, and operators $(+,\times)$ as ordinal addition and multiplication)? If so, what's the least $\alpha$ with this property?