《邏輯學》（第二版）第五章謂詞邏輯的自然演繹系統杜國平教授馬克思主義理論研究和建設工程重點教材授課內容：

1.目標要旨

2.注意事項

3.總體框架

4.主要內容

5.重點難點

6.難點串講

7.案例補充授課內容：

1.目標要旨

2.注意事項

3.總體框架

4.主要內容

5.重點難點

6.難點串講

7.案例補充 1.目標要旨

通過謂詞邏輯自然演繹系統的知識傳授和技術訓練，使得學生掌握基本的謂詞邏輯推理知識，獲得謂詞邏輯推理的技術訓練，從而提高學生的邏輯思維能力。

授課內容：

1.目標要旨

2.注意事項

3.總體框架

4.主要內容

5.重點難點

6.難點串講

7.案例補充 2.注意事項1.1要闡述清楚推理規則背后的直觀思想；1.2要結合具體實例來進行闡述，舉例要自然、具體，不要太抽象。可以舉以正整數、實數為論域或者以人為論域的例子，這樣比較直觀，學生也容易理解。授課內容：

1.目標要旨

2.注意事項

3.總體框架

4.主要內容

5.重點難點

6.難點串講

7.案例補充 3.總體框架1.1謂詞邏輯自然推理系統；

1.2帶等詞的謂詞邏輯自然推理系統；

1.3推理實例分析。授課內容：

1.目標要旨

2.注意事項

3.總體框架

4.主要內容

5.重點難點

6.難點串講

7.案例補充 4.主要內容(1)自然推理系統的6條推理規則：全稱量詞消去規則，全稱量詞引入規則，存在量詞消去規則，存在量詞引入規則，等詞消去規則，等詞引入規則。(2)運用6條規則進行推理；(3)能夠運用推理技術對推理實例進行分析。授課內容：

1.目標要旨

2.注意事項

3.總體框架

4.主要內容

5.重點難點

6.難點串講

7.案例補充 5.重點難點(1)6條推理規則的附加條件。

(2)運用規則進行推理的技巧；

(3)運用推理技術進行推理實例分析。授課內容：

1.目標要旨

2.注意事項

3.總體框架

4.主要內容

5.重點難點

6.難點串講

7.案例補充 6.難點串講1.1謂詞邏輯自然推理系統

1.2帶等詞的謂詞邏輯自然推理系統 6.難點串講1.1謂詞邏輯自然推理系統

1.2帶等詞的謂詞邏輯自然推理系統1.1謂詞邏輯自然推理系統

其中包括4條推理規則1.1謂詞邏輯自然推理系統

其中包括4條推理規則因為經過多人修改，《邏輯學》2017年7月版教材中推理規則的表述不夠嚴謹。本PPT中推理規則的表述與《邏輯學》2017年7月版教材不盡一致，在新版教材中將對推理規則和相關證明作適當修正，謹向各位老師致歉！1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。其中t是一個項，并且t對A中的變元x可自由代入。全稱量詞消去規則的直觀含義是：如果所有個體都具有某個性質，那么“t”所代表的個體也具有該性質。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。

例1

x(AB),A(t/x)B(t/x)，其中t對A和B中x可自由代入。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。

例1

x(AB),A(t/x)B(t/x)，其中t對A和B中x可自由代入。這實際上是單稱三段論的AAA式。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。

例1

x(AB),A(t/x)B(t/x)，其中t對A和B中x可自由代入。證明：

[1]x(AB) pre [2]A(t/x) pre [3]A(t/x)B(t/x) E:[1] [4]B(t/x) E:[2],[3]1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。在運用全稱量詞消去規則時，要注意限制條件：t對A中x可自由代入。不滿足這個限制條件時，不能應用這條規則。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。例如，下面的全稱量詞消去規則的應用是錯誤的：

[1]xyRxy [2]yRyy1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。例如，下面的全稱量詞消去規則的應用是錯誤的：

[1]xyRxy [2]yRyy

第[2]步得到的公式yRyy=yRxy(y/x)，但y對yRxy中的x不是代入自由的。從[1]不能得到[2]。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。例如，下面的全稱量詞消去規則的應用是錯誤的：

[1]xyRxy [2]yRyy

例如：考慮論域D={a,b}，R的解釋為{(a,b),(b,a)}。在這個模型上[1]是真的，因為對D中每個個體，都有另一個個體與它有R關系。但[2]是假的，因為D中每個個體都與自身沒有R關系。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。例如，下面的全稱量詞消去規則的應用是錯誤的：

[1]xyRxy [2]yRyy

再如：考慮論域D為正整數集合N+

