算术系统中的证明谓词

在一阶算术系统中，可构造证明谓词Pr

证明谓词的基本性质：

(1) Pr(p→q)∧Pr(p)→Pr(q)

(2) Pr(p)→Pr(Pr(p))

(3) Pr(Pr(p)→p)→Pr(p)

(4) ⊢A ⇒ ⊢Pr(A)

(5) ⊢ Pr(p)→p ⇒ ⊢p

其他性质：

1、算术系统具有可靠性，即⊢A，则A是真的

2、⊢ Pr(A) ⇒⊢ A

3、Pr(A)真，当且仅当，⊢ Pr(A)

4、Pr(A) → A是真的，但它不是定理

5、Pr(⊥)和﹁Pr(⊥)都不是定理

可证性逻辑GL系统

公理：

(K) □(p→q)∧□p→□q

(W) □(□p→p)→□p

(4) □p→□□p

推理规则：

⊢A ⇒ ⊢□A

性质

1、4公理可去掉，因为它是系统KW的定理。

2、W公理对应的框架条件是传递性和逆良基性。即在这类框架中，W是有效式，并且如果W在一个框架中有效，那这个框架必然具有传递性和逆良基性。（良基，即不存在无穷降链，逆良基是不存在无穷升链。逆良基关系要求非自返性。）

3、一个有穷模型，它是传递的和逆良基的，当且仅当，它是传递的和非自返的。

4、GL系统具有可靠性和弱完全性。

5、GL逻辑具有有穷模型性，即它相对于所有具有传递性和非自返性的有穷框架，具有可靠性和弱完全性。

6、在GL系统中，⊢□A ⇒ ⊢A不成立（？）

GL系统和算术系统

将GL中的语言，翻译成算术系统中的语言。将□翻译为Pr谓词，将GL中的字母翻译为算术系统中的命题。显然具体的翻译有很多种，比如可将GL中的p翻译为1=1，也可以翻译为1=2。

GL系统和算术系统PA有如下的关系：

1、⊢_GL A，当且仅当，对任意翻译f都有，⊢_PA f(A)

2、存在一种翻译f，如果⊢_PA f(A)，那么⊢_GL A

固定点定理

如果公式A(p)中的命题变元p在证明算子的辖域内，那么存在一个公式B，其中B不包含命题变元p，且没有出现A中没有的命题变元，使得：

⊢ B ↔ A(B)

    固定点是唯一的，即任意两个固定点在逻辑上是等价的。

例如A(p)= ﹁□p的固定点是﹁□⊥, 即

⊢  ﹁□⊥ ↔ ﹁□(﹁□⊥).

GLS系统

GLS系统的公理是GL系统的所有定理，和所有形式为□A→A的命题，唯一的推理规则是分离规则。

它的另一种公理化方法如下：

公理：

1、□p→p

2、□p→□□p

3、□(□(p→q)∧□p→□q)

4、□(□(□p→p)→□p)

推理规则：

A，A→B ⇒ B

性质：

1、GLS是非正规系统，因为它不符合必然化规则，所以它没有合适的可能世界语义。（正规系统是指包括K公理和必然化规则的系统。）

2、GLS系统有导出规则：⊢A ⇒ ⊢◇A

3、⊢_GLS A，当且仅当，⊢_GL A^S

（A^S = ∧{□C→C}→A，这里□C是A的子公式。）

4、公式A是GLS的定理，当且仅当，对任意翻译f，f(A)在标准模型中都是真的。