一阶逻辑

维基百科,自由的百科全书
跳转至: 导航搜索

一阶逻辑是使用於数学哲学语言学電腦科學中的一种形式系统

過去一百多年,一階邏輯出現過許多種名稱,包括:一阶谓词演算低階谓词演算量化理論谓词逻辑(一個較不精確的用詞)。一階邏輯和命題邏輯的不同之處在於,一階邏輯有使用量化變數。一個一階邏輯,若具有由一系列量化變數、一個以上有意義的謂詞字母及包含了有意義的謂詞字母的純公理所組成的特定論域,即是一個一階理論

一階邏輯和其他高階邏輯不同之處在於,高階邏輯的謂詞可以有謂詞或函數當做引數,且允許謂詞量詞或函數量詞的(同時或不同時)存在[1]。在一階邏輯中,謂詞通常和集合相關連。在有意義的高階邏輯中,謂詞則會被解釋為集合的集合。

存在許多對一階邏輯是可靠(所有可證的敘述皆為真)且完備(所有為真的敘述皆可證)的演繹系統。雖然一階邏輯的邏輯歸結只是半可判定性的,但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯定理,如勒文海姆–斯科倫定理緊緻性定理

一階邏輯是數學基礎中很重要的一部份,因為它是公理系統的標準形式邏輯。許多常見的公理系統,如一階皮亞諾公理和包含策梅洛-弗蘭克爾集合論公理化集合論等,都可以形式化成一階理論。然而,一階定理並沒有能力去完整描述及範疇性地建構如自然數實數之類無限的概念。這些結構的公理系統可以由如二階邏輯之類更強的邏輯來取得。

簡介[编辑]

不像命題邏輯只處理簡單的陳述命題,一階邏輯還額外包含了謂詞和量化

謂詞像是一個會傳回真或偽的函數。考慮下列句子:「蘇格拉底是哲學家」、「柏拉圖是哲學家」。在命題邏輯裡,上述兩句被視為兩個不相關的命題,簡單標記為pq。然而,在一階邏輯裡,上述兩句可以使用謂詞以更相似的方法來表示。其謂詞為Phil(a),表示a是哲學家。因此,若a代表蘇格拉底,則Phil(a)為第一個命題-p;若a代表柏拉圖,則Phil(a)為第二個命題-q。一階邏輯的一個關鍵要點在此可見:字串「Phil」為一個語法實體,以當a為哲學家時陳述Phil(a)為真來賦與其語義。一個語義的賦與稱為解釋

一階邏輯允許以使用變數的方法推論被許多元件共享的性質。例如,令Phil(a)表示a為哲學家,且令Schol(a)表示a為學者。則公式

\text{Phil}(a)\to \text{Schol}(a) \,

表示若a為哲學家,則a為學者。符號\to被用來標記一個條件敘述。箭號的左邊為假設,右邊則為結論。此一公式的真值取決於標記成a的元件,及「Phil」和「Schol」的解釋之上。

「對於每個a,若a為哲學家,則a為學者」之類形式的斷言,需要同時使用變數及量化。再次,令Phil(a)表示a為哲學家,且令Schol(a)表示a為一學者,則一階敘述

\forall a ( \text{Phil}(a) \to \text{Schol}(a))

表示不論a代表什麼,若a為哲學家,則a為學者。此處的\forall全稱量化)代表宣稱對「所有」a的選擇,括弧內的敘述皆為真的想法。

為了表明,聲稱“如果是一個哲學家然後是一個學者”是假的,一會顯示有一些人是不是一個學者的哲學家。這與存在量詞可以表示反訴 : 若想證明「若a為哲學家,則a為學者」此一宣稱是錯的,有些人會證明存在有些不是學者的哲學家。此一反論可以用存在量化\exists來表示:

\exists a ( \text{Phil}(a) \land \lnot \text{Schol}(a)).

其中,

  • \lnot是否定算符: \lnot \text{Schol}(a)為真若且唯若\text{Schol}(a) \,為假;換句話說,若且唯若a不是學者。
  • \land是合取算符:\text{Phil}(a) \land \lnot \text{Schol}(a)表示a是哲學家且不是學者。

謂詞Phil(a)和Schol(a)都各只有一個參數。但一階邏輯其實也可以表示具有一個以上參數的謂詞。例如,「存在一些人可以在任何時間被愚弄」可表示成

\exists x (\mbox{Person}(x) \and \forall y (\mbox{Time}(y) \rightarrow \mbox{Canfool}(x,y))).

這裡,Person(x)解釋為x是人,Time(y)為y是某段時間,且Canfool(x,y)則為(人)x可在(時)y被愚弄。清楚地說,上述敘述表示至少存在一個人可以在任何時間被愚弄,這比「在任何時間,至少存在一個人可以被愚弄」的敘述要強。後者並不意味著,被愚弄的人在任何時間時上總是要是同一位。