，Rxy解釋為y大于x。在這個模型上[1]表示的是任一正整數都存在一個比它大的正整數，這是真的。[2]表示的是存在一個正整數它比自身大，這是假的。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。例如，下面的全稱量詞消去規則的應用是錯誤的：

[1]xyRxy [2]yRyy

再如：考慮論域D為所有人的集合，Rxy解釋為y是x的母親。在這個模型上[1]表示的是任何一個人都有一個母親，這是真的。[2]表示的是存在一個人，她是自己的母親，這顯然是假的。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。例如，下面的全稱量詞消去規則的應用是錯誤的：

[1]xyRxy [2]yRyy

為什么？1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。例如，下面的全稱量詞消去規則的應用是錯誤的：

[1]xyRxy [2]yRyy

因為xyRxy中的x表示的是論域中的任一個體，而在第[2]步運用全稱消去由yRxy(y/x)得到yRyy時，其中的y對yRxy中的x不是代入自由的。即以y代入yRxy中的x時，由于y被量詞約束，使得代入后的y并不是論域中的任一個體，失去了原意。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。例如，下面的全稱量詞消去規則的應用是錯誤的：

[1]xyRxy [2]yRyy

其中t是一個項，并且t對A中的變元x可自由代入。1.1謂詞邏輯自然推理系統

一、全稱量詞消去規則（簡記為E）

如果xA，則A(t/x)。例如，下面的全稱量詞消去規則的應用是錯誤的：

[1]xyRxy [2]yRyy

其中t是一個項，并且t對A中的變元x可自由代入。限制條件必不可少！1.1謂詞邏輯自然推理系統

二、全稱量詞引入規則（簡記為I） 如果A(c/x)，則xA。

1.1謂詞邏輯自然推理系統

二、全稱量詞引入規則（簡記為I） 如果A(c/x)，則xA。

其中c是不受限制的新常元（用[c]表示），即c是不在前提集中出現的新常元。1.1謂詞邏輯自然推理系統二、全稱量詞引入規則（簡記為I） 如果A(c/x)，則xA。

其中c是不受限制的新常元（用[c]表示），即c是不在前提集中出現的新常元。全稱引入規則的直觀含義是：如果任意個體都具有性質A，那么所有對象都具有性質A。這里用新常元不受限制就是為了使它能夠代表任何個體。1.1謂詞邏輯自然推理系統二、全稱量詞引入規則（簡記為I） 如果A(c/x)，則xA。

其中c是不受限制的新常元（用[c]表示），即c是不在前提集中出現的新常元。如果a不是不受限制的新常元，推理就可能出現錯誤。1.1謂詞邏輯自然推理系統二、全稱量詞引入規則（簡記為I） 如果A(c/x)，則xA。

其中c是不受限制的新常元（用[c]表示），即c是不在前提集中出現的新常元。例如，以Pa為前提不能推出xPx。構造這樣一個模型：論域為所有正整數集合；P在論域上解釋為所有偶數的集合；a解釋為自然數“2”。顯然，“2是偶數”是真的，而“所有正整數都是偶數”是假的。1.1謂詞邏輯自然推理系統二、全稱量詞引入規則（簡記為I） 如果A(c/x)，則xA。

其中c是不受限制的新常元（用[c]表示），即c是不在前提集中出現的新常元。例2xAyA(y/x)，其中y對A中x可自由代入。1.1謂詞邏輯自然推理系統二、全稱量詞引入規則（簡記為I） 如果A(c/x)，則xA。

其中c是不受限制的新常元（用[c]表示），即c是不在前提集中出現的新常元。例2xAyA(y/x)，其中y對A中x可自由代入。 證明：

[1]xA pre [2]A(c/x) E:[1][c] [3]yA(y/x) I:[2]1.1謂詞邏輯自然推理系統

二、全稱量詞引入規則（簡記為I）

例3

x(AB)xAxB1.1謂詞邏輯自然推理系統

二、全稱量詞引入規則（簡記為I）

例3

x(AB)xAxB

證明：

[1]x(AB) pre [2] xA hyp [3] A(c/x) E:[2][c] [4] x(AB) reit:[1] [5] A(c/x)B(c/x) E:[4] [6] B(c/x) E:[3],[5] [7] xB I:[6] [8]xAxB I:[2]-[7]1.1謂詞邏輯自然推理系統

三、存在量詞消去規則（簡記為E）：

如果,A(c/x)B，則,xAB。

其中c是受限制的新常元（用[c*]表示），即c不在前提集和B中出現。

1.1謂詞邏輯自然推理系統三、存在量詞消去規則（簡記為E）：

