日韩成人中文在线视频,中文字幕AV电影

寫(xiě)在前面：最近把科普書(shū)《哥德?tīng)柊Ｉ釥柊秃铡愯抵蟪伞返牟糠钟腥ぶR(shí)整理成了閱讀筆記。
個(gè)人非常推薦這本書(shū)，這是一本讀來(lái)令人驚艷的好書(shū)，它以精心設(shè)計(jì)的巧妙筆法深入淺出地介紹了數(shù)理邏輯、可計(jì)算理論、人工智能、復(fù)雜系統(tǒng)等學(xué)科領(lǐng)域中的許多有趣理論以及它們背后的聯(lián)系。這本書(shū)的價(jià)值不在于它科普知識(shí)的深度，而在于它的美，相信這本書(shū)也會(huì)讓你對(duì)很多東西重拾興趣。
優(yōu)秀的科普書(shū)就是這樣，能激發(fā)人繼續(xù)學(xué)習(xí)和探索的興趣。

集異璧

本篇筆記涉及的內(nèi)容是GEB的前兩個(gè)章節(jié)，討論的是關(guān)于形式系統(tǒng)及其意義。形式系統(tǒng)的一些基礎(chǔ)知識(shí)放到了文章的最后，大多數(shù)內(nèi)容只要有一點(diǎn)數(shù)理邏輯的基礎(chǔ)就能理解。

形式系統(tǒng)WJU

GEB的開(kāi)篇中探討了這樣一個(gè)有趣的問(wèn)題，給定一個(gè)形式系統(tǒng)中的命題公式，判定該命題公式是否是形式系統(tǒng)中的定理。
在數(shù)理邏輯中，如果一個(gè)命題公式是形式系統(tǒng)的定理，那么這個(gè)定理是可以被該形式系統(tǒng)證明的，也就是根據(jù)系統(tǒng)的公理和規(guī)則能通過(guò)有限步的構(gòu)造，得到這個(gè)定理的符號(hào)表達(dá)式。特別要注意有限步的限制。因?yàn)槿绻硞€(gè)定理的證明需要無(wú)限步驟這本身就沒(méi)有意義。
那么現(xiàn)在考慮這樣一個(gè)問(wèn)題，能否單靠系統(tǒng)本身的公理和推理規(guī)則在有限步驟內(nèi)判定一個(gè)命題公式是定理還是非定理呢？
GEB書(shū)中給出了這樣一個(gè)有趣的形式系統(tǒng)：
形式系統(tǒng)WJU

該符號(hào)系統(tǒng)是由 $W，J，U$ 所組成的字符串
初始串是 $WJ$ (相當(dāng)于該系統(tǒng)的一條公理)
系統(tǒng)規(guī)則：
1 如果串的最后一個(gè)符號(hào)是 $J$ ，則可以加上一個(gè) $U$
即：如果 $xJ$ 是定理，那么 $xJU$ 也是定理。
2 如果串是 $Wx$ 形式，則可以再加上 $x$ 生成 $Wxx$ ， $x$ 代表任意由 $W，J，U$ 組成的串
即：如果 $Wx$ 是定理，那么 $Wxx$ 也是定理
3 如果一個(gè)串中出現(xiàn) $JJJ$ ，則可以用 $U$ 代替 $JJJ$ 得到新串
即：如果 $xJJJy$ 是定理，那么 $xUy$ 也是定理
4 如果串中出現(xiàn) $UU$ ，則可以將 $UU$ 刪掉得到新串
即：如果 $xUUy$ 是定理，那么 $xy$ 也是定理

問(wèn)題： $WU$ 是否是系統(tǒng)中的串？( $WU$ 是否是該系統(tǒng)中的定理)
我們當(dāng)然可以自己按規(guī)則推理出這個(gè)形式系統(tǒng)具有的一些定理，甚至發(fā)現(xiàn)這個(gè)系統(tǒng)產(chǎn)生的串的一些固定模式(比如系統(tǒng)中的串一定是 $W$ 開(kāi)頭的)，而且推導(dǎo)一會(huì)兒你就會(huì)發(fā)現(xiàn)， $WU$ 應(yīng)該不會(huì)出現(xiàn)在該系統(tǒng)中了，不妨稱(chēng)為直覺(jué)。但是為什么會(huì)這樣我們還是沒(méi)法說(shuō)的透徹。另外從形式系統(tǒng)的角度看，由公理和推理規(guī)則，我們很容易構(gòu)造定理樹(shù)(定理推理序列樹(shù))：

