更改

=== Solovay 可证性逻辑 ===

=== Solovay 可证性逻辑 ===

'''背景'''：'''可证性逻辑（provability logic）'''&#x7814;究"可证"这个概念的抽象规律，把 "⌜<math>\phi</math>⌝ 在 PA 中可证" 抽象为模态算子 □<math>\phi</math>。[[模态逻辑]]系统 '''GL'''（[[Gödel-Löb 逻辑|Gödel-Löb 逻辑]]）是候选公理系统。

'''背景'''：'''可证性逻辑（provability logic）'''研究"可证"这个概念的抽象规律，把 "⌜<math>\phi</math>⌝ 在 PA 中可证" 抽象为模态算子 □<math>\phi</math>。[[模态逻辑]]系统 '''GL'''（[[Gödel-Löb 逻辑|Gödel-Löb 逻辑]]）是候选公理系统。

> '''Solovay 定理（1976）'''：一个模态公式在 PA 的所有解释下都可证，当且仅当它是 [[Gödel-Löb 逻辑|GL]] 的定理。即 GL '''恰好'''完全刻画了 PA 的可证性逻辑。<ref name="solovay1976" /><ref name="moschovakis2010" />

'''Solovay 定理（1976）'''：一个模态公式在 PA 的所有解释下都可证，当且仅当它是 [[Gödel-Löb 逻辑|GL]] 的定理。即 GL '''恰好'''完全刻画了 PA 的可证性逻辑<ref name="solovay1976" /><ref name="moschovakis2010" />。

[[罗伯特·索洛韦|Solovay]] 的证明漫长精巧，其关键引理需要构造一个'''自指的'''函数 h——h 的定义中引用 h 自己的编号。Solovay 本人用一句话带过："表面上的循环用递归定理以通常方式处理"<ref name="moschovakis2010" />。Moschovakis 评论：无法想象不借助 SRT 如何凭空想出这个构造——在此意义上 SRT 是可证性逻辑这块基石中不可或缺的成分<ref name="moschovakis2010" />。

[[罗伯特·索洛韦|Solovay]] 的证明漫长精巧，其关键引理需要构造一个'''自指的'''函数 h——h 的定义中引用 h 自己的编号。Solovay 本人用一句话带过："表面上的循环用递归定理以通常方式处理"<ref name="moschovakis2010" />。Moschovakis 评论：无法想象不借助 SRT 如何凭空想出这个构造——在此意义上 SRT 是可证性逻辑这块基石中不可或缺的成分<ref name="moschovakis2010" />。