直覺主義邏輯上的Friedman-Sheard理論*,?

李晟

四川師范大學(xué) 邏輯與信息研究所

四川師范大學(xué) 馬克思主義學(xué)院

nklisheng@126.com

李娜

南開大學(xué) 哲學(xué)院

linawii@nankai.edu.cn

1 引言

如果一個(gè)由若干真之規(guī)律（law of truth）組成的集合在經(jīng)典邏輯上是不相容的，那么是否意味著我們應(yīng)當(dāng)拒絕接受它呢？不相容性固然是與真之規(guī)律本身的形式有關(guān)，但經(jīng)典邏輯是否也是影響相容性的一個(gè)因素呢？對(duì)此，利（G.E.Leigh）和拉特延（M.Rathjen）提出了在直覺主義邏輯上重新考察真之規(guī)律各種組合的相容性的研究思路（[6]）。我們認(rèn)為這樣的研究思路對(duì)于找出導(dǎo)致不相容的原因是很有益的。而且我們認(rèn)為，不僅是相容性，保守性、組合性等其他真理論性質(zhì)也可以在新的邏輯上再行檢驗(yàn)。這樣將有助于真正弄清楚這些性質(zhì)究竟是基于真之規(guī)律本身，還是基于它們的邏輯基礎(chǔ)。

我們的方式與利和拉特延的方式有所不同。后者僅僅是以真之規(guī)律的組合為對(duì)象，他們所關(guān)注的焦點(diǎn)在于相容性，其目的是試圖為那些不相容的組合尋求適當(dāng)?shù)霓q護(hù)。而我們則是以公理化真理論的系統(tǒng)為對(duì)象，我們嘗試通過將系統(tǒng)原本的經(jīng)典邏輯基礎(chǔ)直接削弱為直覺主義邏輯，從而嘗試為研究經(jīng)典的公理化真理論及其性質(zhì)提供一種可能的參照。根據(jù)這一方式，我們?cè)谡撐腫9]中討論了兩種基于直覺主義邏輯的公理化真理論：IDT和SICT。但是這兩種真理論的真謂詞都受到了類型的限制，因而具有比較明顯的局限性。所以在本文中，我們選擇在直覺主義邏輯上重新討論Friedman-Sheard理論，這是一種無類型的真理論。本文把這一基于直覺主義邏輯的Friedman-Sheard理論記為IFS。我們將首先給出IFS理論的形式系統(tǒng)；然后討論直覺主義的修正語義學(xué)，并證明IFS理論可以將直覺主義修正語義學(xué)公理化至第一個(gè)極限序數(shù)ω；最后簡(jiǎn)要地討論IFS理論與它的經(jīng)典版本FS理論之間的關(guān)系。

在接下來的各個(gè)小節(jié)里，我們用LHA表示海廷算術(shù)HA（[8]）的語言，包括邏輯常項(xiàng)?、∧、∨、→、?、?、?，等詞符號(hào)=，以及算術(shù)符號(hào)0、S、+、×。HA是以直覺主義邏輯為基礎(chǔ)的，當(dāng)它被加強(qiáng)為經(jīng)典邏輯時(shí)，所得到的就是皮亞諾算術(shù)PA。因此，PA的語言LPA與LHA是完全相同的。如果以一元謂詞T擴(kuò)充LHA，即得到新的語言LT。我們用HAT來命名由LT重新表達(dá)后的HA，也即是允許T謂詞在HA的歸納公理模式中出現(xiàn)。我們還可以相應(yīng)地得到PAT。