如果,A(c/x)B，則,xAB。

其中c是受限制的新常元（推理過程中用[c*]表示），即c不在前提集和B中出現。存在量詞消去規則的直觀含義是：如果假定論域中有一個具有性質A的對象c，由此可以得出結論B，那么我們就可以得出：只要論域中存在個體具有性質A，就可以得出結論B。在規則中我們用符號*表示所使用的常元c是受限制的，即這個c不能代表任意的個體，而只能代表論域中具有性質A的那個證據個體。1.1謂詞邏輯自然推理系統三、存在量詞消去規則（簡記為E）：

如果,A(c/x)B，則,xAB。

其中c是受限制的新常元（推理過程中用[c*]表示），即c不在前提集和B中出現。注意：不能對受限制的新常元c進行全稱引入。例如，如果c是受限制的新常元，那么由A(c/x)推不出xA。1.1謂詞邏輯自然推理系統三、存在量詞消去規則（簡記為E）：

如果,A(c/x)B，則,xAB。

其中c是受限制的新常元（推理過程中用[c*]表示），即c不在前提集和B中出現。例9

x(SxPa),xSxPa 證明： [1]x(SxPa) pre [2]xSx pre [3] Sc hyp:[c*] [4] x(SxPa) reit:[1] [5] ScPa E:[1] [6] Pa E:[3][4] [7]Pa E:[1]-[6]1.1謂詞邏輯自然推理系統三、存在量詞消去規則（簡記為E）：

如果,A(c/x)B，則,xAB。

其中c是受限制的新常元（推理過程中用[c*]表示），即c不在前提集和B中出現。例9

x(SxPa),xSxPa 證明： [1]x(SxPa) pre [2]xSx pre [3] Sc hyp:[c*] [4] x(SxPa) reit:[1] [5] ScPa E:[1] [6] Pa E:[3][4] [7]Pa E:[1]-[6]1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）：

如果A(t/x)，則xA。其中t是一個項，并且t對A中的變元x是可自由代入。

1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）：

如果A(t/x)，則xA。其中t是一個項，并且t對A中的變元x是可自由代入。 存在引入規則的直觀含義是：如果t所代表的個體具有性質A，那么論域中存在具有性質A的對象。1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）：

如果A(t/x)，則xA。其中t是一個項，并且t對A中的變元x是可自由代入。 例10

xAxA

證明：

[1] xA hyp [2] A(c/x) E:[1] [3] xA I:[2] [4]xAxA I:[1]-[3]1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例15x(AB)xAxB1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例15x(AB)xAxB 證明：

[1]x(AB) pre [2] A(c/x)B(c/x)

hyp:[c*] [3] A(c/x) E:[2] [4] xA I:[3] [5] B(c/x) E:[2] [6] xB I:[5] [7] xAxB I:[4],[6] [8]xAxB E:[1]-[7]1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例15x(AB)xAxB

定理15的逆不成立。即由xAxB推不出x(AB)。例如，以正整數作為論域，Ax解釋為x是偶數，Bx解釋為x是奇數，“存在正整數是偶數，并且存在正整數是奇數”是一個真命題，但是“存在正整數既是偶數又是奇數”卻是一個假命題。再如，以人為論域，Ax解釋為x是大于60的老人，Bx解釋為x是小于6歲的幼兒，“有人是大于60的老人，有人是小于6歲的幼兒”是一個真命題，但是“有人既是大于60的老人，又是小于6歲的幼兒”卻是一個假命題。1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例17xyAyxA 證明： [1]xyA pre [2] yA(c/x) hyp:[c*] [3] A(c/x)(d/y) E:[2][d] [4] xA(d/y) I:[3] [5] yxA I:[4] [6]yxA

E:[1]-[5]1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例17xyAyxA

該定理表明，如果論域中存在對象與論域中的所有對象具有關系A，那么論域中的所有對象均存在與其具有關系A的對象。例如，如果至少有一個人尊重所有的人（包括他自己），那么可以得出，所有的人都至少被一個人尊重。1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例17xyAyxA

定理17的逆命題不成立。即由yxA推不出xyA。例如，以自然數作為論域，“所有自然數都存在自然數比它大”是一個真命題，但是“存在自然數比所有自然數大”卻是一個假命題。再如，以所有人為論域，“所有的人都存在一個人是其父親”是一個真命題，但是“存在一個人是所有人的父親”卻是一個假命題。1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例18xAxA

1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例18xAxA 證明： 先證xAxA [1]xA pre [2] xA hyp [3] A(c/x) hyp:[c*] [4] xA reit:[1] [5] A(c/x) E:[4] [6] A(c/x)(A(c/x)BB)

