二维相继式演算中所有*连接词的推理行为语义
Inference-Behaviour Semantics for All$^\ast$ Connectives in Two-Dimensional Sequent Calculi
浏览论文内容
中文总结 AI 辅助
研究二维相继式演算中连接词语义，基于推理行为语义方法，通过应用于10816个连接词规则对，找到21个连接词语义子句，描绘其语义关系，发现直觉主义否定、析取和蕴涵各捕捉经典对应物一半意义。
中文摘要 AI 辅助
推理行为语义（I-bS）是一种新的证明论语义学方法，基于两个推理主义原则：（1）表达式在推理中的使用决定其意义，（2）连接词由其运算规则定义。I-bS通过根据子结构最小可推导关系测量连接词在其可定义性证明中的句法使用来实现这些想法。I-bS由此根据其语义子句（即最小子结构规则对）给出连接词的意义。本文通过将I-bS应用于二维相继式演算中最多使用两个前提相继式和最多两个活跃公式可制定的所有10816个连接词规则对来验证和检验I-bS。结果，我们找到了恰好21个有意义连接词的语义子句，包括底、顶、两个否定（直觉主义和对偶直觉主义）、群和格合取、析取和蕴涵及其逆和反。我们利用这些结果精确地描绘了线性、经典、直觉主义、对偶直觉主义、最小和格逻辑中连接词之间的语义相互关系。最显著的是，我们发现直觉主义否定、析取和蕴涵各自捕捉了其经典对应物意义的一半。
英文摘要
Inference-behaviour semantics (I-bS) is a new approach to proof-theoretic semantics, grounded in two inferentialist principles: (1) the use of an expression in reasoning determines its meaning, and (2) a connective is defined by its operational rules. I-bS operationalises these ideas by measuring the syntactic use of a connective in the proof of its definability, against a substructurally minimal derivability relation. I-bS thereby gives the meaning of a connective in terms of its semantic clause, i.e. minimal substructural rule pair. This paper validates and verifies I-bS by applying it to all $10,816$ connective rule pairs that can be formulated in two-dimensional sequent calculi using at most two premiss sequents and at most two active formulae. As a result, we find semantic clauses for exactly $21$ meaningful connectives, namely bottom, top, two negations (intuitionistic and dual-intuitionistic), group and lattice conjunction, disjunction and implication, as well as their converses and inverses. We use these results to precisely map the semantic interrelations among the connectives, across linear, classical, intuitionistic, dual-intuitionistic, minimal, and lattice logic. Most notably, we find that intuitionistic negation, disjunction and implication each capture half of the meaning of their classical counterparts.
