logic

「邏輯學」。釐清前因後果，把整件事情想清楚的學問。

音譯「邏輯學」、意譯「推理學」或「論證學」。台灣採用音譯，原因大概很恐怖。

台灣也有人譯作「理則學」。但是這個名稱不是學者提出來的，而是知名幫派份子兼通緝要犯提出來的。聯合日本人顛覆清國，聯合蘇聯人顛覆民國。部下殺人如麻，是個恐怖的人。

邏輯學與程式語言

邏輯學不屬於計算機科學系的授課範圍。然而卡內基美隆大學CMU的計算機科學系相當另類。他們開設了邏輯學與程式語言的一系列課程，並且要求學生至少修習一門課程。

http://coursecatalog.web.cmu.edu/schools-colleges/schoolofcomputerscience/undergraduatecomputerscience/#bscurriculumtextcontainer
15-312	Foundations of Programming Languages
15-314	Programming Language Semantics
15-316	Software Foundations of Security and Privacy
15-317	Constructive Logic
15-414	Bug Catching: Automated Program Verification
15-424	Logical Foundations of Cyber-Physical Systems
17-355	Program Analysis
17-363	Programming Language Pragmatics
80-413	Category Theory

proposition

邏輯命題宛如數學變數。

變數習慣用p、q、r。

  | name          | English       | Chinese
--| --------------| --------------| ------------------
p | proposition   | proposition   | 命題

數值只有兩種：⊤、⊥。

  | name          | English       | Chinese
--| --------------| --------------| ------------------
⊤ | true          | true          | 真
⊥ | false         | false         | 假

註：邏輯學採用⊤ ⊥。數學採用T F。
　　數學當中，⊥是垂直。

connective

邏輯連詞宛如數學運算。

運算只有五種：¬、∧、∨、→、↔。

  | name           | English        | Chinese
--| ---------------| ---------------| ------------------
¬ | negation       | not            | 非
∧ | conjunction    | and            | 且
∨ | disjunction    | or             | 或
→ | implication    | if ... then ...| 若…則…
↔ | bi-implication | if and only if | 若且唯若、当且仅当

註：邏輯學採用→ ↔。數學採用⇒ ⇔。
　　數學當中，→是趨近，↔是對應。

針對一種運算（多種運算），枚舉輸入輸出，製作表格，稱作「真值表truth table」。看了真值表，就知道了一種運算的功能。

 p | q ‖ ¬p  | p∧q | p∨q | p→q | p↔q 
---|---‖-----|-----|-----|-----|-----
 ⊤ | ⊤ ‖  ⊥  |  ⊤  |  ⊤  |  ⊤  |  ⊤  
 ⊤ | ⊥ ‖  ⊥  |  ⊥  |  ⊤  |  ⊥  |  ⊥  
 ⊥ | ⊤ ‖  ⊤  |  ⊥  |  ⊤  |  ⊤  |  ⊥  
 ⊥ | ⊥ ‖  ⊤  |  ⊥  |  ⊥  |  ⊤  |  ⊤  

compound proposition

複合命題宛如數學算式。

(p ∧ (p → q)) → q

connective precedence and connective associativity

優先權與結合性宛如先乘除後加減。

優先權：相異運算子的運算順序。

優先權即是上述表格順序¬ ∧ ∨ → ↔。¬最高↔最低。
例如p ∨ q ∧ r的運算順序是p ∨ (q ∧ r)。
例如p → q ∧ r的運算順序是p → (q ∧ r)。

結合性：相同運算子的運算順序。

結合性各自不同。
一、¬不討論結合性。畢竟是一元運算。
二、∧ ∨ ↔可以是左結合或右結合。兩者運算結果相同。
　　例如p ∧ q ∧ r的運算順序可以是(p ∧ q) ∧ r或p ∧ (q ∧ r)。
三、→是右結合。
　　例如p → q → r的運算順序是p → (q → r)。

如果覺得太複雜，那麼可以簡化成一律都是右結合。

logical operation in programming language

程式語言裡面也有邏輯變數，稱作布林Boolean。

logical variable | programming language
-----------------| --------------------
proposition      | Boolean

多數程式語言裡面沒有邏輯數值，以整數1和整數0代替。

例如C、C++、Python、Rust，關鍵字true等同整數1。

logical value    | programming language
-----------------| --------------------
⊤ true           | 1 integer one
⊥ false          | 0 integer zero

