接上文，本篇文章會處理一些有關於直覺主義算術 的問題，主要是 與 之間的關係。

一些約定：

1. 等詞的公理將省略全稱實例化視為規則 直接應用。
2. 等詞的否定的公理 證明從略，同樣視為規則 直接應用。
3. 歸納公理模式也將作為一條規則 來使用。

中的雙否定除去

引理4 。

證明 要證明該命題成立，需要連續使用三次歸納公理模式。首先歸納證明 。然後是 ，其中 由 和 （及前提 ）證得。綜合前兩者即得 。

令 則

再令 ， 則

由這兩者歸納即得 。

引理5 對於任意公式 ， 。

定理6 對於任意算術原子公式 ，均有 。

證明 由公式的定義，每一個原子公式 都必定擁有以下兩種形式之一： 或 （此時 ）。

• 若 ，由於公式必定是有限長的，由我們在上篇文章中引入的約定 有限次應用 即得證。
• 若 ，應用兩次 後由引理4及引理5得證。

推論7 對於任意不含 與 的算術公式，均有 。

證明 由引理1，定理6對公式結構做歸納。

注意由於上篇文章中對可容許的公理的限制，推論7對 自身同樣有效。

主要結論

定理8 對於任意不含 與 的算術公式 ， 當且僅當 。

這就是上一篇文章開頭的(2)。我們假設這些限制對 同樣有效，即 與 的公理必須是相同的。

證明 效仿定理3的處理方式，把每一個證明過程中可能出現的 與 都替換成 與 ，並填補證明中的gap。由推論7，證明中所有對 的應用都是直覺主義有效的，即該證明是一個合法的直覺主義證明。又因為前提 和結論 中都不含有這兩個符號，不受替換的影響，定理得證。

推論9 對於任意算術公式 ，存在一經典等價公式 滿足 當且僅當 。

這基本就是把定理3重說了一遍，只要注意到 （ ）即可。

定理10 一致蘊含 一致。

我們說一個理論 一致當且僅當 ，其中 是任意命題。

證明 我們證它的逆否命題。假設 ，那麼由推論9， ，即 不一致蘊含 不一致。

推薦閱讀：

相关文章