量化的範圍是由可以用來滿足量化的物件所組成的集合(在本節中的一些非正式的例子裡,量化的範圍並沒有被指定)。除了指定Person和Time等謂詞符號的意義,解釋也必須指定一個非空集合,稱為論域,做為量化的範圍。因此,\exists a \text{Phil}(a)之類形式的敘述在一特定解釋下稱之為真,若在可用來賦予謂詞中符號Phil意義的解釋所指定的論域裡存在著物件。

語法[编辑]

一階邏輯可分成兩個主要的部份:語法決定哪些符號的組合是一階邏輯內的合法表示式,而語義則決定這些表示式之前的意思。

詞彙表[编辑]

和英語之類的自然語言不同,一階邏輯的語言是完全形式的,因為可以機械式地判斷一個給定的表示式是否合法。存在兩種合法的表示式:「項」(直觀上代表物件)和「公式」(直觀上代表可真或偽的謂詞)。一階邏輯的項與公式是一串符號,這些符號一起形成了這個語言的詞彙表。如同所有的形式語言一般,符號本身的性質不在形式邏輯討論的範圍之內;它們通常只被當成字母及標點符號。

一般會將詞彙表中的符號分成「邏輯符號」(總有相同的意思)及「非邏輯符號」(意思依解釋不同而變動)。例如,邏輯符號\land總是解釋成「且」,而絕不會解釋成「或」。另一方面,一個非邏輯謂詞符號,如Phil(x),可以解釋成「x是哲學家」、「x的個名為Philip 的人」或任何其他的1元謂詞,單看其解釋為何。

邏輯符號[编辑]

詞彙表中存在若干個邏輯符號,雖然會因作者而異,但通常包括:

  • 量化符號\forall\exists
  • 邏輯聯結詞\land\lor條件\rightarrow雙條件\harr否定\lnot。偶爾還會包括一些其他的邏輯聯結詞。某些作家會使用\Rightarrow或Cpq來表示\rightarrow,用\Harr或Epq來表示\harr,特別是文中\to被拿去做其他用途之時。更多地,也有用\supset來表示\rightarrow,用\equiv來表示\harr,用(~)、Np或Fpq來表示\lnot,用||或Apq來表示\lor,以及用&或Kpq來表示\land,尤其是這些符號因技術上的原因無法輸入時。
  • 括號、方括號及其他標點符號。此類符號的選擇依文章不同而有所不同。
  • 無限集的變數,通常標記為英文字母末端的小寫字母xyz、…,也常會使用下標來區別不同的變數:x0x1x2、…。
  • 一個等式符號= 。詳見下面的「等式」一節。

需注意,並不是所有的符號都需要,只要有量化符號的其中一個、否定及且、變數、括號及等式就足夠了。還存在許多定義了額外邏輯符號的變體:

  • 有時也會包括真值常數,用T、Vpq\top來表示「真」,並用F、Opq\bot來表示「假」。若沒有此類零參數的邏輯算符,這兩個常數就只能用量化來表示。
  • 有時也會包括額外的邏輯聯結詞,如謝費爾豎線、NAND及異或

非邏輯符號[编辑]

非邏輯符號用來表示論域上的謂詞(關係)、函數及常數。以前標準上會對所有不同的用途使用相同的無限集的非邏輯符號,而最近則會根據應用的不同而使用不同的非邏輯符號。因此變得需要列舉出使用於一特定應用中的所有非邏輯符號。其選擇是經由標識來形成的。

傳統的做法是對所有的應用都只有單一個無限集的非邏輯符號。因此,根據傳統的做法只會存在一種一階邏輯的語言。這種做法現在依然很常見,尤其是在哲學方面的書籍。

  1. 對每個整數n ≥ 0,皆存在一組n謂詞符號。因為這些謂詞符號表示n個元素間的關係,因此也稱為關係符號。對每個參數量n,皆能有無限多個謂詞符號:#:Pn0, Pn1, Pn2, Pn3,…
  2. 對每個整數n ≥ 0,皆存在無限多個n函數符號
    f n0, f n1, f n2, f n3,…

在當代的數理邏輯裡,標識會因應用的不同而不同。數學裡的典型標識,在裡為{1, ×},或只為{×};在有序體裡為{0, 1, +, ×, <}。並沒有限制非邏輯符號的數量,標識可以是的、有限、無限,甚至是不可數的。例如,在勒文海姆–斯科倫定理的證明之中即會出現不可數的標識。

根據最近的做法,每個非邏輯符號皆為下列兩種類型的其中一種。

  1. 具有0個或0個以上參數的謂詞符號(或關係符號)。通常標記為大寫字母PQR、…。
    • 0參數的關係可以視同為命題變數。例如可以代表任何敘述的P
    • P(x)為具有1個參數的謂詞變數,其中一個可能的解釋為「x是個人」。
    • Q(x,y)為具有2個參數的由詞變數,其中一些可能的解釋有「x大於y」或「xy的父親」。
  2. 具有0個或0個以上參數的函數符號。標常標記為小寫字母fgh、…。
    • 舉例來說,f(x)可以解釋成「x的父親」;在算術裡,可代表「-x」;在集合論裡,可代表「x冪集」。gx,y)在算術裡可代表「x+y」;在集合論裡,可代表「xy的聯集」。
    • 0參數的函數符號也稱為常數符號,常標記成英文字母前端的字母abc、…。a可代表「蘇格拉底」;在算術裡,可代表0;在集合論裡,可代表空集。

