跳至內容

相繼式

維基百科,自由的百科全書

證明論中,相繼式(sequent)是對在規定演繹演算的時候經常用到的可證明性的形式陳述。

解釋

[編輯]

相繼式有如下形式

這裏的Γ和Σ二者是邏輯公式的序列(就是說公式的數目和出現次序都是重要的)。符號通常被稱為十字轉門(turnstile)或T型符號(tee),並經常被讀做"產生"或"證明"。它不是語言中的符號,而用來討論證明的元語言中的符號。在相繼式中,Γ叫做相繼式的前件(antecedent)而Σ叫做相繼式的後繼(succedent)。

直覺意義

[編輯]

上面給出的那種相繼式的直覺意義是在假定了Γ推出Σ是可證明的之下的。在經典的情形下,在十字轉門左面的公式按合取解釋,而右面的公式按析取解釋。這意味着當在Γ中的所有公式成立的時候,在Σ中至少有一個公式必定是真的。如果後繼為空,則按虛假解釋,就是說意味着Γ證明了虛假,並且因此是矛盾的。在另一方面,空前件被假定為真,就是說意味着Σ沒有任何假定就成立,也就是說,它總是真(作為一個析取式),而且因此是一個斷言

但是上述解釋只用於教學目的。因為在證明論中的形式證明是純粹的語法上的,相繼式的語義只由提供實際的推理規則的演算的性質給出。

剝離在上面的技術性精確定義中的任何矛盾,我們可以按它們的介紹性的邏輯形式來描述相繼式。表示我們開始邏輯處理時做的假定的集合,例如"蘇格拉底是人"和"所有人都是必死的"。表示從這些前提得到的邏輯結論。例如,我們希望在十字轉門的端見到"蘇格拉底是必死的"。在這個意義上,意味着推理過程,或者英語中的"所以"。

我們對這些符號指派的意思是有所助益的。規則自身按機械性本質來運做而不承載潛在的意義。這個主題的詳情請參見哥德爾不完備定理

例子

[編輯]

一個典型的相繼式:

它聲稱要麼要麼可以推導自

性質

[編輯]

因為在(左邊的)的前件中的所有公式都必須為真來獲得在(右邊的)後繼中至少一個公式為真,向任何一端增加公式都導致一個更弱的相繼式,而從任何一端去除公式都得到更強的相繼式。

規則

[編輯]

多數證明系統都提供從一個相繼式到另一個相繼式的演繹方式。這些規則都寫成在橫線上下的相繼式列表。這些規則指示如果在橫線上的所有相繼式都為真,則在橫線之下的也都為真。

一個典型的規則是:

這指示了如果我們可以演繹,則我們也可以演繹它自一起。

注意我們通常使用大寫的希臘字母來指稱(可能為空)公式的列表。被用來指示的緊縮,就是說,這些出現在要麼要麼中但不重複的那些公式的列表。

變體

[編輯]

這裏介紹的相繼式的一般概念能以各種方式特殊化。一個相繼式被稱為是直覺相繼式,如果在後繼中有最多一個公式。這種形式是獲得直覺邏輯的演算是需要的。類似的,你可以通過要求相繼式在前件中只有一個公式來獲得雙直覺邏輯(某種次協調邏輯)的演算。

在很多情況下,相繼式還假定由多重集集合組成。所以你可以漠視公式的次序甚至數目。對於經典命題邏輯這不導致問題,因為你能從一組前提中得出的結論不依賴於這些數據。但是在亞結構邏輯中這就變得很重要了。

一些系統只允許在右邊有一個公式。

歷史

[編輯]

歷史上,相繼式是格哈德·根岑介入用來規定他著名的相繼式演算。在他的德語出版物中他使用了單詞"Sequenz"。但是,在英語中,單詞"序列"已經用來翻譯德語的"Folge"並在數學中經常出現。術語"相繼式"被建立用做這個德語表達的替代翻譯。

本條目含有來自PlanetMathSequent》的內容,版權遵守共享創意協議:署名-相同方式共享協議