析取引入規則

析取引入規則

如果已知一個合式公式為真,那么這個合式公式就可以和任意的合式公式構成析取。因為如果一個合式公式本身是真的,那么它和其他任意的合式公式所構成的析取就能夠保證其為真,即只要這個析取裡面兩個合式公式至少有一個是真的,那么析取就可以保證是真實的。所以已知為真的公式可以和任意的公式構成析取。由於結論當中引入了析取真值聯結詞,因此叫做析取引入規則(introduction rule of disjunction)。

基本介紹

析取引入規則指某些自然推理系統中的推理規則之一。簡記為∨Ⅰ或V+。

可表述為兩種形式:

(1)若Γ├A,則Γ├A∨B;

(2)若Γ├B,則Γ├A∨B。

其中Γ是任意的公式的集合,A、B是公式,├是推出關係。

這一規則意為:若Γ可以推出A,則Γ可以推出A與B的析取式A∨B;若Γ可以推出B,則Γ亦可以推出A∨B。這一規則又可用如下的圖式來表示:

析取引入規則 析取引入規則

也可以表述為如下的圖式:

析取引入規則 析取引入規則

相關概念

析取式

析取式是用析取詞聯結兩個公式構成的真值形式。如p∨q、 (p∧q) ∨⌝r、(p→q) ∨ (p→r) 等等。有時也特指由析取詞聯結兩個命題變元構成的基本真值形式,即p∨q (讀 作“p析取q”,或“p或者 q”)。析取式與其析取支 (即 由析取詞聯結的兩個公式)之間 的真值關係,可用p∨q的真值 表來表示 (以“T” 表示真,以 “F” 表示假) :

析取引入規則 析取引入規則

此表說明,當p和q皆真,或p和q中有一個為真時,p∨q為真; 當p和q皆假時,p∨q為假。用任一其他公式代替命題變 元p或q,並不會改變這種真值 關係。析取式是相容的選言命題的真值形式,它捨去了相容的選言命題的支命題之間在內容、意義上的聯繫。人們在日常思維中 運用選言命題時,總是針對有關某一問題的若干可能情況作出斷 定的,因而不但要求選言支之間有一定的內容、意義上的聯繫,而且要求每個選言支都是有可能 真的。象“屈原是詩人,或者地球是圓的” (其形式為p∨q)、 “屈原是詩人,或者屈原既是詩人又不是詩人” (其形式為p∨ (p∧⌝p) ) 這樣的選言命題,儘管從真值形式來看是真 的,但實際上並不被認為是有意義的。

謂詞邏輯的自然推理系統

直覺主義謂詞邏輯的自然推理系統是由根岑於1934年建構的推理系統。簡記為系統IQN。它的初始符號中有邏輯聯結詞和量詞¬(否定)、∧(合取)、∨(析取)、→(直覺主義蘊涵)、ᗄ(全稱量詞)、∃(存在量詞),對它們可以作直覺主義的構造性解釋。系統IQN包含如下的推理規則:肯定前提規則、合取引入規則、析取引入規則、蘊涵引入規則、否定引入規則、合取消去規則、析取消去規則、蘊涵消去規則、否定消去規則、全稱量詞引入規則、存在量詞引入規則、全稱量詞消去規則、存在量詞消去規則。系統IQN是經典謂詞邏輯的自然推理系統QN的真子系統。“間接證明規則”不是系統IQN中有效的推理規則,如果把“間接證明規則”添加到系統IQN中去,就得到了經典謂詞邏輯的自然推理系統QN,即系統QN=系統IQN+間接證明規則。系統IQN等價於公理化的直覺主義謂詞演算IQ,在語義解釋(模型)的基礎上,可以證明系統IQN的可靠性和完全性。

命題邏輯的自然推理系統

直覺主義命題邏輯的自然推理系統是由根岑於1934年建構的推理系統。簡記為系統IPN。它的初始符號中有邏輯聯結詞¬(否定)、∧(合取)、∨(析取)和→(直覺主義蘊涵),對它們可以作直覺主義的構造性解釋。系統IPN包含如下的推理規則:肯定前提規則、合取引入規則、析取引入規則、蘊涵引入規則、否定引入規則、合取消去規則、析取消去規則、蘊涵消去規則、否定消去規則。系統IPN是經典命題邏輯的自然推理系統PN的真子系統。“間接證明規則”不是系統IPN中有效的推理規則,如果把“間接證明規則”添加到系統IPN中去,就得到了經典命題邏輯的自然推理系統PN,即系統PN=系統IPN+間接證明規則。系統IPN等價於公理化的直覺主義命題演算IP,在語義解釋(模型)的基礎上,可以證明系統IPN的可靠性和完全性,系統IPN還是能行可判定的。

相關詞條

熱門詞條

聯絡我們