數理邏輯＝﹥ ，|－這兩個符號有什麼區別？

11-26

我覺得這兩個符號完全重複了。怎麼理解它們的區別？？

-
謝邀。

我在數理邏輯系統中沒有使用過 $Rightarrow$ ，僅在數學證明中使用過。這個符號不是一個標準命題形式語言中的符號。而是一個日常語言中的符號，它的意義是模糊的。

在命題邏輯中，有三個有推出含義的符號容易混淆：

語義後承（semantic consequence），符號是 $models$ （models）。語義後承在一般情況下是連接一個命題集合和一個命題。如果，在任何一種語義賦值下，只要命題集合 $Sigma$ 中的每一個命題都為真，那麼 $phi$ 就一定為真，那麼，我們就說 $phi$ 是 $Sigma$ 的語義後承，記作 $Sigmamodels phi$ 。
句法後承（syntactic consequence），符號是 $vdash$ （vdash）。句法後承的用法和語義後承類似，也是連接一個命題集合和一個命題，如 $Sigma vdashphi$ ，表示的是 $phi$ 可以通過句法證明的方式從命題集 $Sigma$ 中得出。即，存在一個證明，使得每個前提要麼是公理，要麼是 $Sigma$ 中的命題，而證明的結論是 $phi$ 。具體來說，一個證明是一個命題序列，其中每個命題要麼是公理，要麼是前提，要麼是由前面的命題通過證明規則得到的。其中最後一個稱為結論。
實質蘊含（material implication / material conditional），符號是 $ightarrow$ （
ightarrow）。實質蘊含是一個命題邏輯中的二元運算元，連接的是兩個命題。在句法系統中，由 Hilbert 的前兩條公理完全刻畫，由第三條公理刻畫它和否定的關係。[1] 在語義系統中，我們說 $Sigmamodels p ightarrow q$ 當且僅當 $Sigmamodels q$ 或者 $Sigmamodels eg p$ 。就是說，如果一個實質蘊含條件句成立，就是說，前件（上面的 p）為真的情況下，後件（上面的 q）不可能為假。[2]

除此之外沒有別的常用的，並且經過形式定義的符號。至於 $Rightarrow$ ，其實就是單純表示推出，這種推出是沒有嚴格定義的，一般情況下在簡單的數學系統中，由於系統的強完全性和強可靠性[3]，句法後承和語義後承等價，那麼這時推出就同時都是兩種推出。但是，據我看到 wiki 中的說法，
$Rightarrow$ 只表示邏輯後承，但是沒有具體區分是語義後承還是句法後承，所以對於完全性和可靠性不成立的系統，這個符號就是模糊的。

當然，前面的語義後承和句法後承也不是數理邏輯系統中的符號，這是元語言符號。並且，在句法系統中不談論真假，在語義系統中不談論證明。

當然，在不同的符號系統中，邏輯學家可能會採用 $supset$ 來替代 $ightarrow$ （實質蘊涵），用 $cup$ 替代 $vee$ （或者），用 $cap$ 替代 $wedge$ （且），用 $sim$ 替代 $eg$ （非，否定）。但是我不太清楚到底哪些人是用 $Rightarrow$ 來表示什麼。

[1]
Hilbert 的公理系統可以寫作三個公理模式加一個規則：
$(mathcal{A} ightarrow(mathcal{B} ightarrowmathcal{A}))$
$((mathcal{A} ightarrow(mathcal{B} ightarrow mathcal{C})) ightarrow((mathcal{A} ightarrow mathcal{B}) ightarrow(mathcal{A} ightarrowmathcal{C})))$
$((( egmathcal{A}) ightarrow( egmathcal{B})) ightarrow(mathcal{B} ightarrowmathcal{A}))$
為什麼說是公理模式呢？因為這裡的 $mathcal{A}$ 、 $mathcal{B}$ 、 $mathcal{C}$ 都是元語言中用來代表合式公式的符號。換而言之，這個系統中有無窮多條公理。
至於推理規則，就只有一個 MP 規則： $phi,phi ightarrowpsivdashpsi$ ，中間的 $vdash$ 表示證明系統中的推出，並且，這裡的 $phi$ 和 $psi$ 也都是元語言中代表合式公式的符號。

這種情況下，如果我們要證明 $emptysetvdash p ightarrow p$ （從空集出發能夠推出，即表示在系統內可證），那麼我們要寫出如下命題序列：

