A note on the \(\omega\)-incompleteness formalization (Q1337603)

Let \(S\) be a suitable formal theory containing primitive recursive arithmetic and let \(T\) be a formal extension of \(S\). Using Smoryński's notation, let us single out the following propositions (where \(\alpha(x)\) is a formula with the only free variable \(x\)): (a) (for any \(n\)) (\(\vdash_ T \alpha (\overline {n}))\), (b) \(\vdash_ T \forall x \text{Pr}_ T (^ - \alpha (\dot x)^ -)\), and (c) \(\vdash_ T \forall x \alpha(x)\). The main conclusions of the paper are: 1. the schema corresponding to (b) \(\Rightarrow\) (c) is equivalent to \(\neg \text{Cons}_ T\), and 2. the scheme corresponding to (a) \(\Rightarrow\) (b) is not consistent with the uniform \(\omega\)-consistency schema restricted to PR-formulas.