命題邏輯系統
命題邏輯系統有很多種，比如公理化系統、自然推理系統、sequent系統等。
一些基礎
聯結詞
命題推理系統包括聯結詞和命題。
聯結詞：並非、並且、或者、如果那么、當且僅當。分別用符號﹁、∧、∨、→、↔表示。
- 其中
﹁和→是基本聯結詞，∧、∨、↔都用它們來定義。
命題：也用字母符號表示。
利用這些符號我們可以構造復雜的命題，
- 比如p→q，表示如果p那么q，p∧﹁q，表示p並且﹁q。
- 比如：(p↔q)∨(p→(q→(﹁p∧r)))。
聯結詞完全集
可以把聯結詞看作是一個函數，比如∧是一個二元函數，∧(0,0)=0，∧(0,1)=1，∧(1,0)=1，∧(1,1)=1。
可以證明任何真值函數都可以用{﹁，∧}、{﹁，∨}、{﹁，→}的任一種表示。
舉例說明第一種情況：
f(0)=0，f(1)=1。則f(x)= x
f(0)=0，f(1)=0。則f(p)=x∧﹁x
f(0,0)=0，f(0,1)=0，f(1,0)=1，f(1,1)=1，則f(x,y)=﹁(﹁(x∧﹁y)∧﹁(﹁x∧y))
實際上我們可以定義一個聯結詞↓，使得它能表示所有真值函數。它是這樣定義的：↓(0,0)=1，↓(0,1)=0，↓(1,0)=0，↓(1,1)=0。可以證明它能表示所有函數。
定理和推理
定理：通過公理和推理規則證明的任何一個命題都是定理。任何公理都是定理。
定理的符號：記作⊢A，表示A是定理，亦即A是無條件成立的。
⊢表明一個公式是永真式，定理肯定是永真。
需要推理的定理：如果一個命題還需要其他前提才能證明得到，則記作A⊢B，表示A是前提，B是結論。
演繹定理
如果Γ,A ⊢B ，那么Γ⊢A→B。
- 這里Γ是命題集（可以是空集），A和B是任意命題。如果某個命題集Γ和命題A推出B，則從Γ可推出A→B。這個定理的證明從略。
命題邏輯的可靠性和完全性定理
前面介紹了命題邏輯系統，我們可以用它進行推理。
現在的問題是，它的推理都是有效的嗎？或者說，當前提為真時，它推理得到的結論都是真的嗎？
另一個問題是，用它能得到所有的有效推理嗎？
第一個問題叫可靠性問題：從Γ⊢A，能否得到Γ⊨A？
第二個叫完全性問題：從Γ⊨A，能否得到Γ⊢A？
上面的Γ表示命題集（可以是空集），Γ⊢A，表示從Γ推出A，Γ⊨A表示如果Γ中的每個命題都真，則A真。
(1)可靠性定理
可靠性定理的證明比較簡單。可以檢驗，三條公理都是永真的。即不管原子命題取什么值，它們都取真值。而推理規則是保真的：當p和p→q都為真時，q一定為真。從Γ推出A的過程中，只能使用Γ、邏輯公理和推理規則。所以如果Γ是真的，則推理得到的任何結果都是真的。所以可靠性定理成立。
(2)完全性定理
這里只討論證明思路。
要證：如果Γ⊨ A，那么Γ⊢A。所以要證：如果並非Γ⊢A，那么並非Γ⊨ A。
即要證：並非Γ⊢A，那么Γ和﹁A可以同時為真。
只需證明下面兩點：
1、如果並非Γ⊢A，則Γ∪﹁A是一致集
2、任何一致集都有模型
一致集和模型的定義。Γ是一致集，當且僅當，存在一個公式R，並非Γ⊢R。一個命題或一個命題集合有模型是指，存在一個賦值使得它們為真。
先證明1。
如果Γ∪﹁A不是一致集，則Γ，﹁A ⊢ A。根據演繹定理，有Γ⊢﹁A→A。又因為 (﹁A→A)→A是定理。所以Γ⊢A，與前提相矛盾。
再證明2。
先將一致集擴展成極大一致集，然后給極大一致集找到一個模型。
極大一致集的定義：某個一致集S，對任意的公式A，A或者﹁A恰有一個屬於S，則集合S是極大一致集。
現在將任意的一致集T0擴展成極大一致集。
所有的命題組成的集合是可數的，將它們排列，A1、A2、A3、……An、……。如果Tn ⊢An，則Tn+1=Tn∪{An}，如果並非Tn ⊢An，則Tn+1=Tn∪{﹁An}。令T = ∪Tn，即所有擴充集的並。可證明T是極大一致集。
給T中的每個原子命題賦真值，不在T中的原子命題賦假值。可以通過歸納法證明，這個賦值下，任意一個公式為真當且僅當它屬於T。所以這個賦值是T的模型。
1 命題邏輯的公理系統
這里討論的是公理化系統。它就像我們以前學過的幾何證明一樣，從幾條公理出發，通過推理得到結論。
【我的問題】公理系統僅出現基本聯結詞嗎??不是吧？
(1)初始符號
大寫英文字母
A,...Z表示命題
¬,∨表示聯結詞
(,)一對括號規定了聯結詞運算的優先順序
⊢表明一個公式是永真式
(2)形成規則
稱初始符號構成的符號序列為公式，只有符合以下條件的符號序列是合式公式：
- 單個符號π，π是大寫英文字母
- 若A為合式公式，¬A是合式公式
- 若A,B為合式公式，(A∨B)是合式公式
為簡化其他合式公式的表達，引入如下所示的公式：
p∧q := ﹁(p→﹁q) 或 p∧q := ﹁(﹁p∨﹁q)
p∨q := ﹁p→q 或 p→q := ﹁p∨q
p↔q := (p→q)∧(q→p)
就是說，左邊的命題可以用右邊的命題是等價的。只有聯結詞﹁和→是基本的，∧、∨、↔都用它們來定義。
(3)公理
1、p→(q→p)
2、(p→(q→r))→((p→q)→(p→r))
3、(﹁p→﹁q)→( q→p)
在公理系統中引入如下公理：
⊢(p∨p→p)
⊢(p→p∨q)
⊢(p∨q→q∨p)
⊢((q→r)→((p∨q)→(p∨r)))
(4)推理規則
代入規則、分離規則、置換規則是命題邏輯公理系統中的推理規則
分離規則：
從p和p→q，推出q
- 上面的公理和推理規則中的p、q、r可以代表任何命題。比如r→(s→r)也是公理，它只是把p換成了r，q換成了s。(p∨q)→((r∧s)→(p∨q))也是公理，它把p換成了p∨q，q換成了r∧s。
- 上面的公理中，
僅出現﹁和→，沒有出現∧、∨、↔。
2 命題邏輯的自然推理系統
(1)初始符號
命題邏輯的自然演繹系統的一部分初始符號繼承自命題邏輯的公理系統。此外，命題邏輯的自然演繹系統還包含如下初始符號：
Γ ={A1,…,An}=A1,…,An
表示有限個命題公式集合，定義Γ⊢A表示Γ,A之間有形式推理關系，Γ為形式前提，A為形式結論。
(2)形成規則
命題邏輯的自然演繹系統的形成規則與命題邏輯的公理系統的形成規則相同
(4)定理？公理
命題邏輯的自然演繹系統包含的定理與命題邏輯的公理系統包含的定理相同
(3)變形規則
命題邏輯的自然演繹系統有如下變形規則：
A1,…,An⊢Ai(i=1…,n) ，即前提中的任何命題都可以作為結論出現
傳遞律：若Γ⊢A且A⊢B，則Γ⊢B
反證律：若Γ,¬A⊢B且Γ,¬A⊢¬B，則Γ⊢A（等價於證明Γ∧¬A=F）
分離規則：A,A→B⊢B
蘊含詞引入：若Γ,A⊢B，則Γ⊢A→B
3 非標准邏輯
邏輯符號
(1)Γ，⊢，⊨
Γ是命題集（可以是空集）
⊢表示可推出。
- 自然演繹系統中，A ⊢ B 和 ⊢ A→B 等價。
⊢ is an assertion. It IS NOT necessarily correct and a specific deduction model must be given to make this assertion.
E.g. Sequent A, B ⊢ C, D means that under current deduction model, if both A and B are true, then either C or D is true. This assertion may be correct.
And under natural deduction(自然演繹系統), A ⊢ B and ⊢ A→B are the same.
例子：
如果Γ,A ⊢B ，那么Γ⊢A→B。
- 這里Γ是命題集（可以是空集），A和B是任意命題。如果某個命題集Γ和命題A推出B，則從Γ可推出A→B。這個定理的證明從略。
⊨也表示推出，但更強。
- A⊨B，表示A中所有元素均為真時，B成立。
⊨ is a semantic entailment symbol used to check the relationship among certain variables under every logic model. It’s more like a universal version of ⊢, and it IS NOT necessarily correct as well.
E.g. I’ve just had my meal ⊨ Something just traveled to my stomach through my throat
This semantic entailment isn’t necessarily correct, for there might be some creature using other holes for eating instead of the one we called mouth.
(2):=
:=表示定義為
謂詞邏輯
謂詞邏輯，就是加了"量詞運用規則"的命題邏輯。
命題邏輯可以看作是零階邏輯，謂詞邏輯就是一階邏輯。
一階謂詞邏輯是命題邏輯的推廣，二階謂詞邏輯是一階謂詞邏輯的推廣。
命題邏輯的可滿足性問題是NP-Complete的,一階謂詞邏輯的可滿足性問題不可判定的.
自由變量 （謂詞公式中的自由變量）
術語
argument（論證）
論證(argument)：句子的集合體。
- 講道理的
過程和結果用一個更准確的術語來表示。結果就是道理，即即你說出的一系列句子。 - 由n(n>2)個句子順序構成的論證，前n-1個句子稱作【前提】(premise)，第n個句子稱作【結論】（conclusion）。
有效論證(valid argument):
- 論證的有效性由兩個因素：論證的句法結構，命題真值
論證模式(argument schema)：
- 是論證的一般性公式，抽離了具體命題的內容，只留下了命題真值和句法結構。
- 論證模式和論證，就像算術和代數，前者研究具體計算，后者研究運算規律。
- 論證是展示講道理的具體案例，論證模式展示講道理的一般規律。
參考:
https://site.douban.com/145723/room/3729001/ 【豆瓣邏輯小站，很棒的邏輯學網站】
https://blog.csdn.net/smilejiasmile/article/details/106719257
https://huangfusl.github.io/math/discrete-mathematics/chapter-3/#_16 【命題邏輯系統，總結的也不錯】
https://blog.sciencenet.cn/blog-1255140-1033426.html 【over，命題邏輯系統——邏輯學筆記8】
https://blog.sciencenet.cn/blog-1255140-1033465.html 【未整理，命題邏輯的可靠性和完全性定理——邏輯學筆記9】
http://wangyanjing.com/wp-content/uploads/2019/08/PublicDeltaLogicfinal.pdf 【哲學、數學、計算機中的邏輯學】
https://blog.csdn.net/weixin_43929519/article/details/86012324 【difference between →, ⊢ and ⊨】