Proof-theoretic methods in quantifier-free definability
Zoltan A. Kocsis
TL;DR
The paper develops a novel, fully proof-theoretic approach to proving the undefinability of second-order intuitionistic connectives by quantifier-free schemata, grounded in Pitts interpolants and a formally verified Pitts quantifier theorem. It shows that realizability disjunction, Kreisel's star, and Połacik's connective are not definable quantifier-free, using an auxiliary-formula framework that, if definability held, would entail classical reasoning. The authors provide detailed proof-theoretic arguments, extract new corollaries for related logics, and demonstrate that the method yields results that transfer to univalent type theory and can be checked in Agda, highlighting metatheory robustness and practical applicability. The work advances understanding of the definability landscape for both binary and unary second-order connectives and suggests broad avenues for extending the framework to other logical systems and connectives, with potential impact on semantic-independent proofs and type-theoretic formalization.
Abstract
We introduce a proof-theoretic approach to showing nondefinability of second-order intuitionistic connectives by quantifier-free schemata. We apply the method to prove that Taranovsky's "realizability disjunction" connective does not admit a quantifier-free definition, and use it to obtain new results and more nuanced information about the nondefinability of Kreisel's and Połacik's unary connectives. The finitary and combinatorial nature of our method makes it resilient to changes in metatheory, and suitable even for settings with axioms that are explicitly incompatible with classical logic. Furthermore, the problem-specific subproofs arising from this approach can be readily transcribed into univalent type theory and verified using the Agda proof assistant.