A shorter proof of a recent result by R. Di Paola (Q2266712)

A formula F(v) of PA is said to be extensional if \(\vdash x\leftrightarrow y\) implies \(\vdash F(\bar x)\leftrightarrow F(\bar y);\) in this case, if p is a fixed point of F(v), i.e. if \(\vdash p\leftrightarrow F(\bar p),\) then so is every q provably equivalent to p. In a recent paper [Proc. Am. Math. Soc. 91, 291-297 (1984)] \textit{R. A. Di Paola} has proved that, if \(\dot Thm(v)\) is the standard extensional formula numerating the set of theorems, there is a term t(x) such that the formula \(\neg \dot Thm(\overline{t(\bar x)})\) is nonextensional in a very strong sense. The result is relevant for an algebraic approach to fixed points and incompleteness phenomena. In this paper another proof of this result is presented, which is shorter than Di Paola's. A generalization to nonsound extensions of PA is also discussed.