形成規則[编辑]

形成規則定義一階邏輯的項及公式。因為項及公式被表示為一串符號,這些規則可被用來寫成項及公式的形式文法。這些規則通常是上下文無關的(規則的每個結果在其左側都會有單一個符號),除非允許有無限多符號,且有許多開始符號,如中的變數。

[编辑]

可依如下規則遞歸地定義:

  1. 變數。每個變數皆是項。
  2. 函數。每個具有n個參數的表示式ft1,...,tn,其中每個參數ti是項,且f是具有n個參數的函數符號)是項。另外,標記不同常數的符號是個0參數的函數符號,因此也是項。

只有可經由有限次地應用上述規則來得到的表示式才是項。舉例來說,不存在一個同時是項且包含謂詞符號的表示式。

公式[编辑]

公式(或稱合式公式)可依如下規則遞歸地定義:

  1. 謂詞符號。若P是一個n元謂詞符號,且t1, ..., tn是項,則P(t1,...,tn)是公式。
  2. 等式。若等式符號算是邏輯的一部份,且t1t2是項,則t1 = t2是公式。
  3. 否定。若φ是公式,則\negφ是公式。
  4. 二元聯結詞。若φ及ψ是公式,則(φ \rightarrow ψ)是公式。其他的二元邏輯聯結詞也可相似的規則。
  5. 量化。若φ是公式,且x是變數,則\forall x \varphi\exists x \varphi都是公式。

只有可經由有限次地應用上述規則來得到的表示式才是公式。由頭兩個規則得到的公式稱為原子公式

舉例來說,

\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z)))

是公式,若f是1元函數符號,P是1元謂詞符號,且Q是3元謂詞符號。另一方面,\forall x\, x \rightarrow則不是公式,雖然這也是由詞彙表中的符號組成的字串。

定義中的括號,其用途是為了確保任何公式都只能依遞歸定義以單一種方法得到(換句話說,每一個公式都只存在唯一的剖析樹)。這個性質被稱為公式的唯一可讀性。對於括號要用在公式中的哪裡存在有許多的慣例。例如,有些作者會使用冒號或句號來代替括號,或變更括號插入的地方。但每個作家個人的定義都必須證明會滿足唯一可讀性。

定義公式的規則無法定義「若-則-否則」函數ite(c,a,b),其中的c是個以公式表示的條件,當c為真時傳回a,為假時傳回b。這是因為謂詞和函數都只能接受項當做其參數,但上述函數的第一個參數為公式。某些建構在一階邏輯上的語言,如SMT-LIB 2.0,會增加此一定義。[2]

標示慣例[编辑]

為了方便起見,會約定邏輯算符的優先性,來減少括號使用的情況。這些規則和算術中的運算順序很像,一個常見的慣例為:

  • \lnot最先賦值;
  • 下一個為\land\lor先賦值;
  • 再下一個為量化先賦值;
  • \to則最後賦值。

此外,定義中不需要的額外標點符號也許會插入公式中,使公式更容易閱讀。因此,公式

(\lnot \forall x P(x) \to \exists x \lnot P(x))

可寫成

(\lnot [\forall x P(x)]) \to \exists x [\lnot P(x)].

在某些領域裡,常見使用中綴表示法來代表二元關係及函數,而非上面定義的前綴表示法。例如,在算術中,一般會寫成「2+2=4」,而非「=(+(2,2),4)」。一般會將以中綴表示法表示的公式當做是以前綴表示法表示的對應公式的縮寫。

上面定義中的二元聯結詞,如\to,是使用中綴表示法。一個較少見的慣例為波蘭表示法,它將\rightarrow\wedge等放在參數的前面而非之間。這個表示法允許捨棄所有的標點符號。波蘭表示法是簡潔且優雅的,但因為對人類很難閱讀,所以實務上不常使用。使用波蘭表示法,公式

\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z)))

會變成"∀x∀y→Pfx¬→ PxQfyxz"

自由變數和約束變數[编辑]