WJU定理樹(shù)

其中父節(jié)點(diǎn)到子結(jié)點(diǎn)的邊上的數(shù)字表示按照該系統(tǒng)相應(yīng)的規(guī)則推理。只要我們符合這個(gè)系統(tǒng)的推理規(guī)則，就可以得到一棵樹(shù)，這棵樹(shù)上每個(gè)結(jié)點(diǎn)都是該系統(tǒng)中的定理，那么現(xiàn)在問(wèn)題就轉(zhuǎn)化為： $WU$ 是否存在于這棵定理樹(shù)上？
我們可以看到，這棵樹(shù)的層次是無(wú)窮的，如果 $WU$ 是該系統(tǒng)的定理，則必然可以在該樹(shù)的某一層次上找到它，而且總會(huì)在有限步驟內(nèi)找到。但是，如果 $WU$ 不在這棵樹(shù)上，那我們就永遠(yuǎn)也找不到它，這樣也就沒(méi)辦法判定它到底是不是定理了。但我們希望的是，在一個(gè)形式系統(tǒng)中一個(gè)命題是否定理最好能在有限步驟內(nèi)給出答案。因?yàn)槲覀兿Ｍ诎堰@個(gè)問(wèn)題交給一個(gè)有計(jì)算能力的機(jī)器時(shí)，它能在有限時(shí)間給出問(wèn)題的解答，人是一種智能生物(姑且這樣認(rèn)為吧)，我們可以靠直覺(jué)發(fā)現(xiàn) $WU$ 應(yīng)該不是系統(tǒng)的定理甚至非常確信，因?yàn)槿祟?lèi)總會(huì)發(fā)現(xiàn)一些除了系統(tǒng)公理和規(guī)則之外的特定模式和規(guī)律，所以我們不會(huì)為了這個(gè)問(wèn)題無(wú)休止地推理下去，但是機(jī)器并不這樣，想讓機(jī)器解決這個(gè)問(wèn)題，它就必須能有一個(gè)可以終止的條件，能保證在有限時(shí)間解決該問(wèn)題。
那么 $WU$ 到底在不在這棵樹(shù)上呢？如果交給機(jī)器并按照 $WJU$ 系統(tǒng)自身的規(guī)則并給不了我們答案，我們需要另尋它法，借助一些系統(tǒng)之外的規(guī)則來(lái)幫助我們。注意這里借助系統(tǒng)外規(guī)則的含義，你馬上就會(huì)看到它并不是改變了系統(tǒng)規(guī)則，而是在一個(gè)兼容該系統(tǒng)的系統(tǒng)上去做推理。我們借助的這個(gè)系統(tǒng)就是一個(gè)和 $WJU$ 同構(gòu)的系統(tǒng) $310$ 。所謂同構(gòu)就是這兩個(gè)系統(tǒng)結(jié)構(gòu)是完全一樣的，只是我們換用了字符來(lái)進(jìn)行表示，用 $W$ 對(duì)應(yīng) $3$ ， $J$ 對(duì)應(yīng) $1$ ， $U$ 對(duì)應(yīng) $0$ ，所有規(guī)則不變。

WJU的同構(gòu)系統(tǒng)310

看上去只是換了字符，那這樣做有什么好處呢，好處就是這樣做我們?yōu)檫@個(gè)系統(tǒng)引入了數(shù)論的性質(zhì)， $WJU$ 由一個(gè)字符串組成的系統(tǒng)變成了一個(gè)由 $3,1,0$ 三個(gè)數(shù)字組成自然數(shù)集合了。
同構(gòu)系統(tǒng)310

該符號(hào)系統(tǒng)是由 $3，1，0$ 所組成的自然數(shù)
自然數(shù) $31$ 在系統(tǒng)中(公理)
系統(tǒng)規(guī)則：
如果集合中有數(shù)以 $1$ 結(jié)尾，則末尾添加一個(gè) $0$ 也是集合中的數(shù)
如果集合中有數(shù)以 $3$ 開(kāi)始，則把 $3$ 后面的數(shù)字重復(fù)一次添加在后面也是集合中的數(shù)
如果集合中有數(shù)包含 $111$ ，則把 $111$ 替換為 $0$ 也是集合中的數(shù)
如果集合中有數(shù)包含 $00$ ，去掉 $00$ 也是集合中的數(shù)