已知PA有標(biāo)準(zhǔn)模型N（[5]，第10頁），它以自然數(shù)集N為論域，將算術(shù)符號(hào)分別解釋為自然數(shù)0、后繼函數(shù)、加法函數(shù)和乘法函數(shù)。根據(jù)文獻(xiàn)[8]所給出的直覺主義邏輯Kripke模型的構(gòu)造方法（[8]，第75-87頁），我們可以證明K=〈K,≤,N〉是HA的模型。其中，K是一個(gè)非空的結(jié)點(diǎn)集；≤是結(jié)點(diǎn)之間的二元偏序關(guān)系；N即PA的標(biāo)準(zhǔn)模型。這意味著當(dāng)K中只有一個(gè)結(jié)點(diǎn)時(shí)，K與N是相同的。我們用M=〈K,?〉來表示HAT的模型。其中K是HA的模型，?是一個(gè)賦值函數(shù)，它為每個(gè)結(jié)點(diǎn)k∈K指派N的一個(gè)子集?(k)，作為在該結(jié)點(diǎn)上對(duì)T謂詞的解釋，并同時(shí)滿足條件：對(duì)任意結(jié)點(diǎn)k和k′，如果有k≤k′，那么有。力迫關(guān)系“?”按照通常的方式定義（[8]，第80頁），但還需增加對(duì)T謂詞的解釋：k?T(s)當(dāng)且僅當(dāng)sN∈?(k)。sN表示在N中為s指派的值。為使記法簡(jiǎn)潔，我們將把sN直接記為s。

如果φ是LT的語句，那么┍φ┑表示φ的哥德爾編碼。HA原子語句的真謂詞在HA中是可定義的公式（[4]，第42頁），用V al+(x)表示。此外，SentT(x)表示x是LT語句的哥德爾編碼；AtSentT(x)表示x是LT原子語句的哥德爾編碼。若將下標(biāo)“T”換為“HA”或“PA”，則得到相應(yīng)的HA或PA的句法性質(zhì)的表達(dá)式。三元替換函數(shù)x(t/s)表示用項(xiàng)t去替換公式x中的變?cè)猻。是自然數(shù)n的數(shù)字，有時(shí)我們也用后繼函數(shù)來表示。上方加點(diǎn)的邏輯聯(lián)結(jié)詞和量詞符號(hào)用以表示N上的某種特殊的運(yùn)算，比如：。

2 FS理論的直覺主義版本IFS

2.1 FS理論

哈爾巴赫（V.Halbach）在論文[2]中首次給出了FS理論的公理系統(tǒng)。之所以命名為Friedman-Sheard理論，是因?yàn)樗葍r(jià)于弗里德曼（H.Friedman）和希爾德（M.Sheard）在此前的論文[1]中所給出的系統(tǒng)D。下面給出FS理論的哈爾巴赫版本（[3]，第159-161頁）：

定義1(FS)FS以LT為形式語言，在PAT的基礎(chǔ)上添加下列公理和規(guī)則而得到：

（1）公理：

（2）規(guī)則：

NEC：對(duì)任意LT語句φ，如果能給出φ的證明，那么就能推出T┍φ┑。

CONEC：對(duì)任意LT語句φ，如果能給出T┍φ┑的證明，那么就能推出φ。

FS的外邏輯（outer logic）和內(nèi)邏輯（inner logic）是一致的，也即是構(gòu)造FS的邏輯基礎(chǔ)與FS的T謂詞所能作用的語句所遵循的邏輯都是經(jīng)典邏輯。這是FS最重要的特點(diǎn)。

2.2 直覺主義的IFS理論

定義2(IFS)IFS以LT為形式語言，在HAT的基礎(chǔ)上添加下列公理和規(guī)則而得到：

（1）公理：

（2）規(guī)則：

NEC：對(duì)任意LT語句φ，如果能給出φ的證明，那么就能推出T┍φ┑。

CONEC：對(duì)任意LT語句φ，如果能給出T┍φ┑的證明，那么就能推出φ。

從表面來看，IFS的真之公理與FS的真之公理并不完全相同，前者增加了關(guān)于蘊(yùn)涵的公理IFS5。這是因?yàn)樵谥庇X主義邏輯背景下，邏輯聯(lián)結(jié)詞不能相互定義。而在經(jīng)典邏輯背景下，公理IFS5可以由FS的其余真之公理證明，故而通常將其簡(jiǎn)化。所以，盡管有公理數(shù)量上的不同，但這并不妨礙IFS與FS只在邏輯基礎(chǔ)上有區(qū)別。

如前所述，哈爾巴赫的FS等價(jià)于弗里德曼和希爾德的系統(tǒng)D。通過削弱外邏輯，我們得到了直覺主義的IFS理論，而利和拉特延也按照同樣的方式得到了系統(tǒng)D的直覺主義版本Di（[6]）。本文把Di記為IFSO，現(xiàn)在給出IFSO并探討它與IFS的關(guān)系。

