限定公式、失败即否定与直觉主义命题逻辑的基础扩展语义
计算机科学中的逻辑
2023-03-30 v2 逻辑
摘要
证明论语义学（proof-theoretic semantics, P-tS）是一种语义学范式，其中逻辑的意义基于证明（而非真值）。直觉主义命题逻辑（intuitionistic propositional logic, IPL）的 P-tS 的一个特定实例是其基础扩展语义（base-extension semantics, B-eS）。该语义由一个称为支持的关系给出，用于解释逻辑常量的意义，该关系由称为基础的规则系统参数化，基础提供了原子命题的语义。在本文中，我们将基础解释为限定公式的集合，并利用由一致证明搜索（逻辑编程（logic programming, LP）的证明论基础）提供的后者的操作视角，来建立 IPL 对于 B-eS 的完备性。这一视角允许将 P-tS 中的一个微妙问题——否定，理解为 LP 中的失败即否定协议。具体而言，虽然命题的否定传统上被理解为其否定的断言，但在 B-eS 中，我们可以将命题的否定理解为未能找到其证明。这样，断言和否定都是 P-tS 中的核心概念。
引用
@article{arxiv.2210.05336,
title = {Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic},
author = {Alexander V. Gheorghiu and David J. Pym},
journal= {arXiv preprint arXiv:2210.05336},
year = {2023}
}
备注
submitted