带恢复算子的非经典逻辑语义研究:否定
计算机科学中的逻辑
2023-07-25 v3 逻辑
摘要
我们研究为带有特殊一元联结词(称为恢复算子)的(量化)非经典逻辑族提供自然语义的数学结构,这些恢复算子使我们能够以受控方式“恢复”经典逻辑的性质。这些结构称为拓扑布尔代数,即带有附加运算的布尔代数,这些运算满足特定拓扑性质的条件。本研究聚焦于否定这一范式情形。我们展示这些代数如何恰当地为某些次协调的形式不一致逻辑族与次完全的形式不确定逻辑族提供语义。这些逻辑带有恢复算子,用于标记在与非经典否定交互时表现“经典”的命题。与传统以自然语言(辅以数学简写)开展的语义研究不同,我们的形式元语言是一个存在自动化推理工具的高阶逻辑(HOL)系统。在我们的方法中,拓扑布尔代数通过其Stone型表示被编码为集合代数。我们利用高阶元逻辑定义并互关联了一元集合运算上的若干变换,这些变换自然导出一个对立拓扑立方体。此外,我们的方法能够对命题、一阶与高阶量化(包括常域与变域限制)进行统一刻画。通过本工作,我们旨在倡导利用自动定理证明技术开展非经典逻辑的计算机辅助研究。本文呈现的所有结果均已使用Isabelle/HOL证明助手形式化验证,且在许多情况下由该助手求得。
引用
@article{arxiv.2104.04284,
title = {Semantical Investigations on Non-classical Logics with Recovery Operators: Negation},
author = {David Fuenmayor},
journal= {arXiv preprint arXiv:2104.04284},
year = {2023}
}