那么 $WU$ 是否是系統(tǒng) $WJU$ 的定理就轉(zhuǎn)化為 $30$ 是否是系統(tǒng) $310$ 的定理。
在 $310$ 系統(tǒng)中可以很輕松地判定出，這個(gè)系統(tǒng)中的數(shù)都不可能被 $3$ 整除，這很顯然：
首先， $31$ 不能被 $3$ 整除，其次，規(guī)則1，2，3，4都無(wú)法從不能被 $3$ 整除的數(shù)中生成能被 $3$ 整除的數(shù)。
這下清楚了， $30$ 能被 $3$ 整除，故 $30$ 不是系統(tǒng) $310$ 的定理，從而 $WU$ 不是系統(tǒng) $WJU$ 的定理。
怎么樣，神奇吧。

給我們的啟發(fā)

在上述討論中，我們已經(jīng)看到，在僅僅使用系統(tǒng)本身的公理和規(guī)則是難以保證在有限步驟內(nèi)判定一個(gè)命題是否是該系統(tǒng)的定理的。有時(shí)為了判定，我們需要系統(tǒng)外的規(guī)則，比如同構(gòu)擁有數(shù)論性質(zhì)的系統(tǒng)。
這揭示了一種人和機(jī)器的某種區(qū)別，人能夠在按照系統(tǒng)規(guī)則推理時(shí)發(fā)現(xiàn)一些特定的規(guī)律和模式，這些規(guī)律和模式促使我們尋找系統(tǒng)之外的手段來(lái)解決研究的問(wèn)題，但是同樣的任務(wù)交給機(jī)器就不會(huì)這樣了。

形式系統(tǒng)pq

再來(lái)看另外一個(gè)有趣的形式系統(tǒng)——pq系統(tǒng)，該系統(tǒng)有三個(gè)不同的符號(hào)：
$p,q,-$

系統(tǒng)公理的描述型定義：只要 $x$ 僅由短杠組成，那么 x-qxp- 就是一條公理。
系統(tǒng)的唯一生成規(guī)則：假設(shè) $x，y，z$ 都代表由短杠組成的符號(hào)串，且 $xqypz$ 是一條已知定理，那么 x-qypz- 就是一條定理。
比如讓x是“ ---” ， y是“ --” ， z是“ -” ，這條規(guī)則就是：如果 ---q--p- 是一條定理，則 ----q--p-- 也是一條定理。
現(xiàn)在我們的問(wèn)題是，給定一個(gè)符號(hào)串如何判定它是不是pq系統(tǒng)的定理。
首先由系統(tǒng)公理和規(guī)則，一個(gè)串一定要以一組短杠開(kāi)頭，然后有一個(gè)q，接著是第二組短杠，然后是p，最后是另一組短杠，這才有可能成為定理。這樣的符號(hào)串都叫作良構(gòu)符號(hào)串。凡是非良構(gòu)的一定不是定理?？梢园l(fā)現(xiàn)，一個(gè)良構(gòu)符號(hào)串是否是定理的標(biāo)準(zhǔn)是后兩組短杠加起來(lái)是否等于第一組短杠。例如： ----q--p-- 是一條定理，因?yàn)?等于2加2，而 -q--p-- 不是一條定理，因?yàn)?不等于2加2。另外，該系統(tǒng)的定理是不斷加長(zhǎng)的，因?yàn)椴](méi)有縮短符號(hào)串的規(guī)則。
這樣一來(lái)對(duì)于符號(hào)串是否是定理的判定就可以設(shè)計(jì)算法了：

自底向上方案：從基礎(chǔ)公理和生成規(guī)則一步步加長(zhǎng)字符串，這樣會(huì)把系統(tǒng)的每一條定理都產(chǎn)生出來(lái)。當(dāng)出現(xiàn)比要判定的串更長(zhǎng)的串時(shí)還沒(méi)有出現(xiàn)這個(gè)需要判定的串，就可以說(shuō)這個(gè)串不是定理。

注意區(qū)分和WJU系統(tǒng)的區(qū)別，WJU由于同時(shí)有加長(zhǎng)和縮短的規(guī)則所以不能這樣簡(jiǎn)單判定。

自頂向下方案：將要判定的串按照規(guī)則往短串回溯，如果最終剩余的短串是系統(tǒng)的公理，則該串就是定理。

