Proof-theoretic semantics (P-tS) is the approach to meaning in logic based on 'proof' (as opposed to 'truth'). There are two major approaches to P-tS: proof-theoretic validity (P-tV) and base-extension semantics (B-eS). The former is a semantics of arguments, and the latter is a semantics of logical constants. This paper demonstrates that the B-eS for intuitionistic propositional logic (IPL) encapsulates the declarative content of a version of P-tV based on the elimination rules. This explicates how the B-eS for IPL works, and shows the completeness of this version of P-tV.
翻译:证明论语义学是一种基于"证明"(而非"真值")的逻辑意义理论。该领域存在两种主要研究路径:证明论有效性与基扩展语义。前者关注论证的语义解释,后者聚焦逻辑常项的语义分析。本文论证了直觉主义命题逻辑的基扩展语义能够完整封装基于消去规则的证明论有效性变体的陈述性内容。这一发现既阐释了直觉主义命题逻辑基扩展语义的运作机制,也证明了该证明论有效性变体的完备性。