在一個公式裡,變數可能是自由的或約束的。直觀上來看,一個變數在公式裡是自由的,若其沒化量化:在\forall y\, P(x,y)裡,變數x是自由的,而y則是約束的。自由變數和約束變數可依如下規則遞歸地定義:

  1. 原子公式。若φ是原子公式,則x在φ裡是自由的,若且唯若x出現在φ裡。更甚之,在原子公式中不存在約束變數。
  2. 否定。。x\negφ裡是自由的,若且唯若x在φ裡是自由的。x\negφ裡是約束的,若且唯若x在φ裡是約束的。
  3. 二元聯結詞x在(φ \rightarrow ψ)裡是自由的,若且唯若x在φ或ψ裡是自由的。x在(φ \rightarrow ψ)裡是約束的,若且唯若x在φ或ψ裡是約束的。相同的規則也適用於其他的二元聯結詞之上。
  4. 量化x\forally φ裡是自由的,若且唯若x在φ裡是自由的,且x是個和y相異的符號。而且,x\forally φ裡是約束的,若且唯若xyx在φ裡是約束的。相同的規則也適用於\exists之上。

舉例來說,在\forallx \forally (P(x)\rightarrow Q(x,f(x),z))裡,xy是約束變數,z是自由變數,而w則兩者皆不是,因為它沒有出現在公式之中。

自由和約束也可以用來專指在公式裡特定地方出現的變數。如在P(x) \rightarrow \forall x\, Q(x)裡,第一個x是自由的,而第二個則是約束的。換句話說,xP(x)裡是自由的,而在x in \forall x\, Q(x)裡則是約束的。

在一階邏輯中,一個沒有自由變數的公式稱為一階句子。此類公式在特定解釋之下即會有良好定義的真值。例如,公式Phil(x)是否為真需看x代表什麼,而句子\exists x\, \text{Phil}(x)在一特定解釋下則必為真或必為假。

例子[编辑]

有序阿贝尔群的语言有一个常量0,一个一元函数−,一个二元函数 +,和一个二元关系≤。所以

  • 0, x, y原子项
  • +(x, y), +(x, +(y, −(z)))是,通常写为x + y, x + yz
  • =(+(x, y), 0),≤(+(x, +(y, −(z))), +(x, y))是原子公式,通常写为x + y = 0, x + y - zx + y
  • (∀xy ≤( +(x, y), z))∧(∃x =(+(x, y), 0))是公式,通常写为 (∀xy x + yz)∧(∃x x + y = 0)

語義[编辑]

一階語言的解釋會對語言內的所有非邏輯常數賦予上意義,同時也決定能指明量化範圍的論域。其結果為,每個項都會被賦予其代表的元件,每個句子也都會被賦予上一個真值。這樣,解釋即對語言內的項及公式提供了語義。研究形式語言的解釋的學科稱為形式語義學

論域D是由某種類型的「物件」所組成的非空集合。直觀上來看,一階公式是有關這些物件的敘述。例如,\exists x P(x)敘述存在一個物件x,能使得指涉此物件的謂詞P為真。論域即是此類考量的物件的集合,例如可取D為整數的集合。

函數符號的解釋是函數。舉例來說,若論域由整數所組成,則一個2元的函數符號f能解釋為給出其參數之和的函數。換句話說,符號f和在此解釋下為加法的函數I(f)是相關連的。

常數符號的解釋是一個從單元素集合D0映射至D的函數,也可簡單視為是D內的一個物件。例如,一個解釋可將值I(c)=10賦予常數符號c

n元謂詞符號的解釋是由論域中的元素所組成的n對有序集。這意味著,給定一個解釋、一個謂詞符號及論域中的n個元素,則可依給定的解釋判斷這些元素的謂詞是否為真。例如,一個2元謂詞符號P的解釋I(P)可以是一對整數,能使得第一個整數小於第二個整數。依據這個解釋,謂詞P在其第一個參數小於第二個參數時為真。

一階結構[编辑]

指定一個解釋的最常見方法是指定一個結構(或稱做模型,見下文)。結構包括一個由論域及標識內的非邏輯項的解釋I所組成的非空集合。這個解釋自身是個函數:

  • 每個n元函數符號f都會賦予一個從D^n映射至D的函數I(f)。特別地是,每個標識內的常數符號都會被賦予論域中的一個個體。
  • 每個n元謂詞符號P都會賦予一個在D^n上的關係I(P)(或等價地說,一個從D^n映射至\{true,false\}的函數)。因此,每個謂詞符號都被D上的布林值函數所解釋。

真值的賦值[编辑]

一個公式由給定的解釋及將論域中的元素與每個變數相關連的變數賦值μ來決定為真或為假。需要變數賦值的原因是為了給予具自由變數的公式(如y = x)意義。上述公式的真值為何要看xy是否標記著相同的個體。

首先,變數賦值μ可以擴展到語言內的所有項,使每個項都能映射至論域中的單一元素。下列的規則被用來得到賦值:

  1. 變數。每個變數x皆可得到μ(x)。
  2. 函數。給定一組項t_1, \ldots, t_n(這些項皆已得到論域中的元素d_1, \ldots, d_n)及一個n元函數符號f,則項f(t_1, \ldots, t_n)可得到(I(f))(d_1,\ldots,d_n)