定義3(IFSO)IFSO是由下列公理和規(guī)則組成：

（1）公理：

（2）規(guī)則：T-Intro：對(duì)任意LT語句φ，從φ可以推出T┍φ┑；

T-Elim：對(duì)任意LT語句φ，從T┍φ┑可以推出φ；

?T-Intro：對(duì)任意LT語句φ，從?φ可以推出?T┍φ┑；

?T-Elim：對(duì)任意LT語句φ，從?T┍φ┑可以推出?φ。

在定義中，PRE是HA的子理論，它是通過去掉HA的歸納公理模式而得到。Bew(x)表示x是可證語句的哥德爾編碼。

定理1IFS?IFSO。

證明：只需證明IFSO能夠推出IFS的全部真之公理和規(guī)則。

驗(yàn)證IFSO?IFS1：

因?yàn)镠A的原子公式與PRE的原子公式是相同的，所以在HA中可以證明下面的這個(gè)式子成立：

于是，根據(jù)（2-1），一方面有：

以上推理的第二行是因?yàn)椋篐A??x?y(??(x=y)→x=y)（[8]，第123-128頁）；第三行是依據(jù)了PRE的原子語句滿足排中律；第四行借助了直覺主義邏輯的有效式，并且其前件可根據(jù)PRE-Ref而分離；第五行利用了下述式（2-2）；第六行依賴于事實(shí)：HA??x?y(x=y→??(x=y))。

同樣地，另一方面很容易有：

兩個(gè)方面相結(jié)合，即為IFSO?IFS1。

驗(yàn)證IFSO?IFS2：

因?yàn)?(φ∧ψ)→(ψ→?φ)是直覺主義邏輯的有效式，所以從T-Cons可以推出：

與T-Comp(w)結(jié)合，即為IFSO?IFS2。

驗(yàn)證IFSO?IFS3：

一方面有：

另一方面有：

兩個(gè)方面相結(jié)合，即為IFSO?IFS3。

其余公理和規(guī)則可以類似依次驗(yàn)證。證畢。 □

3 直覺主義的修正語義學(xué)

修正語義學(xué)（revisionsemantics）是由古譜塔（A.Gupta）和赫茲伯格（H.Herzberger）分別獨(dú)立提出，并由貝爾納普（N.Belnap）和古譜塔進(jìn)一步發(fā)展和推廣的語義真理論。它是克里普克語義真理論最強(qiáng)有力的競(jìng)爭(zhēng)者。哈爾巴赫證明了FS與修正語義學(xué)的關(guān)系，即：FS可以將修正語義學(xué)公理化至第一個(gè)極限序數(shù)ω（[3]）。本節(jié)我們將在哈爾巴赫工作1哈爾巴赫在討論修正語義學(xué)時(shí)，不僅使用了有別于以往工作的符號(hào)和記法，而且提出了一種新的“修正”方式。本文所采用的正是哈爾巴赫記法和方式。的基礎(chǔ)上，首先給出標(biāo)準(zhǔn)修正語義學(xué)的基本思想和基本結(jié)論，然后在直覺主義邏輯的背景下對(duì)它們進(jìn)行推廣，并解釋直覺主義修正語義學(xué)與IFS理論的關(guān)系。

3.1 標(biāo)準(zhǔn)的修正語義學(xué)與FS理論

修正語義學(xué)的基本思想是：從對(duì)真謂詞的任意解釋出發(fā)，通過一個(gè)恰當(dāng)?shù)男拚^程，得到對(duì)該真謂詞越來越好的解釋。這個(gè)恰當(dāng)?shù)男拚^程一般是通過修正算子（revision operator）來定義。

定義4(修正算子) 對(duì)自然數(shù)集的任意子集S?N，修正算子Γ定義為：

，其中φ是LT語句。

在定義4中，N是PA的標(biāo)準(zhǔn)模型，S是修正前對(duì)真謂詞的解釋，Γ(S)是修正后的解釋。從該定義可以知道，Γ是N的冪集?(N)上的運(yùn)算，并且有：

根據(jù)定義4，可以將修正算子的迭代應(yīng)用Γn(S)定義如下，從而刻畫后繼序數(shù)次迭代的修正過程：