少數程式語言裡面才有邏輯數值，同樣也是兩種。

例如C#、JavaScript。

logical value    | programming language
-----------------| --------------------
⊤ true           | true  true
⊥ false          | false false

程式語言裡面也有邏輯運算，但是只剩三種。

logical operator | programming language
-----------------| --------------------
¬ negation       | !  logical NOT
∧ conjunction    | && logical AND
∨ disjunction    | || logical OR
→ implication    |
↔ bi-implication |

三種就夠用了。p→q即¬p∨q。p↔q使用==。

 p | q ‖ p→q | ¬p∨q 
---|---‖-----|------
 ⊤ | ⊤ ‖  ⊤  |  ⊤   
 ⊤ | ⊥ ‖  ⊥  |  ⊥   
 ⊥ | ⊤ ‖  ⊤  |  ⊤   
 ⊥ | ⊥ ‖  ⊤  |  ⊤   

statement

邏輯敘述宛如數學函數function。

一個式子，未知數值。

(p ∧ (p → q)) → q

interpretation

邏輯解釋宛如數學函數求值evaluation。

an interpretation:
let p = ⊤
    q = ⊤
get (p ∧ (p → q)) → q = ⊤

another interpretation:
let p = ⊤
    q = ⊥
get (p ∧ (p → q)) → q = ⊤

    :
    :

各個變數代入各種數值，建立真值表。

 p | q ‖ p→q | p∧(p→q) | (p∧(p→q))→q
---|---‖-----|---------|------------
 ⊤ | ⊤ ‖  ⊤  |    ⊤    |      ⊤
 ⊤ | ⊥ ‖  ⊥  |    ⊥    |      ⊤
 ⊥ | ⊤ ‖  ⊤  |    ⊥    |      ⊤
 ⊥ | ⊥ ‖  ⊤  |    ⊥    |      ⊤

tautology / contradiction

複合命題細分為：

tautology    ：恆真句。各個變數代入各種數值，皆求得⊤。
contradiction：恆假句。各個變數代入各種數值，皆求得⊥。
contingency  ：偶真句。上述兩種情況以外。

例如(p∧(p→q))→q是恆真句，¬((p∧(p→q))→q)是恆假句，p∧(p→q)是偶真句。