再來,每個公式皆可賦予一個真值。用來得到賦值的遞歸性定義稱為T-模式

  1. 原子公式(1)。公式P(t_1,\ldots,t_n)是依靠\langle v_1,\ldots,v_n \rangle \in I(P)(其中v_1,\ldots,v_n為項t_1,\ldots,t_n的賦值,且I(P)P的解釋)來決定其值是真是假。
  2. 原子公式(2)。公式t_1 = t_2為真,若t_1t_2得到論域中的相同物件(見下面等式一節)。
  3. 邏輯聯結詞\neg \phi 及\phi \rightarrow \psi等形式的公式是依據聯結詞的真值表(如命題邏輯一般)來賦值的。
  4. 存在量化。公式\exists x \phi(x)根據解釋M和變數賦值μ為真,若存在一個只和μ在對x的賦值上有所不同的變數賦值μ',能使得φ根據解釋M和變數賦值μ'為真。此一形式定義是由「\exists x \phi(x)為真,若且唯若存在一種選擇x的方法,使得φ(x)為真」的這個概念來的。
  5. 全稱量化。公式\forall x \phi(x)根據解釋M和變數賦值μ為真,若φ(x)根據每個只和μ在對x的賦值上有所不同的變數賦值μ'及解釋M為真。此一形式定義是由「\forall x \phi(x)為真,若且唯若每一種選擇x的方法,皆能使φ(x)為真」的這個概念來的。

若一個公式不包含自由變數,即為一個句子,則一開始的變數賦值不會影響其真值。換句話說,一個句子根據M\mu為真,若且唯若這個句子根據M及其他的變數賦值\mu'為真。

還有第二種常見的做法可以定義真值,而且不需要依靠變數賦值函數。給定一個解釋M,首先將一組常數符號加至標識之中,每一個在M中的論域的元素對應一個常數符號:稱對每個域論中的元素d,都會固定有一個常數符號cd。如此,解釋就會被擴展至能使每一新的常數符號被賦予至其對應的論域元素上。現在可語法性地定義量化公式的真值如下:

  1. 存在量化。公式\exists x \phi(x)根據M為真,若存在某些在論域中的d,使得\phi(c_d)為真。這裡,\phi(c_d)是用cd取代每個φ內以自由變數出現的x所得到的公式。
  2. 全稱量化。公式\forall x \phi(x)根據M為真,若對每個論域中的d,根據M\phi(c_d)皆為真。

這個做法對所有的句子會給出和使用變數賦值的做法一樣的真值。

有效性、可滿足性及邏輯結論[编辑]

若句子φ在一給定解釋M下為真,則稱M 滿足φ,標記為M \vDash \phi。一個句子稱為可滿足的,若存在某个解釋使其為真。

具自由變數的公式的可滿足性就較為複雜了,因為只用解釋並無法決定此類公式的真值。一個常見的慣例是稱一個具自由變數的公式在一個解釋下為可滿足的,若不論如何將論域中的個體賦予其自由變數,這個公式皆為真。這等價於稱公式為可從足的,若且唯若其全稱閉包為可滿足的。

一個公式是邏輯有效的(或簡單稱為有效的),若在每一個解釋之下皆為真。此類的公式和命題邏輯中的重言式扮演著相似的角色。

一個公式φ是公式ψ的邏輯結論,若每個使得ψ為真的解釋皆會使得φ為真。在此一狀況下,稱φ被ψ邏輯蘊涵著。

代數化[编辑]

另一種賦予一階邏輯語義的方法可經由抽象代數處理。這種方法是將命題邏輯的林登鮑姆-塔斯基代數擴展而成。有如下幾種類型:

這些代數都是純粹擴展兩元素布爾代數而成的

塔斯基和葛范德於1987年證明,沒有超過包在三個以上的量化內的原子句子的部份一階邏輯,其表示力和關係代數相同。上述部份一階邏輯令人十分地感到有興趣,因為它已足夠表示皮亞諾算術公理化集合論,包括典型的ZFC。他們亦證明了,具有簡單有序對的一階邏輯和具有兩個有序的投影函數的關係代數等價。

一階理論、模型及基本類[编辑]

一階理論是由在一特定一階標識內的一組公理所組成的。公理所組成的集合通常是有限的或遞歸可枚舉的,此類的理論稱為是有效的。有些作者要求理論也要包括所有由公理導出的邏輯結論。

滿足給定理論內的所有句子的一階結構稱為此理論的模型基本類是由所有滿足特定理論的結構所組成的集合。這些類是類型論裡的研究主題。

許多理論都有一個預期解釋,即一個在研究理論時會在意的某種模型。例如,皮亞諾公理預期解釋是由一般的自然數和其一般的運算所組成的。不過,勒文海姆–斯科倫定理證明,大多數的一階理論也都會有其他的非標準模型

一個理論是相容的,若不可能由這個理論的公理中證明出矛盾來。一個理論是完備的,若對每個其標識內的公式,此公式或公式的否定會是個由理論公理導出的邏輯結論。哥德爾不完備定理證明,有效的一階理論只要它強到足以蘊涵自然數的理論,即無法同時是相容且完備的。