通過上述修正過程，雖然我們能夠得到對(duì)真謂詞越來越好的解釋，但是如何理解“越來越好”？這是十分模糊的。而且“越來越好”預(yù)設(shè)了對(duì)真謂詞的起始解釋也應(yīng)該是一種“好”的解釋，那么如何證明這種解釋是好的？這些問題并不容易澄清。因此，哈爾巴赫對(duì)關(guān)于修正過程的觀點(diǎn)做了一些改變。修正過程不再是一個(gè)“越來越好”的過程，而是一個(gè)從對(duì)真謂詞的所有可能解釋中，逐漸剔除不恰當(dāng)解釋的過程。（[3]，第164-172頁）這樣一來，N的任何子集都是對(duì)真謂詞的可能解釋，即從N的冪集?(N)開始，使修正算子Γ作用于?(N)中的每一個(gè)元素，即：

很顯然，Γ[?(N)]是?(N)的子集。重復(fù)上述修正過程，使修正算子Γ作用于Γ[?(N]中的所有元素，從而得到?(N)的一個(gè)更小的子集?？梢?，這樣的修正過程使得其中一些解釋被逐步排除出去?，F(xiàn)在，我們可以更一般地將新的修正過程定義如下：

定義5令M??(N)，并且令Γ[M]={Γ(S)|S?M}，那么Γ的后繼序數(shù)迭代應(yīng)用Γn[M]就可以定義為：

哈爾巴赫利用這種新的修正過程，解釋了FS的子理論（參見定義6）與修正語義學(xué)的關(guān)系：Γn[?(N)]的任意元素，都是對(duì)FS某個(gè)子理論的真謂詞的恰當(dāng)解釋，并且這些FS的子理論都有標(biāo)準(zhǔn)模型N。

定義6(FS的子理論) FS的子理論FSn定義如下：

FS0=PAT；

FS1是由FS的所有公理及PAT的整體反射原理2PAT的整體反射原理PAT-Ref，即：?x(SentT(x)∧BewT(x)→T(x))。組成；

FSn+1的公理與規(guī)則同F(xiàn)S并無差別，但是在形式證明中只允許NEC規(guī)則和CONEC規(guī)則最多應(yīng)用于n個(gè)不同的語句。

定理2對(duì)任意n∈N，以及對(duì)任意S?N，都有：

證明：從左向右，施歸納于FSn證明的長(zhǎng)度。從右向左，只需找到一個(gè)S′，使得 Γ(S′)=S，并且S′∈Γn-1[?(N)]（[3]，第 170-172 頁）。證畢。 □

3.2 直覺主義的修正語義學(xué)

直覺主義修正語義學(xué)的思想是：試圖把修正語義學(xué)與直覺主義邏輯的語義學(xué)相結(jié)合。斯特恩（J.Stern）在研究模態(tài)性與公理化真理論時(shí)，定義了一種模態(tài)修正語義學(xué)，其思想是把修正語義學(xué)與模態(tài)邏輯的可能世界語義學(xué)相結(jié)合。（[7]）本文的直覺主義修正語義學(xué)正是受到斯特恩的啟發(fā)。因?yàn)橹庇X主義邏輯的語義學(xué)也是一種可能世界語義學(xué)，只是在聯(lián)結(jié)詞和量詞的定義方面與模態(tài)邏輯的可能世界語義學(xué)有所不同。

定義7(賦值函數(shù)) 令K=〈K,≤,N〉是HA的模型，?賦值函數(shù)是從結(jié)點(diǎn)集K到N的冪集?(N)的函數(shù)，并且滿足條件：

其中，?(k)?N是?賦值函數(shù)在結(jié)點(diǎn)k上的值，它表示在結(jié)點(diǎn)k上對(duì)T謂詞的解釋。全體?賦值函數(shù)的集合記為V?。

定義8(直覺主義修正算子) 直覺主義修正算子Γi是?賦值函數(shù)集V?上的運(yùn)算，使得對(duì)任意k∈K，都有：

，其中φ是LT語句。

同樣地，Γi的后繼序數(shù)次迭代定義為：。

直覺主義修正算子的直觀含義是：對(duì)?賦值函數(shù)在每個(gè)結(jié)點(diǎn)k上為T謂詞所做的解釋分別進(jìn)行修正。

