Extensional Independence

TL;DR

This paper investigates the existence of extensional formulas that are independent over PA, proving non-existence for certain types and providing positive results under weaker conditions, advancing understanding of independence and extensionality in formal theories.

Contribution

It establishes the non-existence of extensional Rosser formulas of any complexity and offers positive results for weaker forms like Consistent Extensionality and Conditional Extensionality.

Findings

No extensional Rosser formulas of any complexity exist.

Positive results for formulas satisfying Consistent Extensionality.

Negative results for intensional versions under Conditional Extensionality.

Abstract

Joel Hamkins asks whether there is a $\Pi^0_1$-formula $\rho(x)$ such that $\rho(\phi)$ is independent over ${\sf PA}+\phi$, if this theory is consistent, where this construction is extensional in $\phi$ with respect to ${\sf 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 *Consistent Extensionality*. We also prove that we can demand the negation of $\rho$ 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.