Proof-theoretic methods in quantifier-free definability

TL;DR

This paper presents a proof-theoretic method to demonstrate the nondefinability of certain second-order intuitionistic connectives without quantifiers, applicable even in non-classical logical frameworks.

Contribution

It introduces a novel, finitary proof-theoretic approach for nondefinability proofs that is adaptable to various logical settings and compatible with formal verification tools.

Findings

Proves Taranovsky's realizability disjunction is not quantifier-free definable.

Provides new insights into the nondefinability of Kreisel's and Polacik's unary connectives.

Method is resilient to changes in metatheory and compatible with univalent type theory and Agda.

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{\l}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.