2025-11-23T10:43:16.773800

T-BAT semantics and its logics

Pawlowski
\textbf{T-BAT} logic is a formal system designed to express the notion of informal provability. This type of provability is closely related to mathematical practice and is quite often contrasted with formal provability, understood as a formal derivation in an appropriate formal system. \textbf{T-BAT} is a non-deterministic four-valued logic. The logical values in \textbf{T-BAT} semantics convey not only the information whether a given formula is true but also about its provability status. The primary aim of our paper is to study the proposed four-valued non-deterministic semantics. We look into the intricacies of the interactions between various weakenings and strengthenings of the semantics with axioms that they induce. We prove the completeness of all the logics that are definable in this semantics by transforming truth values into specific expressions formulated within the object language of the semantics. Additionally, we utilize Kripke semantics to examine these axioms from a modal perspective by providing a frame condition that they induce. The secondary aim of this paper is to provide an intuitive axiomatization of \textbf{T-BAT} logic.
academic

T-BAT semantics and its logics

基本信息

  • 论文ID: 2510.14361
  • 标题: T-BAT semantics and its logics
  • 作者: P. Pawlowski
  • 分类: cs.LO (计算机科学-逻辑)
  • 发表时间/会议: Logique et Analyse 264 (2023), 335–356
  • 论文链接: https://arxiv.org/abs/2510.14361

摘要

T-BAT逻辑是一个旨在表达非正式可证明性概念的形式系统。这种可证明性与数学实践密切相关，经常与形式可证明性形成对比，后者被理解为在适当形式系统中的形式推导。T-BAT是一个非确定性四值逻辑。T-BAT语义中的逻辑值不仅传达给定公式是否为真的信息，还传达其可证明性状态。本文的主要目标是研究所提出的四值非确定性语义，深入探讨语义的各种弱化和强化与它们所诱导的公理之间相互作用的复杂性。通过将真值转换为在语义对象语言中表述的特定表达式，证明了在此语义中可定义的所有逻辑的完备性。此外，利用Kripke语义从模态视角检验这些公理，提供它们所诱导的框架条件。论文的次要目标是为T-BAT逻辑提供直观的公理化。

研究背景与动机

问题定义

该研究要解决的核心问题是如何形式化表达数学中的"非正式可证明性"（informal provability）概念。在数学实践中存在两种不同的可证明性概念：

  1. 形式可证明性：严格的语法概念，基于特定形式语言和公理框架，通过有限的公式序列进行形式推导
  2. 非正式可证明性：与数学实践密切相关，数学家实际使用的证明方式，包含语义和语用成分

问题重要性

这个问题重要性体现在几个方面：

  • 形式可证明性与非正式可证明性在推理行为上存在本质差异
  • 反射模式（reflection schema）□φ→φ在非正式可证明性中有效，但在表示形式可证明性的模态逻辑GL中无效
  • 直接将反射模式的所有实例与其他直观的可证明性原理结合会导致一阶算术理论的不一致性

现有方法局限性

现有方法的主要局限性包括：

  • 传统模态逻辑GL虽然能准确刻画形式可证明性，但无法处理非正式可证明性的反射原理
  • 简单地添加反射模式会导致理论不一致
  • 缺乏能够同时处理真值和可证明性状态的精细化框架

研究动机

本文的研究动机是开发一个类似于Kripke真值理论方法论的非正式可证明性理论，通过使用有良好动机的非经典逻辑作为背景逻辑来解决不一致性问题。

核心贡献

  1. 提出了T-BAT四值非确定性语义：将数学命题的真值状态与可证明性状态分离，创建了更精细的逻辑框架
  2. 系统研究了语义的各种强化和弱化：通过方法论系统地探索了连接词的不同解释及其诱导的公理
  3. 证明了所有可定义逻辑的完备性：通过将真值转换为对象语言中的特定表达式实现完备性证明
  4. 建立了与Kripke语义的联系：为各种公理提供了相应的框架条件，从模态逻辑视角分析这些公理
  5. 提供了T-BAT逻辑的直观公理化：纠正了之前文献中的错误，给出了正确的公理化系统

方法详解

任务定义

本文的任务是为非正式可证明性提供一个完整的逻辑框架，包括：

  • 定义适当的语义结构
  • 建立语法和语义之间的对应关系
  • 证明系统的健全性和完备性

模型架构

四值语义设计

T-BAT使用四个逻辑值来表示数学命题的不同状态：

  • P: 真且可证明的命题
  • t: 真且独立的命题（既不可证明也不可反驳）
  • f: 假且独立的命题
  • R: 假且可反驳的命题

指定值集合为D = {P, t}，体现了真值保持的直觉。

非确定性矩阵（Nmatrix）

T-BAT的核心是非确定性矩阵MT = (ValT, DT, OT)，其中：

否定真值表：

¬(φ) | φ
-----|----
  R  | P
  f  | t  
  t  | f
  P  | R

模态算子真值表：

□(φ) | φ
-----|-------
  P  | P
{f,R}| t
{f,R}| f
  R  | R

蕴含真值表：

→  | P | t     | f     | R
---|---|-------|-------|---
P  | P | t     | f     | R
t  | P |{P,t}  | f     | f
f  | P |{P,t}  |{P,t}  | t
R  | P | P     | P     | P

技术创新点

1. 真值与可证明性的分离

与传统三值逻辑（BAT, CABAT）不同，T-BAT将"既不可证明也不可反驳"的命题进一步细分为真和假两类，实现了更精细的分类。

2. 非确定性语义

通过非确定性真值函数，T-BAT能够区分可证等价的公式，这为研究超内涵性（hyper-intensionality）提供了专门工具。

3. 系统的公理推导方法

