0
$\begingroup$

Peano Arithmetic consists of axioms $P_1, P_2, \ldots P_7$ plus first order classical logic. Let us call this theory $T$. This theory has its unprovable Gödel’s sentence $G$ such that $$ G\leftrightarrow \sim\mathrm{Prov}_T(⌜G⌝) $$ (Needless to say $\mathrm{Prov}_T(⌜G⌝)$ means $G$ is provable in $T$.)

We can add all the instances of the reflection schema to $T$: $$ \mathrm{Prov}_T(⌜\phi⌝) \to \phi $$ This new theory proves $G$, but has its own unprovable Gödel’s sentence $G’$.

Let $U$ be a theory consisting of $P_1, P_2, \ldots P_7$ plus $\mathrm{Prov}_T(⌜\phi⌝) \to \phi $.

My question is this. How do we add the reflection schema to a theory such that the proof predicate $\mathrm{Prov}_U(\cdot)$ includes the reflection schema itself. Would the following do the trick? $$ P_8: P_1\; \& \;P_2 \;\& \;\ldots \;\&\; P_7 \;\& \;\mathrm{Prov}_T(⌜\phi⌝)\to \phi $$ Is there any publication that addresses this issue?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ Note that your $P_8$ isn't a single sentence, since we need a separate instance of it for each $\phi$ (or at least for each level of the arithmetical hierarchy). $\endgroup$
    – Noah Schweber
    Commented Mar 29, 2022 at 18:46

1 Answer 1

Reset to default
2
$\begingroup$

The best introductory source for reflection principles and their iterations that I know is the survey by Lev Beklemishev [1].

[1] Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2), 197.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .