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.

翻译：我们引入了一种证明论方法，用于证明二阶直觉主义联结词无法通过无量词模式来定义。应用该方法，我们证实了Taranovsky的“可实现性析取”联结词不承认无量词定义，并借此获得了关于Kreisel与Połacik一元联结词不可定义性的新结果及更细微的信息。我们的方法具有有限性和组合性，因此相较于常见的语义方法，在元理论变化时更具鲁棒性——后者一旦进入非经典乃至反经典设定，其稳健性往往摇摆不定。此外，我们还能将问题特定的子证明轻松转录为单值类型理论，并使用Agda证明辅助工具进行检验。