推論1對(duì)任意LT語句φ，以及對(duì)任意結(jié)點(diǎn)k∈K，以下等值式成立：

證明：

首先證明“?”：因?yàn)椤碖,?〉[k]?φ，由定義 8，┍φ┑∈[Γi(?)](k)，從而得到〈K,Γi(?)〉[k]? T┍φ┑。

然后證明“?”：因?yàn)椤碖,Γi(?)〉[k]? T┍φ┑，于是根據(jù)對(duì)T謂詞的解釋可知，┍φ┑∈[Γi(?)](k)，再由定義 8，有〈K,?〉[k]?φ。證畢。 □

事實(shí)上，根據(jù)引理1不難知道如下等值式也是成立的：對(duì)任意LT語句φ，〈K,Γi(?)〉? T┍φ┑?〈K,?〉?φ。

為了表述的方便，下面將以T1┍φ┑ 表示 T┍φ┑，Tn+1┍φ┑ 表示 T┍Tn┍φ┑┑。

定理3以下結(jié)論成立：

（1）對(duì)任意?1,?2∈V?，如果 Γi(?1)= Γi(?2)，那么?1=?2；

（2）對(duì)任意LT語句φ，任意結(jié)點(diǎn)k∈K，以及任意n≥1，都有：

（3）對(duì)任意n≥1且。

證明：（1）假設(shè)，那么存在某個(gè)，使得。不妨假設(shè)存在LT語句φ，使得，而。即但是。即：。矛盾。

（2）只需對(duì)推論1進(jìn)行迭代即可證得。

（3）因?yàn)槭且粋€(gè)LT公式，所以由廣義對(duì)角線引理（[4]，第37頁）可知，存在語句λ使得：

因?yàn)樗愿鶕?jù)（2）可得到如下等值式，對(duì)任意結(jié)點(diǎn)k∈K，都有：

將(3-1)代入左端，即得：

所以。從而有。 □

事實(shí)上，根據(jù)推論1和定理3中的（2），我們還可以證明如下推論：

推論2對(duì)任意LT語句φ，以及對(duì)任意結(jié)點(diǎn)k∈K，以下等值式成立：

證明：可以通過施歸納于n來證明。首先考慮歸納基始：當(dāng)n=1時(shí)，我們可以建立如下推理：

其次考慮歸納步驟：假設(shè)當(dāng)n≤k時(shí)結(jié)論成立，現(xiàn)在驗(yàn)證n=k+1的情形：

由此便證明了。 □

以上是直覺主義背景下的“越來越好”修正過程，接下來定義直覺主義背景下的“逐漸排除不恰當(dāng)”修正過程，也即是允許Γi作用于?賦值函數(shù)集V?。

定義9令Γi是直覺主義修正算子，并且令M?V?，于是：

Γi的后繼序數(shù)次迭代應(yīng)用定義為：。

定理4(Γi的反序性) 對(duì)任意m,n∈N，如果m≤n，那么有：

證明：施歸納于Γi的迭代次數(shù)k。

歸納基始：當(dāng)k=1時(shí)，結(jié)論顯然成立。因?yàn)楦鶕?jù)定義9，，所以很明顯；

歸納步驟：假設(shè)當(dāng)k≤l+1時(shí)都成立，現(xiàn)在證明k=l+2，即證明：

假設(shè)中的任意元素，由定義9可知，存在使得。由歸納假設(shè)，，所以，于是按照定義 9，，也即是。 □

Γi的反序性表明，隨著Γi的不斷迭代，Γi所能作用的賦值函數(shù)將會(huì)越來越少，并且每一次迭代所排除的都是不恰當(dāng)?shù)馁x值函數(shù)。例如，賦值結(jié)果包含空集的函數(shù)將在第一次迭代后被排除，而賦值結(jié)果包含┍T┍0=S(0)┑┑的函數(shù)將在第二次迭代后被排除。

推論3 不存在賦值函數(shù)?的無窮序列?0,?1,?2,...，使得對(duì)任意n∈N，都有 Γi(?n+1)=?n。

證明：假設(shè)存在這樣的無窮序列?，F(xiàn)在定義一個(gè)二元原始遞歸函數(shù)f，使得對(duì)任意n∈N，以及對(duì)任意LT語句φ，f滿足：