空論域[编辑]

上述定義需要任何一個解釋的論域均為非空集合。但在如自由邏輯之中,設定空論域是被允許的。更甚之,若代數結構的類包含一個空結構(如空偏序集),當允許空論域時,這個類只能是一階邏輯中的一個基本類,不然就要將空結構由類中移除。

不過,空論域存在著一些難點:

  • 許多常見的推理規則只在論域被要求是非空時才為有效的。一個例子為,當x不是\phi \,內的自由變數時,\phi \lor \exists x \psi會薀涵\exists x (\phi \lor \psi)。這個用來將公式寫成前束範式的規則在非空論域中是可靠的,但在允許空論域時則是不可靠的。
  • 在使用變數賦值函數的解釋中,真值的定義不能和空論域一起運作,因為不存在範圍為空的變數賦值函數。(相似地,也無法將解釋賦予上常數符號。)在甚至是原子公式的真值可被定義之前,都必須選定一個變數賦值函數。然後一個句子的真值即可在任一個變數賦值之下定義出其真值,且可證明其真值不依選定的賦值而變。這個做法在賦值函數不存在時不能運作;除非將其改成配上空論域。

因此,若空論域是被允許的,通常也必須被視成特例。不過,大多數的作家會簡單地將空論域由定義中排除。

代换[编辑]

t是项。φ(x)是可能包含x作为自由变量的公式。

φ(t)可定义为把自由變量x替代为t的结果,但前提是必須没有任何t在φ(x)中是约束的

若非如此,则x替代成t之前,必须先把φ中的约束变量,改为不同于t的符號。

例如把公式φ(x)假定为∀y:yx("x是极大的")。

若用t代換x,则φ(t)即∀y:yt就表示t是极大的。

這裡舉個錯誤的例子,若在φ(x)中含有約束變量y的狀況下,不去修改φ(x)中含有約束變量y,直接把x代換成y,代換結果如下

y:yy

如此一來即成為跟φ(x)意義完全不同的公式。

正確的演算方法為先把φ(x)中的约束变量用到y的地方改成不同於y的符號,好比z

即把∀y:yx改成∀z:zx,這兩命題的意義一致。

再把x代換成y,即為∀z:zy

所以φ(y)表示∀z:zy,而不是∀y:yy

忘记这个条件是声名狼籍的犯错误原因。

推理规则[编辑]

肯定前件充当推理的唯一规则。

叫做全称普遍化的推理规则是谓词演算的特征。它可以陈述为

如果 \vdash Z(x) \vdash \forall x Z(x)

这裡的Z(x)假定表示谓词演算的一个已证明的定理,而∀xZ(x)是它针对于变量x的闭包。谓词字母Z可以被任何谓词字母所替代。

公理[编辑]

下面描述一阶逻辑的公理。如上所述,一个给定的一阶理论有进一步的非逻辑公理。下列逻辑公理刻画了本文的样例一阶逻辑的一种演算[3]

对于任何理论,知道公理的集合是否可用算法生成,或是否存在算法确定合式公式为公理,是很有价值的。

如果存在生成所有公理的算法,则公理的集合被称为递归可枚举的。

如果存在算法在有限步骤后确定一个公式是否是公理,则公理的集合被称为递归的或“可判定的”。在这种情况下,你还可以构造一个算法来生成所有的公理:这个算法简单的(随着长度增长)一个接一个的生成所有可能的公式,而算法对每个公式确定它是否是个公理。

一阶逻辑的公理总是可判定的。但是在一阶理论中非逻辑公式就不必需如此。

量词公理[编辑]

下列四个公理是谓词演算的特征:

  • PRED-1:  \forall x Z(x) \rightarrow Z(t)
  • PRED-2:  Z(t) \rightarrow \exists x Z(x)
  • PRED-3:  \forall x (W \rightarrow Z(x)) \rightarrow (W \rightarrow \forall x Z(x))
  • PRED-4:  \forall x (Z(x) \rightarrow W) \rightarrow (\exists x Z(x) \rightarrow W)

它们实际上是公理模式:表达式W表示对于其中任何wff,x不是自由的;而表达式Z(x)表示对于任何wff带有额外的约定,即Z(t)表示把Z(x)中的所有x替代为项t的结果。

等式和它的公理[编辑]

在一阶逻辑中对使用等式(或恒等式)有多种不同的约定。本节总结其中主要的。不同的约定对同样的工作给出本质上相同的结果,区别主要在术语上。

  • 对等式的最常见的约定是把等号包括为基本逻辑符号,并向一阶逻辑增加等式的公理。等式公理是