同構(gòu)產(chǎn)生意義

從前面的討論中可以發(fā)現(xiàn)，pq系統(tǒng)的模式特別像自然數(shù)加法，我們可以把q解釋為equel，p解釋為plus，短杠數(shù)目對(duì)應(yīng)到自然數(shù)。是什么東西使我們那樣想的呢？因?yàn)槲覀冊(cè)趐q定理與加法之間看到了同構(gòu)。

pq與加法同構(gòu)

“ 同構(gòu)” 這個(gè)詞的適用情景是：兩個(gè)系統(tǒng)可以互相建立映射，并且每一個(gè)系統(tǒng)的每一部分在另一個(gè)系統(tǒng)中都有一個(gè)相應(yīng)的部分。這里“ 相應(yīng)” 的意思是：在各自的系統(tǒng)中，相應(yīng)的兩個(gè)部分起著相類(lèi)似的作用。當(dāng)然嚴(yán)格的同構(gòu)需要在數(shù)學(xué)上定義。有了同構(gòu)，我們就可以把對(duì)原本很復(fù)雜我們不熟悉的系統(tǒng)的研究轉(zhuǎn)換到對(duì)同構(gòu)系統(tǒng)的研究上，就像pq系統(tǒng)本身是一堆符號(hào)，但當(dāng)與加法建立同構(gòu)后，在相應(yīng)的解釋下這些符號(hào)就有了意義。定理的同構(gòu)反應(yīng)了世界的部分真理。
有意義的解釋和無(wú)意義的解釋
p:馬 q:幸福 -:蘋(píng)果，這樣的解釋就是無(wú)意義的，因?yàn)檫@樣的解釋對(duì)人來(lái)說(shuō)和原來(lái)沒(méi)什么區(qū)別，并不對(duì)應(yīng)現(xiàn)實(shí)世界的真理。
主動(dòng)意義與被動(dòng)意義
受加法的影響我們可能認(rèn)為在pq系統(tǒng)中 --------q--p--p--p-- 是一條定理。至少，我們可能希望這個(gè)符號(hào)串是一條定理，因?yàn)?等于2加2加2加2，但它不是定理，因?yàn)樗皇橇紭?gòu)的，這樣的解釋在pq系統(tǒng)中是錯(cuò)誤的，我們的有意義的解釋都是從良構(gòu)符號(hào)串中得出的。所以在一個(gè)形式系統(tǒng)中，意義一定是“ 被動(dòng)的” 。我們可以根據(jù)其組成符號(hào)的意義來(lái)讀每個(gè)符號(hào)串，但是我們沒(méi)有權(quán)力只根據(jù)我們給符號(hào)指定的意義而創(chuàng)造出新的定理。經(jīng)過(guò)解釋的形式系統(tǒng)是橫跨在沒(méi)有意義的系統(tǒng)與有意義的系統(tǒng)之間的。可以認(rèn)為，它們的符號(hào)串是“ 表達(dá)” 事物的，但這也必定是系統(tǒng)的形式性質(zhì)的產(chǎn)物。
多重意義
pq系統(tǒng)也可以解釋為減法。一個(gè)系統(tǒng)可以有不同的解釋。解釋只要精確地反映現(xiàn)實(shí)世界的某種同構(gòu)，就是有意義的。當(dāng)現(xiàn)實(shí)世界中的不同方面彼此同構(gòu)時(shí)（這里是說(shuō)加法和減法），一個(gè)形式系統(tǒng)可以與這兩者都同構(gòu)，因此可以有多種被動(dòng)意義。
形式系統(tǒng)與現(xiàn)實(shí)
系統(tǒng)的定理和有關(guān)那部分現(xiàn)實(shí)中的真理同構(gòu)。然而，現(xiàn)實(shí)和形式系統(tǒng)是互相獨(dú)立的，并不需要意識(shí)到在兩者之間存在著同構(gòu)關(guān)系，他們每一方面都獨(dú)立存在，不論我們是否知道加法、知道2等于1加1，在pq系統(tǒng)的公理和規(guī)則下 --q-p- 都是一條定理，并且不論我們是否把它與加法相聯(lián)系，--q-p- 總是一條定理。
就形式系統(tǒng)而言，我們幾乎只觸及了表面。人們很自然地想知道，現(xiàn)實(shí)的哪一部份能夠用一組支配無(wú)意義符號(hào)的形式規(guī)則來(lái)加以模仿?，F(xiàn)實(shí)世界的一切都可以變?yōu)樾问较到y(tǒng)嗎？