$p ightarrow((p ightarrow p) ightarrow p)$ （公理 1）
$( p ightarrow( (p ightarrow p) ightarrow p )) ightarrow ((p ightarrow (p ightarrow p)) ightarrow(p ightarrow p))$ （公理 2）
$((p ightarrow (p ightarrow p)) ightarrow(p ightarrow p))$ （1、2，MP 規則）
$p ightarrow (p ightarrow p)$ （公理 1）
$p ightarrow p$ （4、3，MP 規則）

[2] 但是在語義系統中，如果我們要說明 $emptysetmodels p ightarrow p$ （即，是空集的語義後承，或者說，是永真的）。那麼我們只需要說明，由於在 p 為真和 p 為假的情況下，根據實質蘊含運算元的語義規則， $Sigmamodels p ightarrow q$ 當且僅當 $Sigmamodels q$ 或者 $Sigmamodels eg p$ ，我們都能得到 $p ightarrow p$ 為真。因此，我們會說這個公式是空集的語義後承。

[3] 強完全性：對於任意的公式集合 $Sigma$ ，對於任意的公式 $phi$ ，如果 $Sigmamodels phi$ ，那麼 $Sigma vdashphi$ 。強可靠性：
對於任意的公式集合 $Sigma$ ，對於任意的公式 $phi$ ，如果 $Sigma vdashphi$ ，那麼 $Sigmamodels phi$ 。而弱完全性是，方式為真的公式都是可證的；弱可靠性是，凡是可證的公式都是為真的。在有完全性和可靠性的基礎上，沒有必要在實際運用中區分兩種推出。
-

感謝@羅心澄關於那幾個符號的對比。補充一下，「語義後承」的後面是可以接一個命題集合的。只要後面集合中一個命題被滿足就行。

下面我說下「=&>」的意義。在數理邏輯中，它定義了Sequence這個概念，比如 $Gamma Rightarrow Delta$ 就是一個Sequence，其中前後都是有限命題集合。不過它表示一個推理過程，這個過程可能是真，可能是假，要驗證一個Sequence的真偽就要用Sequence Calculus進行推導，直到推出的每一個原子命題都為真。具體的推到規則在 https://logic.rwth-aachen.de/files/MaLo-SS14/script.pdf 中的第一章（命題邏輯）和第四章（謂詞邏輯），當然謂詞邏輯的推導過程要複雜一些。

另外需要注意的是，這是一個語義上的推倒，只不過在謂詞邏輯和命題邏輯中，語義和語法是等價的（在我發的課件中Satz 4.6中描述的完整性）。相應的，要驗證一個Sequence Calculus的正確性，只能通過找對應的Interpretation。

還有一個需要強調的是在謂詞邏輯上因為 $forall$ 和 $exists$ 可能存在多中推倒可能，所以只要有一個推導出的全是原子Sequence，那麼這個Sequence就是正確的。

最後總結一下， $models$ 是語義上的滿足（一定正確的）， $vdash$ 是語法上的滿足（正確的）， $Rightarrow$ 只是一個推導過程，正確性需要驗證。

|— 只代表表示推理過程 {p,q,...}|—s 。
並沒有表明這個推理是正確的。
而=&>代表{p,q,...}|—s 這個式子是一個重言式。
表示推理過程是正確的，有效的。所以兩者是有區別的。
=&>與|=等價。

我在數理邏輯系統中沒有使用過 $Rightarrow$ ，僅在數學證明中使用過。這個符號不是一個標準命題形式語言中的符號。而是一個日常語言中的符號，它的意義是模糊的。

$Rightarrow$ 這個符號表示蘊涵。在元語言中使用。

$vdash$ 這個符號表示語形後承。

有兩個世界，一個是語義世界，一個是語形世界。

前者是語義世界的推倒，後者是語形世界的推導。

舉例：將語義世界理解為我們所生活的現實世界，語形世界則可以是一門描述這個現實世界的語言，例如英語，它是一個由字母和語法規則構成的形式系統，兩者在個體上的對應體現為現實的蘋果和單詞「Apple」。

一些重要的定理正是證明這兩個世界的對應性，例如，按照英語的字母和語法規則推出單詞Dog，則現實世界能夠推出有一個實物與其對應，這應該是完全性（記不清楚了）。