【正文】 個不同的極小項。若在極小項中，將命題變元的原形對應(yīng)1，否定對應(yīng)0，則每個極小項唯一地對應(yīng)一個二進(jìn)制數(shù)，該二進(jìn)制數(shù)的每一位正是使該極小項的真值為1的真值賦值。 【】兩個命題變元p, q生成的4個極小項為： 216。p217。216。q對應(yīng)00，記為m0 216。p217。q對應(yīng)01，記為m1 p217。216。q對應(yīng)10，記為m2 p217。q對應(yīng)11，記為m2由三個命題變元p, q, r生成的8個極小項為： 216。p217。216。q217。216。r對應(yīng)000，記為m0 216。p217。216。q217。r對應(yīng)001，記為m1 216。p217。q217。216。r對應(yīng)010，記為m2 216。p217。q217。r對應(yīng)011，記為m3 p217。216。q217。216。r對應(yīng)100，記為m4 p217。216。q217。r對應(yīng)101，記為m5 p217。q217。216。r對應(yīng)110，記為m6 p217。q217。r對應(yīng)111，記為m7 【】若析取范式中的簡單合取式都是極小項，則稱該析取范式為主析取范式。 【】任何命題公式存在唯一的主析取范式。 求一個公式的主析取范式是： [1] 先求該公式的一個析取范式。 [2] 如果該析取范式的某個簡單合取式A中既不含某個命題變元p，也不含它的否定216。p，則該簡單合取式變?yōu)槿缦滦问剑?A217。p)218。(A217。216。p)。 [3] 消除重復(fù)出現(xiàn)的命題變元或命題變元的否定，矛盾式及重復(fù)出現(xiàn)的極小項，并將每個極小項的命題變元或其否定按下標(biāo)順序或字典順序排列?！尽壳竺}公式的主析取范式 (1). 求(216。p174。q)217。(p174。r)的主析取范式 (2). 求(p174。q)218。(p217。r)的主析取范式【解答】(1)(216。p174。q)217。(p174。r)的一個析取范式是(p217。r)218。(q217。216。p)218。(q217。r)，我們將其中的每個簡單合取式展開為含有所有命題變元的極小項的析?。?p217。r)展開為(p217。q217。r)218。(p217。216。q217。r) (q217。216。p)展開為(216。p217。q217。r)218。(216。p217。q217。216。r)(q217。r)展開為(p217。q217。r)218。(216。p217。q217。r)因此(216。p174。q)217。(p174。r)的主析取范式為(p217。q217。r)218。(p217。216。q217。r)218。(216。p217。q217。r)218。(216。p217。q217。216。r)，按極小項所對應(yīng)的二進(jìn)制數(shù)的大小重新排列為(216。p217。q217。216。r)218。(216。p217。q217。r)218。(p217。216。q217。r)218。(p217。q217。r)。(2)(p174。q)218。(p217。r)的一個析取范式為(216。p)218。q218。(p217。r)，將其中每個簡單合取式展開為含有所有命題變元的極小項的析?。? (216。p)展開為(216。p217。q217。r)218。(216。p217。216。q217。r)218。(216。p217。q217。216。r)218。(216。p217。216。q217。216。r) q展開為(p217。q217。r)218。(216。p217。q217。r)218。(p217。q217。216。r)218。(216。p217。q217。216。r) (p217。r)展開為(p217。q217。r)218。(p217。216。q217。r)因此(p174。q)218。(p217。r)的主析取范式為：(216。p217。216。q217。216。r)218。(216。p217。216。q217。r)218。(216。p217。q217。216。r)218。(216。p217。q217。r)218。(p217。216。q217。r)218。(p217。q217。216。r)218。(p217。q217。r) 主析取范式也可從命題公式的真值表更容易地得到，對應(yīng)地，根據(jù)命題公式的主析取范式也可容易地構(gòu)造其真值表、判定其類型（矛盾式、可滿足式還是永真式）等。 關(guān)于極大項、主合取范式等有關(guān)內(nèi)容學(xué)生根據(jù)教材自學(xué)。作業(yè)：教材p60的9, 10, 11, 15, 17。7. 命題演算系統(tǒng) 命題演算系統(tǒng)是研究利用命題邏輯公式進(jìn)行推理的形式系統(tǒng)。這里的推理指的是前提和結(jié)論之間的邏輯關(guān)系，因此這種形式系統(tǒng)本身不注重前提本身的正確性，而關(guān)心的是是否能從前提有效地推出結(jié)論，討論什么是結(jié)論的有效證明。前提本身的正確性要在賦予形式系統(tǒng)一定的解釋的基礎(chǔ)上才能確定，這種解釋可以說是形式系統(tǒng)的語義。命題演算系統(tǒng)作為一個形式系統(tǒng)研究如何從公理，通過有限的規(guī)則來構(gòu)造有效的證明，這種證明僅僅是符號的改寫，本身沒有什么含義。 一個形式系統(tǒng)包括符號表、公式、公理及規(guī)則，符號表定義形式系統(tǒng)所使用的所有符號，公式是符號表上字符串，公式定義哪些字符串是形式系統(tǒng)所研究的合法對象。公理是構(gòu)造一切證明的前提，公理本身的正確性在形式系統(tǒng)中不關(guān)心，認(rèn)為是不證自明的公式。當(dāng)然在構(gòu)造形式系統(tǒng)的時候，公理的選擇是一定的外在依據(jù)的。規(guī)則是從公理出發(fā)構(gòu)造形式系統(tǒng)中定理的方法。定理就是從公理出發(fā)，使用規(guī)則能夠構(gòu)造出有效證明的公式，形式系統(tǒng)就是研究能夠得到什么定理。 【】命題演算系統(tǒng)P定義為： 1. P的符號表包括： [1]. 命題變元：小寫英文字母并可加下標(biāo) [2]. 聯(lián)結(jié)詞：216。、174。 [3]. 輔助符號：(, )（園括號） 2. P的公式歸納定義為： [1]. 命題變元是公式 [2]. 若A是公式，則(216。A)也是公式 [3]. 若A和B是公式，則(A174。B)也是公式 [4]. 所有公式都是通過有限次使用[1]、[2]和[3]得到。 3. P的公理有如下三類： [A1]. (A174。(B174。A)) [A2]. ((A174。(B174。C))174。((A174。B)174。(A174。C)) [A3]. (((216。A)174。(216。B))174。(B174。A)) 4. P的規(guī)則只有一條： [M]. 分離規(guī)則：由A和(A174。B)可得到B□ 【注解】關(guān)于以上定義，需要注意以下幾點： 1. 在系統(tǒng)P中只使用聯(lián)結(jié)詞216。和174。，這使得系統(tǒng)P比較簡單，但也失去了使用另外三個聯(lián)結(jié)詞217。、218。和171。的方便之處，為此可作如下約定，對于P中公式A和B： (A218。B)代表((216。A)174。B) (A217。B)代表(216。((216。A)218。(216。B))) (A171。B)代表((A174。B)217。(B174。A)) 注意，217。、218。和171。不是系統(tǒng)P的符號，只不過是為了使用方便而引入的符號。 2. 上述給出的公理是一種模式，其中每一條公理實際上代表了無限多個公式，因為其中的A, B, C是一個符號，實際上可代表任意的公式，例如對于[A2]，其中A可代表B174。C得到： (((B174。C)174。(B174。C))174。(((B174。C)174。B)174。((B174。C)174。C))注意在使用公式A替換公式B的符號C時，要將公式A替換B中所有的C。同樣分離規(guī)則也是一個模式?！尽棵}演算系統(tǒng)P中的證明是由P中公式組成的一個序列： A1, A2, …, An使得對每個i(1163。 i 163。 n)，下列兩個條件之一成立： (1). Ai是公理，或者 (2). Ai是由上述序列中Ai之前的某兩個公式Aj, Ak(1163。 j, k 163。 n)應(yīng)用分離規(guī)則(M)得到。此時A1, A2, …, An稱為An的一個證明，而An稱為P的一個內(nèi)定理，記為├An?！酢咀⒔狻筷P(guān)于以上定義，需要注意以下幾點： 1. ├也不是P中的符號，只是用├An來表明An是一個內(nèi)定理。 2. 所謂的用兩個公式Aj, Ak應(yīng)用分離規(guī)則(M)得到，是指{Aj, Ak} = {Aj, Aj174。Ai}或{Aj, Ak} = {Ak, Ak174。Ai}。 3. 若A1, A2, …, An是An的一個證明，則對每個Ai(1163。 i 163。 n)都有├Ai。 4. P的每個公理都是P中的內(nèi)定理。 5. 要證明一個公式A為P的內(nèi)定理，只要給出A的證明序列即可。【】設(shè)A, B是P中的公式，證明：├(A174。B)174。(A174。A)【證明】 (1). ├A174。(B174。A) // 公理[A1] (2). ├(A174。(B174。A))174。((A174。B)174。(A174。A)) // 公理[A2]，其中C用A代替 (3). ├(A174。B)174。(A174。A) // 分離規(guī)則(M)及(1)和(2)【】設(shè)A是P中的公式，證明：├(A174。A)【證明】 (1). ├A174。((B174。A)174。A) // 公理[A1] (2). ├(A174。((B174。A)174。A))174。((A174。(B174。A))174。(A174。A)) // 公理[A2] (3). ├((A174。(B174。A))174。(A174。A)) // 分離規(guī)則(M)及(1)和(2) (4). ├(A174。(B174。A) // 公理[A1] (5). ├(A174。A) // 分離規(guī)則(M)及(3)和(4)【】設(shè)A, B, C是P中的三個公式： [1]. 若├A，且├A174。B，則├B [2]. 若├A174。B，且├B174。C，則├A174。C【證明】[1]就是分離規(guī)則。對于[2]，證明如下： (1). ├(B174。C)174。(A174。(B174。C)) // [A1] (2). ├(B174。C) // 前提 (3). ├(A174。(B174。C)) // 分離規(guī)則 (4). ├(A174。(B174。C))174。((A174。B)174。(A174。C)) // [A2] (5). ├(A174。B)174。(A174。C) // 分離規(guī)則 (6). ├(A174。B) // 前提 (7). ├(A174。C) // 分離規(guī)則□ 以后稱此定理的[2]為傳遞規(guī)則(Tr)?！尽孔C明：├(216。A)174。(A174。B)【證明】 (1). ├(216。A)174。((216。B)174。(216。A)) // [A1] (2). ├((216。B)174。(216。A))174。(A174。B) // [A3] (3). ├(216。A)174。(A174。B) // 傳遞規(guī)則【】證明：[1]. ├(216。216。A)174。A[2]. ├A174。(216。216。A)【證明】[1]的證明如下： (1). ├(216。216。A)174。(216。A174。216。216。216。A) // (2). ├(216。A174。216。216。216。A)174。(216。216。A174。A) // [A3] (3). ├(216。216。A)174。(216。216。A174。A) // 傳遞規(guī)則 (4). ├(216。216。A174。(216。216。A174。A))174。((216。216。A174。216。216。A)174。(216。216。A174。A))// [A2] (5). ├(216。216。A174。216。216。A)174。(216。216。A174。A) // 分離規(guī)則 (6). ├(216。216。A174。216。216。A) // (7). ├(216。216。A174。A) // 分離規(guī)則 [2]的證明如下： (1). ├(216。216。216。A)174。(216。A) // [1] (2). ├(216。216。216。A174。216。A)174。(A174。216。216。A) // [A3] (3). ├A174。216。216。A // 分離規(guī)則【注解】通過以上例子，我們可發(fā)現(xiàn)在構(gòu)造公式的證明中可使用如下方法：1. 可靈活地使用公理，公理中的每個符號代表的是無限多的公式，公理中某個符號的所有出現(xiàn)可用某個公式替換。但這與教材p43頁的置換規(guī)則不同，教材沒有為命題邏輯公式的推理建立形式系統(tǒng)，而是根據(jù)命題邏輯公式的真值來討論推理，因此有所謂的等值公式的置換，而我們這里所定義的形式系統(tǒng)還沒有涉及到真值賦值，這里的證明僅僅是符號的改寫。建立形式系統(tǒng)的方法更符合計算機的思維方式，因為程序從本質(zhì)來說也是個形式系統(tǒng)，計算機將輸入變換到輸出也只是符號的改寫，至于程序員所認(rèn)為的程序功能，是程序員賦予程序的解釋，這種解釋計算機并不理解。也就是說，對于計算機學(xué)科，形式系統(tǒng)的推導(dǎo)和形式系統(tǒng)的含義是分開的，正是這種分離，才使得形式系統(tǒng)的推導(dǎo)可由計算機來機械地完成，而人們又可以賦予形式系統(tǒng)各種各樣的解釋來完成人們所需要的功能。2. 可使用分離規(guī)則和傳遞規(guī)則來構(gòu)造證明。3. 可使用已經(jīng)證明過的內(nèi)定理作為前提，這相當(dāng)于教材p43頁的結(jié)論引入規(guī)則。4. 教材中所討論的推理是在某種前提下的推理，下面我們在命題演算系統(tǒng)P中來定義這種推理?！尽吭O(shè)S是P中的一個公式集，稱P中的公式序列： A1, A2, …, An為前提S下推出An的一個證明，如果對每個i(1163。 i 163。 n)，下列三個條件之一成立： (1). Ai是公理，或者 (2). Ai206。S，或者 (3). Ai是由上述序列中Ai之前的某兩個公式Aj, Ak(1163。 j, k 163。 n)應(yīng)用分離規(guī)則(M)得到。此時記為S├An?！酢咀⒔狻繉τ谏鲜龆x，我們需要注意以下幾點：1. S中的公式不一定是P中的公理或內(nèi)定理，也不一定是有限集合?？梢哉fS是假設(shè)的前提，在前提S下的證明實際上是將S中的公式當(dāng)作“臨時公理”的一個證明。2. 易證：當(dāng)S = f時，f├A當(dāng)且僅當(dāng)├A，或者說├A就是沒有前提的證明。3. 易證：對P中的任意公式A及公式集S和S39。，若S39。205。S，且S39。├A，則有S├A。4. 易證，若A206。S，則有S├A?！尽孔C明：{A, B174。(A174。C)}├(B174。C)【證明】 (1). A // 前提 (2). A174。(B174。A) // 公理[A1] (3). (B174。A) // 分離規(guī)則: (1)和(2) (4). (B174。(A174。C)) // 前提 (5). (B174。(A174。C))174。((B174。A)174。(B174。C)) // 公理[A2] (6). (B174。A)174。(B174。C) // 分離規(guī)則: (4)和(5) (7). (B174。C) // 分離規(guī)則: (3)和(6) 下面利用上述定義和定理來形式化地討論教材p42中給出的推理定律的正確性。這里形式化的含義是不通過對公式的真值討論，而只是根據(jù)P系統(tǒng)的公理和分離規(guī)則來證明那些推理定律，當(dāng)然證明時允許使用我們已經(jīng)證明過的內(nèi)定理。為此，我們首先給出命題演算系統(tǒng)中最重要的一條定理，即演繹定理，通過演繹定理可將在某個前提S下的證明與P系統(tǒng)中的內(nèi)定理相聯(lián)