f在LT中用符號(hào)表示。令ψ(y)表示LT公式，根據(jù)廣義對(duì)角線引理，存在語句λ使得：

很明顯，無論對(duì)T謂詞作何解釋，(3-2)都成立。也即是對(duì)任意a∈N，都有：

根據(jù)?的定義不難知道，對(duì)任意結(jié)點(diǎn)k∈K，都有：

于是對(duì)任意結(jié)點(diǎn)k1≥k，可以建立如下的推理：

上述推理的第七步與最后一步明顯矛盾。而如果假設(shè)〈K,?a〉[k1]?λ，又可以建立如下的推理：

很明顯，上述推理的第十二步與最后一步也是矛盾的。

同理可驗(yàn)證，當(dāng)假設(shè)，及假設(shè)，也都導(dǎo)致矛盾。所以，任何模型都無法滿足(3-3)，因而本引理描述的無窮序列不存在。 □

以上的討論都是Γi后繼序數(shù)次迭代應(yīng)用的情形。現(xiàn)在討論Γi極限序數(shù)次迭代應(yīng)用，并將第一個(gè)極限序數(shù)ω次迭代記為：

但是由Γi的反序性可知，Γi的迭代應(yīng)用不會(huì)永恒地進(jìn)行下去。那么什么時(shí)候是盡頭呢？下面這個(gè)定理將說明，Γi的極限序數(shù)ω次迭代應(yīng)用將是這個(gè)盡頭。

定理5

證明：假設(shè)，也即是存在。于是存在一個(gè)賦值函數(shù)的無窮序列?0,?1,?2,...，使得對(duì)任意n∈N，都有Γi(?n+1)=?n。但是根據(jù)推論3，這樣的無窮序列是不存在的。所以。 □

現(xiàn)在建立IFS理論與直覺主義修正語義學(xué)之間的核心結(jié)論：IFS可將直覺主義修正語義學(xué)公理化至第一個(gè)極限序數(shù)ω。

定義10（IFS的子理論）IFS的子理論IFSn定義如下：

IFS1是由IFS的所有公理及HAT的整體反射原理組成；

IFSn+1的公理與規(guī)則同IFS并無差別，但是在形式證明中只允許NEC規(guī)則和CONEC規(guī)則最多應(yīng)用于n個(gè)不同的語句。

定理6如果令K是HA的模型，Γi是直覺主義修正算子，那么對(duì)任意n∈N，下面的等值式成立：

證明：可通過施歸納于n來證明。歸納基始分為兩種子情形：

當(dāng)n=0時(shí)：，IFS0=HAT。已知K是HA的模型，并且在HAT中沒有真之公理，所以HAT的T謂詞不受任何約束，因而V?中的任何?賦值函數(shù)都是對(duì)HAT中的T謂詞的恰當(dāng)解釋；反過來，在每個(gè)結(jié)點(diǎn)k上任意指派N的一個(gè)子集S，只要這些S滿足條件，就可以構(gòu)成一個(gè)?賦值函數(shù)，由此形成的〈K,?〉一定是HAT的模型，而V?又是所有賦值函數(shù)的集合，所以必定有。此種情形得證。

當(dāng)n=1時(shí)：先證明。對(duì)任意，可通過施歸納于IFS1證明的長(zhǎng)度。只需驗(yàn)證〈K,?〉滿足IFS1的真之公理和HAT的整體反射原理。因?yàn)?，所以存在，使得?/p>

IFS1的驗(yàn)證比較簡(jiǎn)單，此處從略。

驗(yàn)證IFS2，對(duì)任意結(jié)點(diǎn)k∈K：

其余聯(lián)結(jié)詞和量詞公理均可類似驗(yàn)證。現(xiàn)在說明〈K,?〉滿足HAT的整體反射原理。因?yàn)橐呀?jīng)證明了〈K,?′〉?HAT，所以根據(jù)定義8，對(duì)于任意結(jié)點(diǎn)k∈K，HAT的所有可證語句的哥德爾編碼都在[Γi(?′)](k)中，因而都能為T謂詞作用。

再證明。要想證明，也就是要能找到一個(gè)，并能證明?，F(xiàn)在構(gòu)造一個(gè)函數(shù)，使得對(duì)任意結(jié)點(diǎn)k∈K，都有：

