  We introduce a proof-theoretic method for showing nondefinability of
second-order intuitionistic connectives by quantifier-free schemata. We apply
the method to confirm 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 more resilient to changes in metatheory than common semantic
approaches, whose robustness tends to waver once we pass to non-classical and
especially anti-classical settings. Furthermore, we can easily transcribe the
problem-specific subproofs into univalent type theory and check them using the
Agda proof assistant.