命題邏輯

[7] A(c/x)BB E:[3],[6] [8] BB E:[5],[7] [9] BB

E:[1]-[8] [10] B

E:[9] [11] B

E:[9] [12]xA I:[2]-[11]

1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例18xAxA 證明：

再證xAxA [1]xA pre [2] A(a/x) hyp[a] [3] xA I:[2] [4] xA reit:[1] [5]A(a/x) E:[2][4] [6]xA I:[5]

1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例18xAxA 證明： 先證xAxA [1]xA pre [2] xA hyp [3] A(c/x) hyp:[c*] [4] xA reit:[1] [5] A(c/x) E:[4] [6] A(c/x)(A(c/x)BB)

命題邏輯

[7] A(c/x)BB E:[3],[6] [8] BB E:[5],[7] [9] BB

E:[1]-[8] [10] B

E:[9] [11] B

E:[9] [12]xA I:[2]-[11]

歸謬法

1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例18xAxA 證明：

再證xAxA [1]xA pre [2] A(a/x) hyp[a] [3] xA I:[2] [4] xA reit:[1] [5]A(a/x) E:[2][4] [6]xA I:[5]

反證法

1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例18xAxA

例19xAxA

1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例18xAxA

例19xAxA

例20xAxA

1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例18xAxA

例19xAxA

例20xAxA

證明： 先證xAxA [1]xA pre [2] xA hyp [3] xA 例18:[2] [4] xA reit:[1] [5]xA E:[2]-[4]1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）：

例18xAxA

例19xAxA

例20xAxA

證明：

再證xAxA [1]xA pre [2] xA hyp [3] xA 例18:[2] [4] xA reit:[1] [5]xA I:[2]-[4]

1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）： 例18xAxA

例19xAxA

例20xAxA

證明： 先證xAxA [1]xA pre [2] xA hyp [3] xA 例18:[2] [4] xA reit:[1] [5]xA E:[2]-[4]

反證法1.1謂詞邏輯自然推理系統

四、存在量詞引入規則（簡記為I）：

例18xAxA

例19xAxA

例20xAxA

證明：

再證xAxA [1]xA pre [2] xA hyp [3] xA 例18:[2] [4] xA reit:[1] [5]xA I:[2]-[5] 歸謬法

1.2帶等詞的謂詞邏輯自然推理系統

1.2帶等詞的謂詞邏輯自然推理系統

一、等詞消去規則（簡記E）：

1.2帶等詞的謂詞邏輯自然推理系統

一、等詞消去規則（簡記E）： A(t1/x)A(t2/x)

t1t2t1t2

A(t2/x) A(t1/x)

其中t1和t2是項，分別對A中x可自由代入。1.2帶等詞的謂詞邏輯自然推理系統

一、等詞消去規則（簡記E）： A(t1/x)A(t2/x)

t1t2t1t2

A(t2/x) A(t1/x)

其中t1和t2是項，分別對A中x可自由代入。 等詞消去規則的直觀含義是：如果t1（或t2）所代表的個體具有性質A，那么t2（或t1）所代表的同一個個體也具有性質A。1.2帶等詞的謂詞邏輯自然推理系統

二、等詞引入規則（簡記I）：

tt1.2帶等詞的謂詞邏輯自然推理系統

二、等詞引入規則（簡記I）：

tt

等詞引入規則的直觀含義是：任何個體與自身相等。1.2帶等詞的謂詞邏輯自然推理系統

二、等詞引入規則（簡記I）：

tt

等詞引入規則的直觀含義是：任何個體與自身相等。 例26abba1.2帶等詞的謂詞邏輯自然推理系統

二、等詞引入規則（簡記I）：

tt

等詞引入規則的直觀含義是：任何個體與自身相等。 例26abba

證明：

[1]ab pre [2]aa I [3]ba E:[1],[2]1.2帶等詞的謂詞邏輯自然推理系統

二、等詞引入規則（簡記I）：

tt

等詞引入規則的直觀含義是：任何個體與自身相等。 例26abba

證明：

[1]ab pre [2]aa I [3]ba E:[1],[2]1.2帶等詞的謂詞邏輯自然推理系統

二、等詞引入規則（簡記I）：

tt

等詞引入規則的直觀含義是：任何個體與自身相等。 例26abba

證明：

[1]ab pre [2]aa I [3]ba E:[1],[2]1.2帶等詞的謂詞邏輯自然推理系統

例27

abbaab,bcac1.2帶等詞的謂詞邏輯自然推理系統

例27

