Several recent results bring into focus the superintuitionistic nature of most notions of proof-theoretic validity, but little work has been done evaluating the consequences of these results. Proof-theoretic validity claims to offer a formal explication of how inferences follow from the definitions of logic connectives (which are defined by their introduction rules). This paper explores whether the new results undermine this claim. It is argued that, while the formal results are worrying, superintuitionistic inferences are valid because the treatments of atomic formulas are insufficiently general, and a resolution to this issue is proposed.
翻译:近期多项研究聚焦于大多数证明论有效性概念的超直觉主义性质,但鲜有工作评估这些结论的后果。证明论有效性声称能够提供一种形式化解释,说明推理如何源于逻辑连接词的定义(这些连接词由其引入规则定义)。本文探讨这些新成果是否动摇了这一主张。本文认为,尽管形式化结果令人担忧,但超直觉主义推理仍然成立,因其对原子公式的处理不够普遍化,并就此问题提出了解决方案。