，其中φ是LT語句。

很明顯，，現(xiàn)在證明。可以通過對(duì)二者中的語句（確切地說，是其元素所編碼的語句）的復(fù)雜度進(jìn)行歸納來證明。

對(duì)于原子語句T┍φ┑的情形：

對(duì)于復(fù)合語句?φ的情形：

其余聯(lián)結(jié)詞和量詞的情形類似可證，從而證明Γi(?′)=?。

歸納步驟：假設(shè)當(dāng)n≤k時(shí)都成立，現(xiàn)在證明n=k+1。同樣分兩個(gè)方向：

先證明從左到右：也即是假設(shè)，證明。根據(jù) Γi的反序性可知，，所以根據(jù)歸納假設(shè)，〈K,?〉是IFSk的模型，故而只需證明在IFSk中多使用一次NEC規(guī)則和CONEC規(guī)則可保持〈K,?〉是模型。又因?yàn)?，所以存在某個(gè)，使得。

假設(shè)多使用一次NEC規(guī)則：

假設(shè)多使用一次CONEC規(guī)則：

需要注意的是，上述推理從第四步到第五步，是因?yàn)?′既屬于又屬于，而并不是因?yàn)榭梢源嬖谀硞€(gè)?′，使得。而最后一步的得出是因?yàn)橥评碇械?′具有任意性。

再證明從右到左：假設(shè)，并且構(gòu)造一個(gè)賦值函數(shù)?′，使得對(duì)任意k∈K：

，其中φ是LT語句。

由情形n=1的證明可知，Γi(?′)=??，F(xiàn)在只需證明，根據(jù)歸納假設(shè)，也就是要證明〈K,?′〉? IFSk。

不難知道，對(duì)任意LT語句φ，如果IFSk?φ，那么只需對(duì)φ再使用一次NEC規(guī)則即可推出 T┍φ┑，也即是IFSk+1?T┍φ┑。于是根據(jù)假設(shè)就有〈K,?〉? T┍φ┑。又因?yàn)橐呀?jīng)證明 Γi(?′)=?，所以，，即對(duì)任意k∈K，都有。根據(jù)推論 1可以得到，。從而也就證明了。 □

推論4IFS是相容的。

證明：對(duì)任意LT語句φ，如果IFS?φ，那么在對(duì)φ的證明中必定只包含有窮多次使用NEC規(guī)則和CONEC規(guī)則，也就是存在某個(gè)子理論IFSn?φ。對(duì)任意的賦值函數(shù)?，都有，于是由定理6可知，即為IFSn的一個(gè)模型，所以任何IFSn都是相容的。 □

推論4說明了IFS的相容性。因?yàn)槎ɡ?表明，當(dāng)Γi通過極限序數(shù)次迭代應(yīng)用之后，已經(jīng)不存在恰當(dāng)?shù)?賦值函數(shù)，所以IFS不能證明包含T謂詞超窮迭代的語句。也即是，IFS本身沒有基于K的算術(shù)模型。這與經(jīng)典的FS理論的結(jié)論是完全相同的。

定義11（ω-不相容性）算術(shù)理論S是ω-不相容的，當(dāng)且僅當(dāng)存在一個(gè)公式φ(x)，使得：

（1）S???xφ(x)；

（2）對(duì)任意n∈N，都有S?φ()。

定理7IFS是ω-不相容的。

證明：定義原始遞歸函數(shù)f=(n,φ)，參見推論3。根據(jù)廣義對(duì)角線引理：

現(xiàn)在建立如下IFS推理一：

此外，還可建立如下IFS推理二：

推理一與推理二相結(jié)合就得到：

如果不斷地由(3-5)使用NEC規(guī)則，則不難得到如下無窮序列：

這也就說明，對(duì)任意n∈N，都有。將其與(3-6)結(jié)合，即可證明IFS是ω-不相容性的。 □

FS的最大不足在于ω-不相容性，雖然它并不等同于FS自身的不相容，但是作為一種真理論，這是很難讓人接受的。因?yàn)镕S是ω-不相容的，也就意味著FS不適合PA的標(biāo)準(zhǔn)解釋。這就說明當(dāng)T謂詞被添加到PA后，徹底改變了PA原有的意義。而現(xiàn)在看來，這一不足與FS的邏輯基礎(chǔ)無關(guān)。總之，IFS基本上保持了FS的主要性質(zhì)。下面簡(jiǎn)要分析其原因。