abbaab,bcac

證明：

[1]ab pre [2]bc pre [3]ac E:[1],[2]1.2帶等詞的謂詞邏輯自然推理系統

例27

abbaab,bcac

證明：

[1]ab pre [2]bc pre [3]ac E:[1],[2]1.2帶等詞的謂詞邏輯自然推理系統

例28

ab,acbc1.2帶等詞的謂詞邏輯自然推理系統

例28

ab,acbc

證明：

[1]ab pre [2]ac pre [3]bc E:[1],[2]1.2帶等詞的謂詞邏輯自然推理系統

例28

ab,acbc

證明：

[1]ab pre [2]ac pre [3]bc E:[1],[2]1.2帶等詞的謂詞邏輯自然推理系統

例28

ab,acbc

證明：

[1]ab pre [2]ac pre [3]bc E:[1],[2]1.2帶等詞的謂詞邏輯自然推理系統

例29

x(y(xyPy)Px)1.2帶等詞的謂詞邏輯自然推理系統

例29

x(y(xyPy)Px)

證明： [1] y(ayPy) hyp[a] [2] acPc hyp[c*] [3] ac E:[2] [4] Pc E:[2] [5] Pa E:[3],[4] [6] Pa E:[1]-[5] [7]y(ayPy)Pa I:[1]-[6] [8]x(y(xyPy)Px) I:[7]授課內容：

1.目標要旨

2.注意事項

3.總體框架

4.主要內容

5.重點難點

6.難點串講

7.案例補充 6.案例補充

例1所有的偶數(Ex)都能被2整除(Dx)，所有的6的倍數(Mx)都是偶數，因此，所有的6的倍數都能被2整除。 6.案例補充

例1所有的偶數(Ex)都能被2整除(Dx)，所有的6的倍數(Mx)都是偶數，因此，所有的6的倍數都能被2整除。 x(ExDx),x(MxEx)x(MxDx) 6.案例補充

例1所有的偶數(Ex)都能被2整除(Dx)，所有的6的倍數(Mx)都是偶數，因此，所有的6的倍數都能被2整除。 x(ExDx),x(MxEx)x(MxDx)

證明： [1]x(ExDx)

pre [2]x(MxEx)

pre [3]EcDc

E:[1] [4]McEc

E:[2] [5] Mc hyp [6] Ec

E:[4][5] [7] Dc

E:[3][6] [8]McDc

I:[5]-[7] [9]x(MxDx) I:[8] 6.案例補充

例2

所有的馬(Fx)都是動物(Ax)。因此，所有的馬頭都是動物頭(Hxy：y是x的頭)。 6.案例補充

例2

所有的馬(Fx)都是動物(Ax)。因此，所有的馬頭都是動物頭(Hxy：y是x的頭)。

x(FxAx)x(y(FyHxy)y(AyHxy) 6.案例補充

例2

所有的馬(Fx)都是動物(Ax)。因此，所有的馬頭都是動物頭(Hxy：x是y的頭)。

x(FxAx)x(y(FyHxy)y(AyHxy)

證明： [1]x(FxAx)

pre [2] y(FyHay) hyp[a] [3] FcHac hyp:[c*] [4] Fc E:[3] [5] Hac E:[3] [6] x(FxAx) reit:[1] [7] FcAc E:[6] [8] Ac E:[4][7] [9] AcHac I:[5][8] [10] y(AyHay)

I:[9] [11] y(AyHay) E:

[1]-[10] [12]y(FyHay)y(AyHay) I:[2]-[11] [13]x(y(FyHxy)y(AyHxy) I:[12] 6.案例補充

例3

任何一條魚(Fx)都比任一較它小一點的魚游得快(Sxy：x比y游得快；Lxy：x大于y)。所以，如果有一條最大的魚就有一條游得最快的魚。 6.案例補充

例3

任何一條魚(Fx)都比任一較它小一點的魚游得快(Sxy：x比y游得快；Lxy：x大于y)。所以，如果有一條最大的魚就有一條游得最快的魚。x(Fxy(FyLxySxy))x(F(x)y(Fy(xy)Lxy))x(Fxy(Fy(xy)Sxy)) 6.案例補充

x(Fxy(FyLxySxy))x(F(x)y(Fy(xy)Lxy))x(Fxy(Fy(xy)Sxy))

證明： [1]x(Fxy(FyLxySxy))

pre [2] x(F(x)y(Fy(xy)Lxy))

hyp [3] F(c)y(Fy(cy)Lcy))

E:[2][c*] [4] Fc E:[3] [5] y(Fy(cy)Lcy))

E:[3]