Extensional independence

Abstract

Joel Hamkins asks whether there is a $\Pi^0_1$-formula $\varrho(x)$ such that $\varrho(\ulcorner\varphi\urcorner)$ is independent over $\mathsf{PA}+\varphi$, if this theory is consistent, where this construction is extensional in $\varphi$ with respect to $\mathsf{PA}$-provable equivalence. We show that there can be no such extensional Rosser formula of any complexity. We give a positive answer to Hamkins' question for the case where we replace Extensionality by a weaker demand that we call consistent extensionality. We also prove that we can demand the negation of $\varrho$ to be $\Pi^0_1$-conservative, if we ask for the still weaker conditional extensionality. We show that an intensional version of the result for conditional extensionality cannot work.