4 FS與IFS的關(guān)系

已經(jīng)知道，HA一方面是PA的子理論，但另一方面，PA也可通過否定性轉(zhuǎn)換（negative translation）嵌入HA（[8]，第128頁）。FS與IFS之間也有這樣的轉(zhuǎn)換。在已有的轉(zhuǎn)換條款的基礎(chǔ)上，我們可以定義：

定義12(真理論的否定性轉(zhuǎn)換) 真理論的否定性轉(zhuǎn)換是在PA到HA的否定性轉(zhuǎn)換的基礎(chǔ)上，增添如下一條關(guān)于T謂詞原子語句的轉(zhuǎn)換條款：

定理8 FS?φ?IFS?φ?。

證明：只需從兩個(gè)方向分別驗(yàn)證該結(jié)論對(duì)任意邏輯公理、算術(shù)公理以及真之公理都成立。從右向左是顯然的，下面只證明從左向右。邏輯公理和算術(shù)公理的情形，參閱[8]。

驗(yàn)證IFS2*，：

故而；

驗(yàn)證 IFS4*，：

同理可驗(yàn)證，；

驗(yàn)證 IFS7*，：

同理可驗(yàn)證，；其余真之公理可類似驗(yàn)證。 □

定理8表明，IFS之所以能夠保持FS的性質(zhì)，乃是因?yàn)槲覀兛梢酝ㄟ^否定性轉(zhuǎn)換，把關(guān)于FS的性質(zhì)的結(jié)論轉(zhuǎn)換為關(guān)于IFS的性質(zhì)的相應(yīng)結(jié)論。而這也就說明，F(xiàn)S的基本真理論性質(zhì)主要是基于其真之公理，而不是邏輯基礎(chǔ)。

5 結(jié)語

在本文中，我們討論了基于直覺主義邏輯的Friedman-Sheard理論IFS。我們的目的是為研究FS提供一個(gè)參照，所以我們建立的IFS理論僅僅是在邏輯基礎(chǔ)上與FS不同，而并非按照FS的框架討論了基于直覺主義的真之規(guī)律的新的公理化真理論。我們還討論了直覺主義修正語義學(xué)，它是把標(biāo)準(zhǔn)的修正語義學(xué)推廣至多個(gè)結(jié)點(diǎn)而得到。因此當(dāng)結(jié)點(diǎn)集K中只含一個(gè)結(jié)點(diǎn)時(shí)，我們的直覺主義修正語義學(xué)就等同于標(biāo)準(zhǔn)的修正語義學(xué)。我們證明了IFS能將這樣的直覺主義修正語義學(xué)公理化至第一個(gè)極限序數(shù)ω，這是本文最重要的結(jié)果。本文最后一個(gè)定理的證明表明，F(xiàn)S的性質(zhì)是由真之規(guī)律本身而不是由邏輯基礎(chǔ)決定的。

[1]H.Friedman and H.Sheard,1987,“An axiomatic approach to self-referential truth”,Annals of Pure and Applied Logic,33:1-21.

[2]V.Halbach,1994,“A system of complete and consistent truth”,Notre Dame Journal of Formal Logic,36:311-327.

[3]V.Halbach,2011,Axiomatic Theories of Truth,Cambridge:Cambridge University Press.

[4]L.Horsten,2011,The Tarskian Turn:Deflationism and Axiomatic Truth,Cambridge:MIT Press.

[5]R.Kaye,1991,Models of Peano Arithmetic,Oxford:Clarendon Press.

[6]G.E.Leigh and M.Rathjen,2012,“The Friedman-Sheard programme in intuitionistic logic”,Journal of Symbolic Logic,77(3):777-806.

[7]J.Stern,2014,“Modality and axiomatic theories of truth I:Friedman-Sheard”,The Review of Symbolic Logic,7(2):273-298.

[8]A.S.Troelstra and D.van Dalen,1998,Constructivism in Mathematics,Amsterdam:North-Holland.

[9]李娜，李晟，“直覺主義邏輯上的公理化真理論”，邏輯學(xué)研究，2015年第3期，第48-63頁。