形式系統(tǒng)簡(jiǎn)介

數(shù)理邏輯中，只是使用真值計(jì)算，以帶入規(guī)則，替換規(guī)則進(jìn)行推演是難以反應(yīng)人類(lèi)思維的推理過(guò)程，我們需要建立嚴(yán)密的符號(hào)推理體系。也就是我們要像做數(shù)學(xué)計(jì)算一樣進(jìn)行推理，這樣的推理體系就是形式系統(tǒng)。
形式系統(tǒng)

形式系統(tǒng)是一個(gè)符號(hào)體系
形式系統(tǒng)中的概念用符號(hào)來(lái)表示，推理過(guò)程即符號(hào)變換的過(guò)程
它以若干最基本的重言式(永真式)為基礎(chǔ)，稱(chēng)做公理
系統(tǒng)內(nèi)符號(hào)變換的依據(jù)是若干由重言式導(dǎo)出重言式的規(guī)則，稱(chēng)作推理規(guī)則

公理和推理規(guī)則能確保正確的前提總能得到正確的推理結(jié)果。
證明
公式序列 $A_1,A_2,...,A_m$ 稱(chēng)作 $A_m$ 的一個(gè)證明，如果 $A_i(1\leq{i}\leq{m})$ :

或者是公理
或者是由 $A_{j_1},A_{j_2},...,A_{j_k}(j_1,...,j_k\leq{i})$ 用推理規(guī)則推得

當(dāng)這樣的證明存在時(shí)，稱(chēng) $A_m$ 為系統(tǒng)的定理。
演繹
設(shè) $\Gamma$ 為一公式集合，公式序列 $A_1,A_2,...,A_m$ 稱(chēng)作 $A_m$ 的以 $\Gamma$ 為前提的一個(gè)演繹，如果 $A_i(1\leq{i}\leq{m})$ :

或者是公理
或者是 $\Gamma$ 中的公式
或者是由 $A_{j_1},A_{j_2},...,A_{j_k}(j_1,...,j_k\leq{i})$ 用推理規(guī)則推得

當(dāng)這樣的演繹存在時(shí)，稱(chēng) $A_m$ 為 $\Gamma$ 的演繹結(jié)果。
可以看到，其實(shí)證明就是演繹在 $\Gamma$ 為空集時(shí)的特例。

命題演算形式系統(tǒng)PC(Proposition Calculus)

我們將命題以及重言式變換演算構(gòu)造為形式系統(tǒng)，成為命題演算形式系統(tǒng)PC：
PC的構(gòu)成：

首先，PC是一個(gè)符號(hào)系統(tǒng)
命題變?cè)?img class="math-inline" src="https://math.jianshu.com/math?formula=p%2Cq%2Cr%2Cs%2C..." alt="p,q,r,s,..." mathimg="1">
命題常元： $t,f$ ，分別代表真和假
聯(lián)結(jié)詞和括號(hào)： $\neg,\rightarrow$ (功能完備集)， $()$
命題公式：由命題常元和變?cè)戏ńM成的公式，命題常元命題變?cè)旧砭褪枪健?img class="math-inline" src="https://math.jianshu.com/math?formula=A%2CB" alt="A,B" mathimg="1">是公式，則 $\neg{A}, A \rightarrow B$ 也是公式，只有有限次使用上面兩條規(guī)則得到的符號(hào)串才是命題公式。

PC的公理：
$A \rightarrow (B \rightarrow A) \\ (A \rightarrow (B \rightarrow C))\rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) \\ (\neg{A} \rightarrow \neg{B}) \rightarrow (B \rightarrow A)$
PC的推理規(guī)則
分離規(guī)則： $A,A\rightarrow B\ than\ B$ ( $A,B$ 表示任意公式)，也就是如果公式序列已經(jīng)有 $A$ 和 $A\rightarrow B$ 那么可以在公式序列后面添加上 $B$ 。

此外為了擴(kuò)大形式系統(tǒng)的可研究范圍以及形式語(yǔ)言的易理解性，還有謂詞演算形式系統(tǒng)FD，自然推理系統(tǒng)ND等等。

完美的形式系統(tǒng)應(yīng)該具有的性質(zhì)：

