命題演算分離規則:命題演算分離規則(modus ponens in a -百科知識中文網

分離規則

分離規則是命題演算或謂詞演算的公理系統的一個變形規則，其具體內容是：若是可推出的，並且A也是可推出的，則B也是可推出的。若用“ "表示“可推出的”，可表述為：若並且，則。這裡的A、 B是表示任一合式公式的元語言符號； “⊢”表示緊跟其後的公式為本系統所肯定，即為本系統的定理。即是說，如果A→B 和A都是系統中的定理，則B也是系統中的定理。例如，在命題演算中，由和，可得。在謂詞演算中，由和，可得。根據分離規則進行的推演，類似於普通邏輯中充分條件假言推理的肯定前件式。

這條規則可用圖式表示為：

這條規則實質上就是承認前件則必須承認後件的充分條件假言推理。

命題演算公理系統的變形規則

命題演算公理系統的變形規則是命題演算公理系統的一個組成部分，由一個或兩個公式轉換為另一個公式，即由一個或兩個公式推導出另一個公式的規則。以具體公理為出發點的命題演算的公理系統，一般以 代入規則和 分離規則為其變形規則。以公理圖式為出發點的命題演算的公理系統，可僅以分離規則為其變形規則。

命題演算的代入規則

命題演算的代入規則命題是演算公理系統的一個變形規則，可表述為：如果⊢A，則⊢ Aπ/B。這裡的A、B是表示任一合式公式的元語言符號; π是表示任一命題變元的元語言符號；“⊢”表示緊跟其後的公式為本系統所肯定，即為本系統的定理; Aπ/B表示將公式A中出現的某命題變元π處處代以公式B而得到的公式。即是說，如果一公式A是本系統的定理，那么將A 中的某命題變元π處處換以某公式B而得到的公式也是本系統的定理。例如，將公式p→(p∨q) 中的命題變元p處處代以⌝p而得到公式 ⌝p→(⌝p∨q)，由⊢p→(p∨q)，可得⊢⌝ p→(⌝p∨q)。命題演算的代入規則只允許把某命題變元代以某公式，不允許把不是命題變元的某公式代以另一公式; 如果某命題變元在一公式中多次出現，則對之進行的替代必須在其出現的每一處進行，並且處處換以同樣的公式。

關於分離規則的討論

雖說分離規則對推理本身而言已足夠，但為了推導方便起見，將從分離規則出發，引入一些導出規則。

假設已證明了定理，編號為(a)，又證明了定理，編號為(b)，由此可得，編號為(c)，記為分。可以看作對(a)和(b)實施分離規則的結果。換個角度來說，我們也可將看作對“(b)”實施“分(a)”規則的結果，即

分(a)規則： .

也就是說，每給一條定理(a)：，我們就有一條相應的分(a)規則。即由(a)的前件可得出(a)的後件。

同理，假設我們證明了一條定理，編號為(a)，又有定理(b)：和定理(c)：，由它們利用分離規則可得。其推理過程如下：

分(a)(b)=(d) ，

分(d)(c)=(e) .

將(d)式代人得

分分(a)(b)(c)=(e).

這裡我們既可以把看作兩次實施分離規則的結果，第一次是對(a)和(b)實施分離規則，第二次是對(d)和(c)實施分離規則，但也可將其看作對(b)和(c)實施“分分(a)”規則的結果，即

分分(a)規則： .

故由(a)的兩個前件，可以得出(a)的後件。

依次類推，如果有定理(a)：，我們就有如下規則：

分(a)規則：

分分(a)規則：

分分分(a)規則：

直言三段論

直言三段論是由直言命題所組成的一種推理形式，簡稱 三段論。傳統邏輯的三段論演繹體系是由亞里士多德創立的，在中世紀得以完善，現代的數理邏輯對三段論也作過專門的研究。

三段論的結構

一個直言三段論由三個直言命題所組成，其中兩個為前提，一個為結論。三個直言命題包含三個不相同的詞項，其中只在兩個前提中出現而不在結論中出現的詞項稱為中項，用字母“M”表示；在結論中作為主詞的詞項稱為小項，用字母“S”表示；在結論中作為賓詞的詞項稱為大項，用字母“P”表示。兩個前提中包含大項的前提稱為大前提，包含小項的前提稱為小前提。在排列順序上，通常大前提在前，其後是小前提，最後為結論。但這種順序不是絕對的。

三段論的公理

又稱曲全公理。直言三段論推理的依據。內容為：凡對一類事物有所肯定，則對該類事物中的每一個對象也有所肯定；凡對一類事物有所否定，則對該類事物中的每一個對象也有所否定。

三段論的規則

要保證直言三優論推理的有效性，就必須遵守一定的規則。三段論的規則共二類四條。第一類是關於詞項的規則：(一)在前提中，中項至少要周延一次；(二)詞項只有在前提中周延，才可在結論中周延。第二類是關於質的規則：(一)至少有一個前提必須是肯定的；(二)如果有一個前提是否定的，則結論必須是否定的。以這四條基本規則也可以證明一些從屬的規則，例如，兩個特稱的前提推不出結論；如果前提中有一個是特稱的，則結論必須是特稱的；如果結論是肯定的，則兩個前提必須是肯定的；如果結論是全稱的，則兩個前提必須是全稱的；如果結論是否定的，則兩個前提中必須有一個是否定的。

三段論的格

直言三段論中由於中項在前提中的位置不同而構成的不同形式。三段論有四個格。第一格，中項是大前提的主詞，小前提的賓詞。第二格，中項在大小前提中都是賓詞。第三格，中項在大小前提中都是主詞。第四格，中項是大前提的賓詞，小前提的主詞。四個格的結構如下圖：

根據三段論總的規則，結合各個格具體形式，可以引申出每格的具體規則。第一格：(一)大前提須是全稱的；(二)小前提須是肯定的。第二格：(一)兩個前提中須有一個是否定的；(二)大前提須是全稱的。第三格：(一)小前提須是肯定的；(二)結論須是特稱的。第四格：(一)如果大前提是肯定的，則小前提必須是全稱的；(二)如果小前提是肯定的，則結論必須是特稱的；(三)如果前提中有一個是否定的，則大前提必須是全稱的。

三段論的式

直言三段論的大前提、小前提和結論都可能由A、E、I、O中任一個命題充當，共有64種可能的組合；再考慮三段論有四個格，就有256種可能的組合每一種組合稱為一個式。在256個式中，符合三段論規則的叫有效式，違反三段論規則的叫無效式。三段論的有效式共24個，分別如下：

第一格：AAA，EAE，AII，EIO，(AAI)，(EAO)；

第二格：AEE，EAE，EIO，AOO，(AEO)，(EAO)；

第三格：AAI，AII，EAO，EIO，IAI，OAO；

第四格：AAI，AEE，EAO，EIO，IAI，(AEO)。

上例各式中19個不帶括弧的叫強式，5個帶括弧的叫弱式。弱式本可以得出全稱命題為結論，但只以特稱命題為結論。中世紀經院邏輯為了便於記憶，分別給這19個強式以特殊的名稱。並編成“格式歌訣”。例如，Barbara，Celarent分別表示第一格的AAA式和EAE式。除了這24個有效式外，其餘的232個式是無效式。

三段論的化歸

在傳統邏輯中，直言三段論是一個近似完整的公理體系。其中，第一格的AAA式和EAE式起著分理的作用，其他17個強式的有效性須通過這兩個式加以證明。證明的方法是用有效的邏輯方法把這17個式化歸(又叫還原)為第一格的AAA式和EAE式。化歸方法有兩種。一種是直接化歸，將前提或結論換位，或將兩前提對調，就可把其他格化歸為第一格。例如，第三格的IAI式具有下面的形式：

MIP

MAS/SIP

把它的大前提換位，再把大小前提對調，最後把結論換位，即成為：

MAS

PIM/PIS

這就是第一格的形式。另一種是間接化歸，使用歸謬法，把否定了的結論與一個否定了的前提對調，從而化歸為第一格。例如，第二格的AOO式具有下面的形式：

PAM

SOM/SOP

把結論SOP否定，得SAP；再把前提中的SOM否定，得SAM;然後把它們對調、即成為

PAM

SAP/SAM

這就是第一格的AAA式，所以使用這種方法，是因為前提中含有0命題，而0命題是不能換位的。

三段論的現代研究成果用謂詞邏輯的符號來表示三段論的推理式，則三段論的有效式都可從謂詞邏輯系統中推出，其中9個從兩個全稱前提得出特稱結論的式，須將主詞存在這一傳統邏輯隱含的前提揭示出來。這表明三段論推理只是謂詞邏輯的一部分。盧卡西維茨(1878—1965)用數理邏輯為工具，對三段論體系作了專門研究。他用a、b、c等表示項詞，用△，I代表運算元，採用前置號的方法，Aab表示所有a是b，Iab表示有的a是b。將Eab(所有a不是b)定義為Iab的否定，Oab(有的a不是b)定義為Aab的否定。用下面4條公理：

(一)Aaa

(二)Iaa

(三)Abc∧Aab→Aac

(四)Abc∧Iba→IbC

其中第三條公理是三段論第一格的AAA式，第四條公理是第三格的AII式。再藉助代入規則、分離規則以及命題演算的規律，就可推出直言命題的換位規律和所有的三段論的有效式。這個完全形式化的三段論公理系統的建立使人們對傳統邏輯的三段論體系有了新的認識。

命題演算分離規則