x = x
x = yf(...,x,...) = f(...,y,...)对于任何函数f
x = y →(P(...,x,...) → P(...,y,...))对于任何关系P(包括 = 自身)
  • 其次常见的约定是把等号包括为理论的关系之一,并向这个理论的公理增加等式的公理。在实际中这是同前面约定最难分辨的,除了在没有等式概念的不常见情况下。公理是一样的,唯一的区别是把它叫做逻辑公理还是这个理论的公理。
  • 在没有函数和有有限数目个关系的理论中,有可能以关系的方式定义等式,通过定义两个项st是相等的,如果任何关系通过把s改变为t 在任何讨论下都没有改变。例如,在带有一个关系∈的集合论中,我们可以定义s = t为∀x (sxtx) ∧ ∀xxsxt)的缩写。这个等式定义接着自动的满足了关于等式的公理。
  • 在某些理论中有可能给出特别的等式定义。例如,在带有一个关系 ≤的偏序的理论中,我们可以定义s = tstts的缩写。

谓词演算[编辑]

谓词演算是命题演算的扩展,它定义了哪些一阶逻辑的陈述是可证明的。它是用来描述数学理论的形式系统。如果命题演算用一组合适的公理和一个单一的推理规则肯定前件来定义(可以有很多不同的方式),则谓词演算可以通过增加一些补充的公理和补充的推理规则"全称普遍化"来定义。更精确地说,谓词演算采用的公理有:

  • 来自命题演算的所有重言式(命题变量被替代为公式)。
  • 上面给出的量词公理。
  • 上面给出的等式公理,如果等式被认为是逻辑概念的话。

一个句子被定义为是在一阶逻辑中可证明的,如果可以通过从谓词演算的公理开始并重复应用推理规则"肯定前件"和"全称普遍化"来得出它。

如果我们有一个理论T(在某些语言中叫做公理的陈述的集合),则一个句子φ被定义为是在理论T中可证明的,如果

ab ∧ ... → φ

在一阶逻辑中对于理论T的某个公理a, b,...的有限集合是可证明的。

可证明性的一个明显问题是它好像非常特别:我们采用了显然随机的公理和推理规则的搜集,不清楚是否意外的漏掉了某个关键的公理或规则。哥德尔完备性定理确保这实际上不是问题:这个定理声称在所有模型中为真的任何陈述在一阶逻辑中都是可证明的。特别是,在一阶逻辑中"可证明性"的任何合理定义都必须等价于上述定义(尽管在不同的可证明性的定义下证明的长度可能有巨大差别)。

有很多不同(但等价)的方式来定义可证明性。前面的演算是"希尔伯特风格"演算的一个典型例子,它有许多不同的公理但只有非常少的推理规则。"根岑风格"谓词演算有非常少的公理但有许多推理规则。

文法上说谓词演算在现存的命题演算上增加了“谓词-主词结构”和量词。主词是给定的个体群组(集合)的一个成员的名字,而谓词是在这个群组上的关系,一元谓词在哲学中称为性质,在数学中称为指示函数,在数理逻辑中称为布尔值函数

可证明的恒等式[编辑]

\neg \forall x P(x) \Leftrightarrow \exists x \neg P(x)
\neg \exists x P(x) \Leftrightarrow \forall x \neg P(x)
\forall x \forall y P(x,y) \Leftrightarrow \forall y \forall x P(x,y)
\exists x \exists y P(x,y) \Leftrightarrow \exists y \exists x P(x,y)
\forall x P(x) \land \forall x Q(x) \Leftrightarrow \forall x (P(x) \land Q(x))
\exists x P(x) \lor \exists x Q(x) \Leftrightarrow \exists x (P(x) \lor Q(x))

可能增加的推理规则[编辑]

\exists x \forall y P(x,y) \Rightarrow \forall y \exists x P(x,y)
\forall x P(x) \lor \forall x Q(x) \Rightarrow \forall x (P(x) \lor Q(x))
\exists x (P(x) \land Q(x)) \Rightarrow \exists x P(x) \land \exists x Q(x)
\exists x P(x) \land \forall x Q(x) \Rightarrow \exists x (P(x) \land Q(x))

一阶逻辑的元逻辑定理[编辑]

下面列出了一些重要的元逻辑定理。

  1. 不像命题演算,一阶逻辑是不可判定性的。对于任意的公式P,可以证实没有判定过程,判定P是否有效,(参见停机问题)。(结论独立的来自于邱奇图灵。)
  2. 有效性的判定问题是半可判定的。按哥德尔完备性定理所展示的,对于任何有效的公式P, P是可证明的。
  3. 一元谓词逻辑(就是说,谓词只有一个参数的谓词逻辑)是可判定的。

转换自然语言到一阶逻辑[编辑]

用自然语言表达的概念必须在一阶逻辑(FOL)可以为为其效力之前必须被转换到FOL,而在这种转换中可能有一些潜在的缺陷。在FOL中,p \or q意味着“要么p要么q要么二者”,就是说它是“包容性”的。在英语中,单词“or”有时是包容性的(比如,“加牛奶或糖?”),有时是排斥性的(比如,“喝咖啡或茶?”,通常意味着取其中一个或另一个但非二者)。类似的,英语单词“some”可以意味着“至少一个,可能全部”,有时意味着“不是全部,可能没有”。英语单词“and”有时要按“or”转换(比如,“男人和女人可以申请”)。 [4]