合理性：如果 $A$ 是PC的定理，則 $A$ 是重言式；如果 $A$ 是集合 $\Gamma$ 的演繹結(jié)果，則 $A$ 是 $\Gamma$ 的邏輯結(jié)果。合理性說(shuō)明了PC中的定理和演繹結(jié)果都是合乎邏輯的。
一致性： $\neg{A},A$ 不能同時(shí)出現(xiàn)在PC中，也就是一個(gè)符合邏輯的形式系統(tǒng)不可能即推出 $A$ ，又推出 $\neg{A}$ 這兩個(gè)自相矛盾的命題。
完備性：如果 $A$ 是重言式，則 $A$ 一定是PC中的定理，這意味著PC中一定存在證明序列可以得到 $A$ ；如果 $A$ 是公式集合 $\Gamma$ 的邏輯結(jié)果，則 $A$ 一定是 $\Gamma$ 的演繹結(jié)果。也就是凡是合乎邏輯的命題，一定可以被該系統(tǒng)證明。

PC是滿(mǎn)足上述性質(zhì)的(證明太難，略了)。那么任意一個(gè)形式系統(tǒng)可不可能都同時(shí)滿(mǎn)足上面3個(gè)性質(zhì)呢，現(xiàn)在來(lái)思考一下這個(gè)問(wèn)題，為了保證推得的命題是真命題，首先性質(zhì)1和性質(zhì)2必須被滿(mǎn)足(否則這樣的系統(tǒng)沒(méi)有意義)。那么性質(zhì)3呢？一個(gè)真命題一定能夠被系統(tǒng)本身證明嗎？或者換句話(huà)說(shuō)：一個(gè)命題一定能夠在該系統(tǒng)內(nèi)部被證明是真或者是假嗎？答案是否定的，這也正是哥德?tīng)査龅墓ぷ髦弧?br> 元定理
元定理就是關(guān)于定理證明的定理。

演繹定理： $\Gamma$ 推出 $A\rightarrow B$ 當(dāng)且僅當(dāng) $\Gamma \cup{\{A\}}$ 推出 $B$ ，特別當(dāng) $\Gamma$ 為空集時(shí)， $A\rightarrow B$ 當(dāng)且僅當(dāng) $A$ 推出 $B$ 。
歸謬定理：若 $\Gamma \cup{\neg{A}}$ 推出 $B$ 且 $\Gamma \cup{\neg{A}}$ 推出 $\neg{B}$ ，則 $\Gamma \rightarrow A$ ，其意義在于如果同一組前提能推導(dǎo)出相互矛盾的結(jié)論，說(shuō)明這組前提之間相互不一致。那么這組前提中就存在一些前提，它的反面可以被 $\Gamma$ 推出(對(duì)立面是正確的)。
窮舉定理：若 $\Gamma \cup{\neg{A}}$ 推出 $B$ 且 $\Gamma \cup{A}$ 推出 $B$ ，那么 $\Gamma$ 推出 $B$ (不依據(jù) $A$ )，其意義在于如果一個(gè)前提和這個(gè)前提的反面都能推出相同的結(jié)論，那么說(shuō)明這個(gè)結(jié)論的成立與該前提是否成立沒(méi)有關(guān)系，就可以從 $\Gamma$ 中剔除這個(gè)前提。

一階謂詞演算形式系統(tǒng)(First order predicate Calculus)

