技术摘要：通过证明论语义构建信息的推论主义阐释

1. 问题陈述

尽管“信息”概念对现代社会和信息技术至关重要，但本文指出，目前尚缺乏令人完全信服的逻辑或数学基础来支撑这一概念。现有的方法，特别是那些植根于模型论语义（如情境理论）的方法，依赖于从外部模型推导出的真值条件。作者认为，这种对真值（特别是“真实性论题”）和外部模型的依赖，限制了对复杂、分布式信息生态系统进行推理的能力。他们提出，需要一种框架，其中信息的意义由其在使用中的推论作用决定，而非由其与模型的对应关系决定。

2. 方法论

作者提出了一种基于证明论语义（P-tS）的信息推论主义语义理论，具体利用了基扩展语义（B-eS）。该方法论包含三个相互作用的组成部分：

1. 概念分析（形而上学）： 作者重新诠释了弗雷德·德雷茨基（Fred Dretske）关于信息的形而上学（意向性、真实性、可传递性）。他们用可推理性取代了对真实性的要求。信息不再被定义为模型中为真的事实，而是被定义为可从一组原子规则（即“基”）推导出的单元。
2. 逻辑（形式化）： 本文利用 P-tS 构建了一种关于信息基本单元——**推论元（inferon）的数学逻辑理论。这种方法与情境理论（Barwise, Seligman 等）中的模型论信息元（infon）**形成对照。
   • 推论元： 定义为三元组 $\langle\langle P, \mathcal{P}, b \rangle\rangle$，其中 $P$ 是原子命题或谓词，$\mathcal{P}$ 是局部推论元基（一组原子规则），$b$ 是极性（断言或否认）。
   • 意义： 推论元的意义源自原子规则的全局基和推论元的局部基，而非一阶模型。
   • 逻辑： 作者基于直觉主义逻辑开发了推论元逻辑，扩展了 Sandqvist 针对直觉主义命题逻辑（IPL）的 B-eS 以及 Gheorghiu 对一阶逻辑的扩展。
3. 系统（应用）： 所开发的 P-tS 工具被应用于建模分布式系统。作者调整了“分布式系统逻辑”（LDS）框架（Barwise & Seligman），用推论元基和**推论同态（inferomorphisms）**取代了分类和信息同态。

3. 主要贡献

A. 推论元与推论主义语义

核心贡献是将推论元定义为情境理论中信息元的推论主义对应物。

• 结构： 推论元 $\iota = \langle\langle P, \mathcal{P}, b \rangle\rangle$ 由命题 $P$、局部基 $\mathcal{P}$ 和极性 $b$ 组成。
• 支持关系： 有效性是相对于基 $B$ 通过支持关系 $\Vdash_B$ 定义的。一个原子推论元被支持，当且仅当它在基的全局并集与局部基的并集中是可推导的：$\Vdash_B \langle\langle P, \mathcal{P}, b \rangle\rangle$ 当且仅当 $\vdash_{B \cup \mathcal{P}} \langle\langle P, b \rangle\rangle$。
• 能动性： 该框架引入了代理模态（$[a]$ 和 $\langle a \rangle$）来表示推论能力。一个代理支持推论元的能力取决于环境基与该代理特定基集的并集。

B. 逻辑结果

本文确立了推论元逻辑的形式性质：

• 可靠性与完备性： 作者证明了推论元命题逻辑的定理 11（可靠性）和定理 12（完备性），并调整了 Sandqvist 的证明。这些结果被扩展至一阶情形（定理 11 和 12 的扩展版）。
• （推论元）公理： 引入了一条特定公理来处理局部基与全局支持关系之间的相互作用，确保自然演绎演算与基扩展语义之间的一致性。
• 复合推论元： 该框架允许推论元内部包含逻辑连接词，支持关系通过递归方式定义（图 9）。

C. 信息流与推论同态

本文构建了分布式系统中信息流的推论主义阐释：

• 推论同态： 类似于 LDS 中的信息同态，推论同态是一对函数（$f^\vee$ 作用于项，$f^\wedge$ 作用于谓词），用于在不同基之间保持可推导性关系。
• 通道： 通道被定义为一组共享共同核心（一个中心基）的推论同态族。
• 信息流： 信息流的特征在于通道间推论元之间的约束。如果约束在核心中成立，它便将信息从一个组件传递到另一个组件。
• 站点与语境： 作者引入了站点（推论元原子的有限集）和语境支持关系 $\Vdash^P_B$。这使得能够建模信息流，其中约束通过蕴含和"Inf"规则被内化，而非作为外部语义条件存在。

4. 结果与示例

本文通过多个示例展示了该框架的效用：

• 无火不起烟： 将针对约束的“调谐”形式化为连接推论元基的推理规则。它展示了代理如何基于局部感知（烟）和共享约束，推导出关于远程情境（火）的信息，而无需直接访问远程事实。
• 智者谜题： 使用固定的推论能力对认识论谜题进行建模。代理推理其他代理无法进行推论的情况，展示了该框架如何处理关于推论本身的推理，而无需进行无界的状态空间探索。
• 访问控制： 建模了一个密码和令牌导致访问的系统，说明了约束如何通过蕴含在逻辑中被内化。
• 机场安检： 一个详细的案例研究（图 11），对信息流（护照、机票、行李）通过分布式系统的过程进行建模。它展示了站点（某处可用的信息）和基（推理能力）如何通过通道演变和交互，以确保系统完整性（例如，将乘客与行李匹配）。

5. 意义与主张

本文声称提供了一种基于推理和推论的概念严谨的数学逻辑信息阐释。其意义在于：

• 基础转变： 从模型论观点（模型中的真值）转向证明论观点（基中的可推导性）。这与推论主义哲学相一致，即意义由使用决定。
• 回应范·本瑟姆的范畴： 作者认为他们的方法主要解决了作为关联的信息（通过推论元和情境），但也提供了解决作为范围的信息（通过基的范围）和作为代码的信息（通过消息的推论内容）的途径。
• 建模分布式系统： 它提供了一种基于推理的信息流理论，适用于信息处理系统的组织，为理解复杂生态系统提供了工具，而无需依赖可能难以管理的全局模型。
• 谦逊性： 作者将这项工作描述为迈向完整推论主义阐释的“第一步”。他们承认，关于真实性、能动性以及与其他逻辑动态（如范·本瑟姆的工作）的整合的深入讨论留待未来工作。他们并未声称解决了所有基础问题，但已建立了一个可行的逻辑框架以供进一步发展。