一阶逻辑的限制[编辑]

所有数学概念都有它的强项和弱点;下面列出一阶逻辑的一些问题。

难于表达if-then-else[编辑]

带有等式的FOL不包含或允许定义if-then-else谓词或函数if(c,a,b),这裡的c是表达为公式的条件,而a和b是要么都是项要么都是公式,并且它的结果是a如果c为真,或者b如果它为假。问题在于FOL中,谓词和函数二者只接受(“非布尔类型”)项作为参数,而条件的明确表达是(“布尔类型”)公式。这是不幸的,因为很多数学函数是依据if-then-else而方便的表达的,而if-then-else是描述大多数计算机程序的基础。

在数学上,有可能重定义匹配公式算子的新函数的完备集合,但是这是非常笨拙的。[5] 谓词if(c,a,b)如果重写为(c \wedge a) \or (\neg c \wedge b)就可以在FOL中表达,但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况谓词叫做“if(条件,a, b)”(这里a和b是公式)和/或函数“ite(条件,a, b)”(这裡的a和b是项),它们都接受一个公式作为条件,并且等于a如果条件为真,或b如果条件为假。这些扩展使FOL易于用于某些问题,并使某类自动定理证明更容易。[6] 其他人进一步扩展FOL使得函数和谓词可以在任何位置接受项和公式二者。

类型(种类)[编辑]

除了在公式(“布尔类型”)和项(“非布尔类型”)之间的区别之外,FOL不包括类型(种类)到自身的概念中。 某些人争辩说缺乏类型是巨大优点 [7],而很多其他人发觉了定义和使用类型(种类)的优点,比如帮助拒绝某些错误或不想要的规定 [8]。 想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂,并也容易导致错误。

单一参数谓词可以用来在合适的地方实现类型的概念。例如:

\forall x (Man(x) \rightarrow Mortal(x))

谓词Man(x)可以被认为是一类“类型断言”(就是说,x必须是男人)。 谓词还可以同指示类型的“存在”量词一起使用,但这通常应当转而与逻辑合取算子一起来做,比如:

\exists x (Man(x) \wedge Mortal(x))(“存在既是男人又是人类的事物”)。

容易写成\exists x Man(x) \rightarrow Mortal(x),但这将等价与\exists x \neg Man(x) \or \exists x Mortal(x)(“存在不是男人的事物或者存在是人类的事物”),这通常不是想要的。类似的,可以做一个类型是另一个类型的子类型的断言,比如:

\forall x (Man(x) \rightarrow Mammal(x))(“对于所有x,如果x是男人,则x是哺乳动物)。

难于刻画有限性或可数性[编辑]

Löwenheim–Skolem定理得出在一阶逻辑中不可能刻画有限性或可数性。例如,在一阶逻辑中你不能断言实数的集合的上确界性质,它声称实数的所有有界的、非空集合都有上确界;这就需要二阶逻辑了。

图可及性不能表达[编辑]

很多情况可以被建模为节点和有向连接(边)的。例如,效验很多系统要求展示不能从“好”状态触及到“坏”状态,而状态的相互连接经常可以建模为图。但是,可以证明这种可及性不能用谓词逻辑完全表达。换句话说,没有谓词逻辑公式f,带有u和v作为它的唯一自由变量,而R作为它唯一的(2元)谓词符号,使得f在一个有向图中成立,如果在这个图中存在从关联于u的节点到关联于v的节点的路径。[9]

参考文献[编辑]

引用[编辑]

  1. ^ Mendelson, Elliott. Introduction to Mathematical Logic. Van Nostrand Reinhold. 1964: 56. 
  2. ^ The SMT-LIB Standard: Version 2.0, by Clark Barrett, Aaron Stump, and Cesare Tinelli. http://goedel.cs.uiowa.edu/smtlib/
  3. ^ For another well-worked example, see Metamath proof explorer
  4. ^ Suber, Peter, Translation Tips, [2007-09-20] 
  5. ^ Otter Example if.in, [2007-09-21] 
  6. ^ Manna, Zohar, Mathematical Theory of Computation, McGraw-Hill Computer Science Series, New York, New York: McGraw-Hill Book Company, 77–147, 1974, ISBN 0-07-039910-7 
  7. ^ Leslie Lamport, Lawrence C. Paulson. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems. 1998. http://citeseer.ist.psu.edu/71125.html
  8. ^ Rushby, John. Subtypes for Specification. 1997. Proceedings of the Sixth European Software Engineering Conference (ESEC/FSE 97). http://citeseer.ist.psu.edu/328947.html
  9. ^ Huth, Michael; Ryan, Mark, Logic in Computer Science, 2nd edition, 138–139, 2004, ISBN 0-521-54310-X 

书目[编辑]

外部链接[编辑]

参见[编辑]