FC的符號(hào)系統(tǒng)：
個(gè)體變?cè)簒，y，z，u，v，w，...
個(gè)體常元：a，b，c，d，e，...
個(gè)體間運(yùn)算符號(hào)(函數(shù)符)： $f^{(n)}，g^{(n)}，h^{(n)}，...$ ，其中n是正整數(shù)，表示函數(shù)的元數(shù)
謂詞符號(hào)： $P^{(n)},Q^{(n)},R^{(n)},S^{(n)},...$ ，n表示謂詞的元數(shù)，當(dāng)n=0時(shí)謂詞公式退化為命題常元
聯(lián)結(jié)詞與括號(hào)： $\neg,\rightarrow,()$
量詞： $\forall$ ( $\exists{x}$ 等價(jià)于 $\neg \forall x \neg$ )
個(gè)體項(xiàng)(term)：簡(jiǎn)稱(chēng)項(xiàng)，個(gè)體變?cè)蛡€(gè)體常元是項(xiàng)；若 $f^{n}$ 是n元函數(shù)符， $t_1,t_2,...t_n$ 為項(xiàng)，則 $f^{n}(t_1,t_2,...,t_n)$ 也為項(xiàng)；只有有限次使用上述規(guī)則得到的符號(hào)串才是項(xiàng)。
合式公式：簡(jiǎn)稱(chēng)公式，若 $P^{n}$ 是n元謂詞符， $t_1,t_2,...t_n$ 為項(xiàng)，則 $P^{n}(t_1,t_2,...,t_n)$ 是公式，n=0時(shí)，命題常元也是公式；如果 $A,B$ 是公式，v為任意一個(gè)個(gè)體變?cè)?img class="math-inline" src="https://math.jianshu.com/math?formula=%5Cneg%20A%2CA%5Crightarrow%20B%2C%5Cforall%7BvA(v)%7D" alt="\neg A,A\rightarrow B,\forall{vA(v)}" mathimg="1">都是公式；只有有限次使用上述規(guī)則得到的符號(hào)串才是公式。
全稱(chēng)封閉式：是用全稱(chēng)量詞 $\forall$ 約束給定公式所有自由變?cè)玫拈]公式。

FC的公理：
$A \rightarrow (B \rightarrow A) \\ (A \rightarrow (B \rightarrow C))\rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) \\ (\neg{A} \rightarrow \neg{B}) \rightarrow (B \rightarrow A) \\ \forall{xA(x)} \rightarrow A(t)\\ \forall{x}(A(x)\rightarrow B(x))\rightarrow (\forall{x}A(x)\rightarrow \forall{x}B(x)) \\ A\rightarrow \forall{xA} \\ 上述6條的全稱(chēng)封閉式都是FC的公理$
FC的推理規(guī)則：
分離規(guī)則： $A,A\rightarrow B\ than\ B$ ( $A,B$ 表示任意公式)，也就是如果公式序列已經(jīng)有 $A$ 和 $A\rightarrow B$ 那么可以在公式序列后面添加上 $B$ 。
全稱(chēng)引入規(guī)則：
存在消除規(guī)則：
上述兩條規(guī)則一樣可以推廣到演繹中。如存在消除規(guī)則，我們經(jīng)常在數(shù)學(xué)證明中用“不妨設(shè)”理論依據(jù)就是這個(gè)規(guī)則。

自然推理系統(tǒng)ND

FC和PC都比較繁復(fù)，為了追求簡(jiǎn)潔只用了兩個(gè)聯(lián)結(jié)詞，如果能夠引入更多聯(lián)結(jié)詞，量詞，推理規(guī)則，那么證明和演繹都會(huì)更加的自然。
(演繹)為了證明A-＞B，常假設(shè)A成立，如果能夠證明B成立，則A-＞B也就被證明。
(歸謬/反證)為了證明A，常假設(shè)非A，得到矛盾。
(窮舉)已知A或B，常假設(shè)A和B成立分別證明C，若都能成功，則完成C的證明。
(不妨設(shè))
在形式系統(tǒng)中引入帶假設(shè)的推理規(guī)則，能夠使推理過(guò)程更加接近人的思維，更加高效和便捷。
自然推理系統(tǒng)ND
采用5個(gè)聯(lián)結(jié)詞，2個(gè)量詞
少數(shù)的公理，更多的規(guī)則，引入假設(shè)。
用推理規(guī)則體現(xiàn)人的推理習(xí)慣
公理只有一個(gè) $\Gamma,A$ 可以推出 $A$ ，這也是自然推理系統(tǒng)的證明方式。
推理規(guī)則(18條)：
假設(shè)引入規(guī)則
假設(shè)消除規(guī)則
$\vee$ 引入規(guī)則
$\vee$ 消除規(guī)則
$\wedge$ 引入規(guī)則
$\wedge$ 消除規(guī)則
$\rightarrow$ 引入規(guī)則
$\rightarrow$ 消除規(guī)則
$\neg$ 引入規(guī)則
$\neg$ 消除規(guī)則
$\neg\neg$ 引入規(guī)則
$\neg\neg$ 消除規(guī)則
$\leftrightarrow$ 引入規(guī)則
$\leftrightarrow$ 消除規(guī)則
$\forall$ 引入規(guī)則
$\forall$ 消除規(guī)則
$\exists$ 引入規(guī)則
$\exists$ 消除規(guī)則
FC的公理和定理都是ND的定理，ND是合理的一致的完備的。