通过将真值的含义直接翻译为对象语言中的公式来系统地推导公理。例如，对于否定的第一行：

  • 如果v(φ) = P，则v(¬φ) = R
  • 翻译为公理：□φ→□¬¬φ

实验设置

理论验证方法

本文主要采用理论证明方法，包括：

  1. 健全性证明：通过对公式复杂度的归纳证明
  2. 完备性证明：基于极大一致集和赋值引理
  3. 公理等价性证明：建立不同公理系统之间的等价关系

对比分析

论文将T-BAT与以下系统进行对比：

  • 模态逻辑GL（形式可证明性）
  • 模态逻辑S4, S5
  • 之前的BAT和CABAT系统
  • Omori和Skurt的S4⁻系统

实验结果

主要理论结果

1. 最小逻辑W的完备性

定理1（健全性）：对于任意Γ, φ，如果Γ ⊢W φ，则Γ ⊨W φ。

定理2（完备性）：Γ ⊨W φ当且仅当Γ ⊢W φ。

2. T-BAT逻辑的公理化

T-BAT逻辑被刻画为逻辑W加上以下公理：

  • N1: □φ→□¬¬φ
  • N4: ¬□φ∧φ→¬□¬¬φ
  • B1: □φ→□□φ
  • B7: □¬φ→□¬□φ
  • 以及多个蕴含相关的公理（IPP,P, IPt,P等）

3. 公理等价性结果

事实2：公理ItP,t与公理K在W上等价。

框架条件分析

论文为许多公理提供了相应的Kripke框架条件，例如：

  • 公理N3对应条件：∀x,y xRy → x = y
  • 公理B1对应条件：传递性
  • 公理B7对应条件：∀x,y (xRy → ∃z (xRz ∧ yRz))

系统分类

论文将所研究的公理分为三类：

  1. 在模态逻辑K中可证的公理
  2. 在T中可证但在K中不可证的公理
  3. 在S5中都不可证的公理

相关工作

非确定性语义历史

  • 1930年代：Zich和Zawirski独立发展了非确定性语义
  • 1960年代：Rescher使用非确定性真值函数研究自然语言中的蕴含
  • 现代发展：Avron引入非确定性矩阵（Nmatrix）概念，建立严格的数学框架

模态逻辑中的应用

  • Kearns和Ivlev将非确定性语义应用于模态逻辑
  • 当代逻辑学家进一步发展了这一理论，特别是在非正规模态逻辑中的应用

非正式可证明性研究

论文建立在之前关于BAT、CABAT逻辑系统的工作基础上，特别是Pawlowski和Urbaniak的研究。

结论与讨论

主要结论

  1. T-BAT逻辑为非正式可证明性提供了一个完整且一致的形式框架
  2. 四值非确定性语义能够精确区分数学命题的真值状态和可证明性状态
  3. 系统的公理推导方法揭示了语义强化与公理之间的深层联系
  4. 并非所有相关逻辑都是S4或S5的子逻辑，这具有重要的哲学意义

局限性

  1. 哲学基础：非正式可证明性的概念尚未完全操作化，难以判断各种推理模式的正确性
  2. 实用性：缺乏确定哪些T-BAT扩展适用于非正式可证明性的标准
  3. 框架条件：对于某些公理无法找到相应的Kripke框架条件

未来方向

  1. 为非正式可证明性概念提供更实质性的刻画
  2. 开发判断推理模式正确性的标准
  3. 探索T-BAT在其他哲学和数学应用中的潜力
  4. 研究超内涵性的进一步发展

深度评价

优点

1. 理论创新性

  • 提出了精细化的四值语义，成功分离了真值和可证明性状态
  • 发展了系统的公理推导方法论
  • 建立了非确定性语义与Kripke语义之间的桥梁

2. 数学严谨性

  • 提供了完整的健全性和完备性证明
  • 系统地分析了所有可能的语义强化
  • 建立了精确的数学对应关系

3. 哲学意义

  • 为长期存在的非正式可证明性问题提供了新的解决思路
  • 揭示了数学实践与形式系统之间的深层关系

不足

1. 实用性限制

  • 非正式可证明性概念的操作化程度有限
  • 缺乏实际应用的具体指导

2. 技术挑战

  • 某些公理的框架条件仍未找到
  • 系统的复杂性可能限制其实际应用

3. 哲学争议

  • 关于非正式可证明性本质的哲学争论仍在继续
  • 不同哲学立场可能对系统有不同评价

影响力

1. 学术贡献

  • 为逻辑学和数学哲学提供了新的研究工具
  • 推进了非确定性语义理论的发展
  • 为超内涵性研究开辟了新方向

2. 理论价值

  • 展示了非经典逻辑在解决哲学问题中的潜力
  • 提供了处理不一致性问题的新方法

3. 可复现性

  • 提供了完整的数学定义和证明
  • 方法论清晰，便于后续研究

适用场景

  1. 数学哲学研究：特别是关于证明概念的研究
  2. 逻辑学理论：非确定性语义和模态逻辑的进一步发展
  3. 人工智能：可能在知识表示和推理中有应用潜力
  4. 数学教育：帮助理解形式证明与直观证明的关系

参考文献

论文引用了47篇相关文献，涵盖了逻辑学、数学哲学、模态逻辑等多个领域的重要工作，特别是：

  • Solovay关于可证明性逻辑的经典工作
  • Avron等人关于非确定性矩阵的理论发展
  • Kripke关于真值理论的方法论
  • 作者之前关于BAT逻辑系统的研究

这篇论文为非正式可证明性这一重要哲学问题提供了严格的数学处理，虽然在实用性方面还有待发展，但其理论贡献和方法论创新具有重要的学术价值。