具有强一致性算子的次协调逻辑的证明论方面
逻辑
2023-04-25 v1
摘要
为开发用于不一致性自动推理(定理证明器)的高效工具，并最终使形式不一致逻辑(Logics of Formal inconsistency, LFI)成为在不确定性下推理更具吸引力的形式体系，重要的是发展此类LFI一阶版本的证明论。在我们的工作中，我们意在朝该方向迈出第一步。另一方面，Ciore逻辑被开发出来以从LFI视角为不一致数据库研究提供新逻辑系统。关于Ciore一个有趣的事实是它拥有一个强一致性算子，即一种(前向/后向)传播不一致性的一致性算子。此外，它还是一个可代数化逻辑(在Blok与Pigozzi意义上)，可通过一个3值逻辑矩阵来刻画。近来，定义了Ciore的一阶版本即QCiore，保留了Ciore的精神，即不引入量词之间非预期的关系。此外，针对该逻辑已获得一些重要的模型论结果。本文我们分别研究Ciore与QCiore的一些证明论方面。首先，我们为Ciore引入一个双侧相继式系统。随后，我们证明该系统具有切割消除性质，并应用它推导一些有趣的性质。之后，我们将上述系统扩展到一阶语言，并利用著名的Sh"utte技术证明完备性与切割消除性质。
引用
@article{arxiv.2304.11481,
title = {Proof-theoretic aspects of paraconsistency with strong consistency operator},
author = {Victoria Arce Pistone and Martín Figallo},
journal= {arXiv preprint arXiv:2304.11481},
year = {2023}
}