邏輯學家借用tautology和contradiction這兩個語言學詞彙，作為恆真句和恆假句。這兩個語言學詞彙的原意不是恆真和恆假。tautology原意是同義反覆，中文音譯為套套邏輯。contradiction原意是語意相左，中文意譯為矛盾。:-(

有些邏輯學家創造logical truth和logical falsity這兩個詞彙，作為恆真句和恆假句。這兩個詞彙容易跟true和false搞混。:-(

UVa 11108

equivalence

邏輯等價宛如數學恆等式identity。

p → q ≡ ¬p ∨ q

左式右式的真值表相符。左式右式同時是⊤、同時是⊥。

 p | q ‖ p→q | ¬p∨q 
---|---‖-----|------
 ⊤ | ⊤ ‖  ⊤  |  ⊤   ✔
 ⊤ | ⊥ ‖  ⊥  |  ⊥   ✔
 ⊥ | ⊤ ‖  ⊤  |  ⊤   ✔
 ⊥ | ⊥ ‖  ⊤  |  ⊤   ✔

恆真句、恆假句，表示成邏輯等價：

(p∧(p→q))→q ≡ ⊤        tautology
¬((p∧(p→q))→q) ≡ ⊥     contradiction

equivalence改寫成複合命題

≡換成↔。

logical equivalence: p → q ≡ ¬p ∨ q
tautology:           p → q ↔ ¬p ∨ q ≡ ⊤

觀察真值表。邏輯等價成立，複合命題恆真。

 p | q ‖ p→q | ¬p∨q   	 p → q ↔ ¬p ∨ q 
---|---‖-----|------  	----------------
 ⊤ | ⊤ ‖  ⊤  |  ⊤   ✔	       ⊤
 ⊤ | ⊥ ‖  ⊥  |  ⊥   ✔	       ⊤
 ⊥ | ⊤ ‖  ⊤  |  ⊤   ✔	       ⊤
 ⊥ | ⊥ ‖  ⊤  |  ⊤   ✔	       ⊤

rule of replacement

邏輯學家已經發明許多取代規則。以下介紹其中三個：

一、雙重否定定律double negation law：

¬¬p ≡ p

二、笛摩根定律De Morgan's law：

¬(p ∧ q) ≡ ¬p ∨ ¬q
¬(p ∨ q) ≡ ¬p ∧ ¬q

三、逆否命題定律contraposition law：

p → q ≡ ¬q → ¬p

statement

邏輯敘述宛如數學運算式expression。

一個式子，未知數值。

(p ∧ (p → q))

argument

邏輯論點宛如數學方程式equation。

一個式子（甚至多個式子），假設數值。

(p ∧ (p → q)) = ⊤

inference狹義版本

邏輯推論宛如數學方程組求解equation solving。

假設大量敘述的數值，求得特定敘述的數值。

這些敘述分別稱作「前提premiss」與「結論conclusion」。

assume (p → q) = ⊤      (premiss)
       ¬(q → r) = ⊥     (premiss)
solve (p → r) = ?       (conclusion)

建立真值表，嘗試求解。

 p | q | r ‖ p→q | ¬(q→r) | p→r 
---|---|---‖-----|--------|-----
 ⊤ | ⊤ | ⊤ ‖  ⊤  |    ⊥   |  ⊤  ✔
 ⊤ | ⊤ | ⊥ ‖  ⊤  |    ⊤   |  ⊥  
 ⊤ | ⊥ | ⊤ ‖  ⊥  |    ⊥   |  ⊤  
 ⊤ | ⊥ | ⊥ ‖  ⊥  |    ⊥   |  ⊥  
 ⊥ | ⊤ | ⊤ ‖  ⊤  |    ⊥   |  ⊤  ✔
 ⊥ | ⊤ | ⊥ ‖  ⊤  |    ⊤   |  ⊤  
 ⊥ | ⊥ | ⊤ ‖  ⊤  |    ⊥   |  ⊤  ✔
 ⊥ | ⊥ | ⊥ ‖  ⊤  |    ⊥   |  ⊤  ✔

邏輯推論，可能成功，可能失敗。

成功稱作「有效valid」。失敗稱作「無效invalid」。

一、前提充足，結論得以確定，要嘛全部⊤，要嘛全部⊥。（有效）
　　宛如數學唯一解unique solution。
二、前提不足，結論無法確定，既有⊤也有⊥。（無效）
　　宛如數學無限多解infinitely many solution。
三、前提相左，前提假設數值，真值表找不到這種組合。（無效）
　　宛如數學無解inconsistency。

有效時，可以調整每個敘述，適度追加¬，使得數值都是⊤。

assume (p → q) = ⊤
       (q → r) = ⊤
determine (p → r) = ⊤

有效時，真值表當中，當前提皆是⊤，則結論必須是⊤。

 p | q | r ‖ p→q | q→r | p→r 
---|---|---‖-----|-----|-----
 ⊤ | ⊤ | ⊤ ‖  ⊤  |  ⊤  |  ⊤  ✔
 ⊤ | ⊤ | ⊥ ‖  ⊤  |  ⊥  |  ⊥    
 ⊤ | ⊥ | ⊤ ‖  ⊥  |  ⊤  |  ⊤    
 ⊤ | ⊥ | ⊥ ‖  ⊥  |  ⊤  |  ⊥    
 ⊥ | ⊤ | ⊤ ‖  ⊤  |  ⊤  |  ⊤  ✔
 ⊥ | ⊤ | ⊥ ‖  ⊤  |  ⊥  |  ⊤    
 ⊥ | ⊥ | ⊤ ‖  ⊤  |  ⊤  |  ⊤  ✔
 ⊥ | ⊥ | ⊥ ‖  ⊤  |  ⊤  |  ⊤  ✔

有效時，可以寫成直式或者橫式。不必寫= ⊤。

特殊等號⊨稱作「導致entailment」。

直式     	半直半橫         	橫式
p → q    	p → q , q → r    	p → q , q → r ⊨ p → r
q → r    	⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
⎯⎯⎯⎯⎯    	p → r
p → r

inference廣義版本

邏輯學家採用廣義版本。允許無解。

前提相左的情況，本來視作無效，現在視作有效。

前提相左的情況，前提們形成恆假句。

p₁ , p₂ , ... , pₙ ⊨ q is valid when p₁ ∧ p₂ ∧ ... ∧ pₙ ≡ ⊥

前提恆假導致結論可真可假，稱作「爆炸explosion」。

經典範例：p是真、非p是真，導致任何敘述是真。

p, ¬p ⊨ q

也可以是假。

p, ¬p ⊨ ¬q

廣義版本，差別只在於爆炸，視作有效。:-(

inference改寫成複合命題

,換成∧。⊨換成→。

logical inference: p → q  ,  q → r  ⊨  p → r
tautology:        (p → q) ∧ (q → r) → (p → r) ≡ ⊤

觀察真值表。邏輯推論有效，複合命題恆真。

 p | q | r ‖ p→q | q→r | p→r   	 (p→q) ∧ (q→r) → (p→r)
---|---|---‖-----|-----|-----  	----------------------
 ⊤ | ⊤ | ⊤ ‖  ⊤  |  ⊤  |  ⊤  ✔	           ⊤
 ⊤ | ⊤ | ⊥ ‖  ⊤  |  ⊥  |  ⊥    	           ⊤
 ⊤ | ⊥ | ⊤ ‖  ⊥  |  ⊤  |  ⊤    	           ⊤
 ⊤ | ⊥ | ⊥ ‖  ⊥  |  ⊤  |  ⊥    	           ⊤
 ⊥ | ⊤ | ⊤ ‖  ⊤  |  ⊤  |  ⊤  ✔	           ⊤
 ⊥ | ⊤ | ⊥ ‖  ⊤  |  ⊥  |  ⊤    	           ⊤
 ⊥ | ⊥ | ⊤ ‖  ⊤  |  ⊤  |  ⊤  ✔	           ⊤
 ⊥ | ⊥ | ⊥ ‖  ⊤  |  ⊤  |  ⊤  ✔	           ⊤

rule of inference

邏輯學家已經發明許多推論規則。以下介紹其中三個：

一、肯定前件modus ponens：

p
p → q
⎯⎯⎯⎯⎯
q

二、否定後件modus tollens：

p → q
¬q
⎯⎯⎯⎯⎯
¬p

三、歸謬法reductio ad absurdum：

p → q
p → ¬q
⎯⎯⎯⎯⎯⎯
¬p

延伸閱讀：adequacy

邏輯運算¬、∧、∨是充分的，足以製造全部的真假組合。

註：此處只談「充分的」，沒有談「必要的、最少的」。

 p | q ‖  ⊤  | p∨q | p∨¬q|  p  |       |¬p∧¬q|  ⊥  |
---|---‖-----|-----|-----|-----|- ... -|-----|-----|
 ⊤ | ⊤ ‖  ⊤  |  ⊤  |  ⊤  |  ⊤  |       |  ⊥  |  ⊥  |
 ⊤ | ⊥ ‖  ⊤  |  ⊤  |  ⊤  |  ⊤  |       |  ⊥  |  ⊥  |
 ⊥ | ⊤ ‖  ⊤  |  ⊤  |  ⊥  |  ⊥  |       |  ⊥  |  ⊥  |
 ⊥ | ⊥ ‖  ⊤  |  ⊥  |  ⊤  |  ⊥  |       |  ⊤  |  ⊥  |

2 values.                       (⊤ and ⊥)
N = 2 variables.                (p and q)
2^N = 4 inputs.                 (⊤⊤/⊤⊥/⊥⊤/⊥⊥)
2^2^N = 16 different functions. (⊤⊤⊤⊤/⊤⊤⊤⊥/⊤⊤⊥⊤/...)

邏輯運算→、↔是多餘的，用於簡潔呈現邏輯推論和邏輯等價的複合命題。 符號外觀源自後面章節提到的衍生。

logical equivalence: p ≡ q
tautology:           p ↔ q ≡ ⊤

logical inference: p₁ , p₂ , ... , pₙ ⊨ q
tautology:         p₁ ∧ p₂ ∧ ... ∧ pₙ → q ≡ ⊤

其實→、↔可以全面換成¬、∧、∨。

p→q ≡ ¬p∨q
p↔q ≡ (p∧q)∨(¬p∧¬q)

inference

方才使用真值表。現在使用規則表。

邏輯命題習慣用A、B、C。

直式     	半直半橫   	橫式
A        	A , B      	A , B ⊢ A ∧ B
B        	⎯⎯⎯⎯⎯
⎯⎯⎯⎯⎯    	A ∧ B
A ∧ B

特殊等號⊢稱作「可衍生derivability」。

rule of inference

邏輯學家已經發明一套推論規則：

introduction:
                                          [A]         [A]     
                                           ⋮           ⋮      
A , B          A             B             B           ⊥      
⎯⎯⎯⎯⎯ (∧I)   ⎯⎯⎯⎯⎯ (∨I₁)   ⎯⎯⎯⎯⎯ (∨I₂)   ⎯⎯⎯⎯⎯ (→I)   ⎯⎯⎯ (¬I)
A ∧ B        A ∨ B         A ∨ B         A → B        ¬A     

elimination:
                                   [A] [B]    
                                    ⋮   ⋮     
A ∧ B         A ∧ B         A ∨ B , C , C    
⎯⎯⎯⎯⎯ (∧E₁)   ⎯⎯⎯⎯⎯ (∧E₂)   ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ (∨E)
  A             B                 C           

A , A → B        A , ¬A     
⎯⎯⎯⎯⎯⎯⎯⎯⎯ (→E)   ⎯⎯⎯⎯⎯⎯ (¬E)
    B              ⊥       

other:
                     [¬A]      
                       ⋮       
¬¬A         ⊥          ⊥       
⎯⎯⎯ (¬¬)   ⎯⎯⎯ (⊥)   ⎯⎯⎯⎯ (RA)
 A          A          A       
雙重否定定律 爆炸      歸謬法

註：此處的⊥不是先前章節的假false。
　　此處的⊥不是先前章節的恆假句contradiction。
　　此處的⊥是一種特殊的命題。
　　此處的⊥稱作bottom。bottom是⊥這個符號的原始名稱。
　　有些邏輯學家將此處的⊥定義成A ∧ ¬A，呼應恆假句。

註：順便介紹其他符號的原始名稱。
　　⊤ top / down tack  頂／朝下圖釘
　　⊥ bottom / up tack 底／朝上圖釘
　　⊢ turnstile        驗票閘門
　　⊨ double turnstile 雙重驗票閘門

derivation

利用規則表，前提一路變成結論。

套用規則稱作「衍生derivation、演繹deduction」。

例如且運算交換律「A ∧ B ⊢ B ∧ A」的衍生過程：

樹狀風格                            列表風格
derivation tree:                   derivation list:

A ∧ B         A ∧ B                1 │ A ∧ B
⎯⎯⎯⎯⎯ (∧E₂)   ⎯⎯⎯⎯⎯ (∧E₁)            ├───────
  B             A                  2 │ B        from 1 (∧E₂)
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ (∧I)     3 │ A        from 1 (∧E₁)
          B ∧ A                    4 │ B ∧ A    from 2 3 (∧I)

axiom

各種命題A、B、C、……都可以假設數值是真，作為最初的前提，作為衍生的起點。

現在改成只有部分敘述可以假設數值是真，作為最初的前提，作為衍生的起點。這些敘述稱作「公理axioms」。

deductive system：演繹系統。衍生起點可以是任意命題。
axiomatic system：公理系統。衍生起點只能是指定敘述。

知名的公理系統：

Gentzen system：一個公理，多個規則。我不打算深入介紹。
Hilbert system：三個公理，一個規則。我不打算深入介紹。

equivalence

方才使用真值表。現在使用規則表。

實施兩次邏輯推論：左式衍生右式，右式衍生左式。如果兩者皆可衍生，那麼兩者等價。

¬(A ∨ B) ⟛ (¬A ∧ ¬B)

特殊等號⟛稱作「互相可衍生interderivability」。

proof【名稱尚待確認】

邏輯推論本身作為邏輯敘述，拿來進行邏輯推論。

如此一來，就能調整前提結論。

A ⊢ C
B ⊢ C
⎯⎯⎯⎯⎯⎯⎯⎯⎯
A , B ⊢ C

邏輯學家已經發明許多推論規則。以下介紹其中三個：

（Γ Σ Δ Π各是一連串敘述。敘述數量可以是零個。）

introduction:

Γ, A ⊢ Δ             Γ ⊢ Δ, A         
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ (∨L₁)   ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ (∨R₁)
Γ, A ∨ B ⊢ Δ         Γ ⊢ Δ, A ∨ B    

elimination:

Γ, A ⊢ Δ         
Σ, B ⊢ Π, A      
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ (cut)   原理其實就是q→r, p→q ⊢ p→r，前提對調順序。
Γ, B ⊢ Δ, Π      

other:

         
⎯⎯⎯⎯⎯ (I)   同一律
A ⊢ A    

恆真句／公理可以寫成推論規則的模樣：前提是空集合，結論是恆真句／公理。

⊨ ¬(p ∧ ¬p)   tautology
⊢ ¬(A ∧ ¬A)   axiom

intuitionistic logic / classical logic

直覺主義邏輯：自訂規則。

經典邏輯：符合下述六種規則。也符合五種運算的真值表。

排中律　　　　law of excluded middle       ⊢ (A ∨ ¬A)
無矛盾律　　　law of noncontradiction      ⊢ ¬(A ∧ ¬A)
追加無謂前提　monotonicity of entailment   (A ⊢ B) ⊢ (A , X ⊢ B)
消滅重複前提　idempotency of entailment    (A , A ⊢ B) ⊢ (A ⊢ B)
且運算交換律　commutativity of conjunction (A ∧ B) ⊢ (B ∧ A)
笛摩根對偶　　De Morgan duality            ¬(A ∨ B) ⊢ (¬A ∧ ¬B)

順帶一提，邏輯學家依據上述六種規則，創造五種邏輯運算的真值表。綜觀歷史，先有規則表，才有真值表。

好久好久以前，邏輯學只有規則表。邏輯推論過程冗長，令人望而生畏。直到真值表橫空出世，邏輯學搖身一變宛如數學。自此邏輯學就變得平易近人了。

consequence

邏輯結果宛如數學因此therefore。

  | name                  | English | Chinese
--| ----------------------| --------| ----------
⊨ | semantic consequence  | entail  | 導致、蘊涵 :-(
⊢ | syntactic consequence | derive  | 衍生、推導

註：邏輯學採用⊨。數學沒有對應符號。
　　數學不討論此概念。
註：邏輯學採用⊢。數學採用∵和∴配對。
　　數學當中，⊢是伴隨函子。

邏輯推論有兩種手法：真值表（解釋）、規則表（衍生）。

真值表固定不變（源自標準規則表）。規則表可以自訂。

採用標準規則表，那麼兩種手法相同。

自訂規則、自訂公理，那麼兩種手法不相同。

許多學問經常自訂規則、自訂公理。例如數學、社會學。

valid / derivable

valid:     a inference is true by intepretation
derivable: a inference is true by derivation

valid:     Γ ⊨ Δ
derivable: Γ ⊢ Δ

valid but not derivable
https://math.stackexchange.com/questions/3987061/

形容詞valid、名詞validity。

有效的：根據真值表，若前提皆⊤，則結論是⊤。

當所有前提皆假設為⊤，則這個結論有唯一解⊤。

形容詞derivable、名詞derivability。

可衍生的：根據規則表，若前提皆⊤，則結論是⊤。

當所有前提皆假設為⊤，則可以衍生這個結論。

sound / complete

sound:    all derivable inferences are valid
complete: all valid inferences are derivable

sound:    (Γ ⊢ Δ) → (Γ ⊨ Δ)
complete: (Γ ⊨ Δ) → (Γ ⊢ Δ)

complete but not sound
https://math.stackexchange.com/questions/441025/

形容詞sound、名詞soundness。

可靠的：可衍生的邏輯推論都是有效的。

這套前提衍生的所有結論，皆有唯一解⊤。

前提很合理，結論皆實話。所到之處，皆為實話。宛如洪水。

形容詞complete、名詞completeness。

完備的：有效的邏輯推論都是可衍生的。

凡有唯一解⊤，必是這套前提衍生的結論。

前提很充足，道盡一切實話。所有實話，皆可觸及。宛如連通。

satisfiable / consistent

形容詞satisfiable、名詞satisfiability。

可滿足的：存在一種interpretation，使得敘述是⊤。

這個敘述不是恆假句。

形容詞consistent、名詞consistency。

一致的：存在一種interpretation，使得結論皆⊤。

這個演繹系統／公理系統，所有結論∧起來，不是恆假句。

soundness implies consistency

  sound ∧ conjunction of all premisses is not a contradiction
→ conjunction of all conclusions is not a contradiction (consistency)

soundness implies consistency
https://cs.stackexchange.com/questions/88274/

可靠的：可衍生的邏輯推論都是有效的。

有效的：若不是爆炸（若前提不是恆假句），那麼存在一種interpretation，當前提皆真，則結論皆真。

換句話說，可靠的情況下，若前提不是恆假句，則一致。

logical reasoning

邏輯推理。找到前提結論，製造邏輯推論。

邏輯學家考慮下述三種手法：

deductive reasoning：演繹。找到結論。
abductive reasoning：溯因。找到前提。
inductive reasoning：歸納。找到規則。

演繹當中，最經典的手法是「自然演繹natural deduction」：自訂前提，套用規則，不斷衍生，找到結論。先前章節已經介紹了。

statistical reasoning

統計推理。針對某些現象，進行取樣，將發生機率最高的事件聯繫配對在一起。簡單來說就是英國研究。

例如交通肇事者當中有70%擁有吃早餐的習慣。兩者關聯之後：吃早餐極可能導致車禍。

例如有錢屬於好事、照顧老弱婦孺屬於好事、為民服務是好事。這些關聯之後：地方首長發放敬老津貼、生育補助，地方首長是在做好事。

人類經常採用關聯，很少採用衍生。大部分人類的知識架構皆源自統計推理，而非邏輯推理。統計推理符合人類習性，自然而然就會適應。邏輯推理違反人類直覺，實施教育才能習得。

predicate

邏輯謂詞宛如數學集合。

借鑑集合論，發明新變數：P(x)、P(x,y)。

一元版本P(x)：x是正整數、x屬於S集合、……。

二元版本P(x,y)：x包含y、x大於y、x等於y、……。

P(x)與P(x,y)，寫作函數，當作變數，實為集合。

援引集合的概念，稍微符合真實世界常見情況。

     | name        | English     | Chinese
-----| ------------| ------------| ------------
P(x) | predicate   | predicate   | 謂詞

connective

邏輯連詞宛如數學運算。

借鑑集合論，推廣舊運算：¬、∧、∨、→、↔。

舊運算全面改成集合運算，但是沿用舊符號。

logical operator | set operator
-----------------| --------------
¬ negation       | ‾ complement
∧ conjunction    | ∩ intersection
∨ disjunction    | ∪ union
                 | \ subtraction
→ implication    | ⊃ inclusion
↔ bi-implication | = equivalence

compound predicate

複合謂詞宛如數學算式。

(P(x) → Q(x)) ∨ (P(x) ∧ ¬Q(x))

quantifier

邏輯量詞宛如數學性質符號。

借鑑集合論，發明新運算：∀、∃。

將複合謂詞變成邏輯命題。

  | name                       | English      | Chinese
--| ---------------------------| -------------| -------
∀ | universal quantification   | for all      | 所有
  |                            | given any    | 任意
∃ | existential quantification | for some     | 某些
  |                            | there exists | 存在

proposition

複合謂詞變成邏輯命題，需要使用量詞。

一元謂詞需要一個量詞，二元謂詞需要兩個量詞。

∀xP(x)
∃x∀yP(x,y)

多元複合謂詞需要多個量詞。

∀x((P(x) → Q(x)) ∨ (P(x) ∧ ¬Q(x)))
∀x∀y(P(x) ∧ Q(y) ∧ R(y) ∧ S(x,y))

數值只有兩種：⊤、⊥。

∀xP(x) = ⊤
∀x∃yP(x,y) = ⊥
∀x(P(x) → Q(x)) ∨ (P(x) ∧ ¬Q(x)) = ⊥
∀x∀y(P(x) → Q(y) ∨ R(y)) = ⊥

compound proposition

複合謂詞變成邏輯命題之後，得以使用舊運算。

由於運算符號一模一樣的緣故，需要仔細解讀。

¬∀xP(x) → ∃x(¬P(x) → Q(x))

P(x) and Q(x) are predicates
¬P(x) → Q(x) is a compound predicate
∀xP(x) and ∃x(¬P(x) → Q(x)) are propositions
¬∀xP(x) → ∃x(¬P(x) → Q(x)) is a compound proposition

rule of replacement

命題運算¬改成謂詞運算¬。

¬∃xP(x) ≡ ∀x¬P(x)
¬∀xP(x) ≡ ∃x¬P(x)

這是錯誤範例。等號右側量詞短缺，文法錯誤。

∀x∀yP(x,y) ≡ ∀xP(x,y) ∧ ∀yP(x,y)

propositional logic / predicate logic

命題邏輯（零階邏輯）：變數是一個數值。運算一共五種。

謂詞邏輯（一階邏輯）：變數是一個集合。追加兩種運算。

可以推廣成更高階，但是沒有太大意義。