量化 (數理邏輯)

在語言和邏輯中，量化是用量詞指定一個謂詞的有效性的廣度的構造，就是說指定謂詞在一定範圍的事物上成立的程度。產生量化的語言元素叫做量詞。結果的句子是量化的句子，我們稱我們已經量化了這個謂詞。量化在自然語言和形式語言中都使用。在自然語言中，量詞的例子有「所有」、「某些」；「很多」、「少量」、「大量」也是量詞。在形式語言中，量化是從舊公式產生新公式的公式構造子（constructor）。語言的語義指定了如何把這個構造子解釋為一個有效性的廣度。量化是變量約束操作的實例。

在謂詞邏輯的兩類基本量化是全稱量化和存在量化。這些概念被更詳細的敘述於在單獨文章中；下面我們討論適用於二者的特徵。其他種類的量化包括唯一量化。

自然語言中的量化

所有已知人類語言都使用量化，即使是那些沒有完整的數字系統的語言（Wiese 2004）。例如：

• 「我最近訂的所有玻璃都碎了」。
• 「站在河邊的一些人帶著白臂章」。
• 「我交談的多數人都沒有從屬的俱樂部」。
• 「在候診室里的所有人都對Ballyhoo醫生有至少一個抱怨」。
• 「在他的班級中有些人能夠正確的回答我提出的所有問題」。
• 「大量的人是聰明的」。

不存在簡單的方式把這些表達重新公式化為句子們的合取或析取，它們每個都有個體的簡單謂詞如「酒杯碎了」。這些例子也暗示了在自然語言中的量化表達式構造可以是語法上非常複雜的。幸運的是，對於數學斷言，量化過程在語法上是更加直接的。

研究自然語言中的量化比研究形式語言的量化要難很多。這部分的由於自然語言句子的文法結構可能隱藏了邏輯結構的事實。而數學約定嚴格的為形式語言量詞指定了有效範圍；為自然語言指定有效性的範圍要求處理不平凡的語義問題。

Montague文法給出了新穎的自然語言的形式語義。它提起爭論說它比弗雷格、羅素和蒯因的傳統處理更加自然的對自然語言的形式化表現。

數學論斷中的量詞

我們開始討論在非正式數學討論中的量化。考慮下列陳述

1·2 = 1 + 1，且2·2 = 2 + 2，且3 · 2 = 3 + 3，....，且n · 2 = n + n等等。在外觀上這是命題的無限合取。從形式語言的觀點看這立即是一個問題，因為我們希望語法規則生成有限個對象。把這個缺陷放到一邊，還要注意在這個例子中我們幸運的有一個生成所有結合項（conjunct）的過程。但是，如果我們想要斷言關於無理數的某個事物，我們沒有辦法枚舉所有結合項，因為無理數不能被枚舉。避免這些問題的一個簡潔的公式化是使用全稱量化：

對於任何自然數n, n·2 = n + n。類似的分析適用於析取，

1是素數，或2是素數，或3是素數等等。它可以使用存在量化重組：

對於某些自然數n, n是素數。

量詞的嵌套

考慮下列語句：

對於任何自然數n，有一個自然數s使得s = n×n。這明顯是真的；它只是斷言了所有自然數都有一個平方。

下面這個斷言中的量詞的意義就非常不同了：

有一個自然數s使得對於所有自然數n，有s = n×n。這明顯是假的；它斷言了有一個單一的自然數是s是所有自然數的平方。

這展示了量詞嵌套的時候的基本要點：量詞間隔的次序是絕對重要的。不平常些的例子是來自數學分析的一致連續的概念，只是通過對換了兩個量詞的位置，它就不同於更加熟悉的逐點連續的概念。

量詞的範圍

每個量詞都涉及一個特定的變量和這個變量的論域或「量化範圍」。量化的範圍指定這個變量採用的值的集合。在上面的例子中，量化的範圍是自然數的集合。量化範圍的指定允許我們表達出，在斷言一個謂詞對某些自然數成立和對某些實數成立之間的區別。說明性的約定經常保留某些變量名字，比如n保留給自然數，x保留給實數，儘管依賴於命名約定一般不能工作，因為變量的範圍在數學論證過程中是可以變更的。

限制論域的更自然的方式是使用「監控量化」。例如：

對於某些自然數n，n是偶數且n是素數。意味著

對於某些偶數n，n是素數。

早某些數學理論中你可以預先假定一個固定的單一論域。例如，在Zermelo Fraenkel集合論中，變量範圍是在所有集合之上。在這種情況下，可以監控量詞來模擬更小的量化範圍。如上述例子中

對於所有自然數n，n·2 = n + n

在Zermelo-Fraenkel集合論中，你可以說

對於任意n，如果n屬於N，則n·2 = n + n，這裡的N是所有自然數的集合。

量詞的記號

全稱量詞的傳統符號是∀，它倒過來的字母A，表示單詞「all」。存在量詞的相應的符號是∃，它是反過來的字母E，表示單詞「exists」。相應的量化表達式構造如下：

$\exists {n}\,P\quad \forall {n}\,P$

這裡的P指示一個公式。有很多變體被使用了，比如

$\exists {n}\,P\quad (\exists {n})P\quad \exists {n}(P)\quad \exists _{n}\,P\quad \exists {n}{,}\,P\quad \exists {n}{:}\,P\quad \exists {n}{\in }\mathbb {N} \,P\quad \exists \,n\in \mathbb {N} {,}\,P\quad \exists {n}{:}\mathrm {uint} \,P$

所有這些變體都同樣適用於全稱量化和存在量化。

二十世紀早期的文獻不使用∀符號。典型的記號是用（x）P來表達"對於所有的x，P"和"（∃x）P"表示"存在x使得P"。∃符號是皮亞諾在1890年左右提出的。後在，在1930年左右，Gerhard Gentzen介入了∀符號來表示全稱量化。弗雷格的《概念文字》使用完全不同記號，它根本就不包括存在量詞；∃x:P總是用概念文字表達為等價的¬∀x:¬P。

注意某些版本的記號明確的提及了量詞的範圍。量詞的範圍總是必須指定，但是對於給定的數學理論，可以用多種方式來做：

• 為每個量詞假定一個固定的論域，比如Zermelo Fraenkel集合論，
• 預先固定多個論域並要求每個變量有一個聲明了域，它就是這個變量的類型。這類似於強類型的計算機編程語言，那裡的變量有聲明過的類型。
• 明確的提及量化的範圍，可能使用在這個域中所有對象的集合或在這個域中對象的類型符號。

在不發生變量捕獲的限制條件下，可以使用任何變量作為量化變量，替代任何其他變量。即使這種記號使用了有類型的變量，你仍可以使用這種類型的任何變量。變量捕獲的問題是極其重要的，並在下面的形式語義章節中討論。

非正式地，"∀x"或"∃x"也可以出現在P（x）之後，甚至在P（x）的中間，如果它是個長短語的話。正式而言，介入虛擬變量的短語在標準上要位於前面。

注意數學公式混合了量詞的符號表達和自然語言量詞，比如：

對於任何自然數x, ....

存在一個x使得....

對於至少一個x....

唯一量化的關鍵字包括：

對於正好一個自然數x, ....

有一個且只有一個x使得....

你使用代名詞來避免變量名字如x。例如：

對於任何自然數，它乘以2等於它加以自身

某些自然數是素數。

形式語義

數理語義是用形式化的數學上的特定語言表達的研究意義的數學應用。它有三個要素：通過語法的一類對象的數學規定，各種語義域的數學規定，和在二者之間的關係，它通常表達為從語法對象到語義對象的函數。在本文中，我們只致力於描述量詞元素如何解釋的問題。

在本文中，我們只考慮帶有函數符號的一階邏輯。我們建議讀者看模型論的文章獲得關於在這個邏輯框架內公式釋義的更詳細信息。公式的語法可以用語法樹給出。量詞有範圍，而變量x是自由的，如果它不在這個變量的量化範圍內。所以在

$\forall x(\exists yB(x,y))\vee C(y,x)$

中，x和y二者在C（y,x）中的出現是自由的。

展示範圍和變量捕獲的語法樹

一階謂詞演算的釋義假定給出一個個體域X。自由變量是x₁, ..., x_n的一個公式A被解釋為n個參數的一個布爾值函數F（v₁, ..., v_n），這裡的每個參數都定範圍在域X上。布爾值意味著這個函數採用值T（解釋為真）或F（解釋為假）中的一個。公式

$\forall x_{n}A(x_{1},\ldots ,x_{n})$

的釋義是n-1個參數的函數G，使得G（v₁, ...,v_n-1） = T，若且唯若對於在X中所的w有F（v₁, ..., v_n-1, w） = T。如果對於至少w的一個值，有F（v₁, ..., v_n-1, w） = F，則G（v₁, ..,v_n-1） = F。類似的，公式

$\exists x_{n}A(x_{1},\ldots ,x_{n})$

的釋義為n-1個參數的函數H，使得H（v₁, ...,v_n-1） = T，若且唯若對於至少一個w有F（v₁, ...,v_n-1, w） = T，否則H（v₁, ..., v_n-1） = F。

唯一量化的語義要求帶有等號的一階謂詞演算。這意味著這裡要有一個顯著的二元謂詞"="；語義也要相應的修改來使"="總是被解釋為在X上的二元等價關係。

$\exists !x_{n}A(x_{1},\ldots ,x_{n})$

被解釋為n-1個參數的函數，它是如下兩個釋義的邏輯與

$\exists x_{n}A(x_{1},\ldots ,x_{n})$

$\forall y,z\left\{A(x_{1},\ldots ,x_{n-1},y)\wedge A(x_{1},\ldots ,x_{n-1},z)\implies y=z\right\}$

幾個、多個和其他程度的量詞

我們只考慮了在數學中的全稱、存在和唯一量化。它們都不能用來量化如下

• 今晚在舞場有很多舞女。

儘管在本文中我們沒有考慮自然語言的語義，我們將嘗試用如下類型的自然語言為斷言提供語義

• 有很多n < 100的整數，使得n能被2或3或5整除。

一種可能的解釋機制可以獲得如下：假設除了語義域X之外，我們還給出在X上定義一個概率測度P和截斷數0 < a ≤ b ≤ 1。如果A是帶有自由變量x₁,...,x_n的公式，它的釋義是變量v₁,...,v_nthe的函數F，則

$\exists ^{\mathrm {many} }x_{n}A(x_{1},\ldots ,x_{n-1},x_{n})$

的釋義是v₁,...,v_n-1的函數，它是T若且唯若

$\operatorname {P} \{w:F(v_{1},\ldots ,v_{n-1},w)=\mathbf {T} \}\geq b$

，否則是F。類似的，

$\exists ^{\mathrm {few} }x_{n}A(x_{1},\ldots ,x_{n-1},x_{n})$

的釋義是v₁,...,v_n-1的函數，它是T若且唯若

$0<\operatorname {P} \{w:F(v_{1},\ldots ,v_{n-1},w)=\mathbf {T} \}\leq a$

，否則是F。我們已經完全避免了關於釋義函數的測度性的技術問題的討論；其中某些技術問題要求Fubini定理。

我們還要警告讀者這種語義相應的邏輯是非常複雜的。

形式化的歷史

在形式邏輯中的量化的第一個基於變量的處理直到19世紀才出現，儘管詞項邏輯以同在自然語言很緊密的方式處理量化，但不適合於形式分析。亞里斯多德邏輯在公元前1世紀給出了「所有」、「某些」和「沒有」量詞和對真勢模態的處理。

第一個基於變量的邏輯處理是弗雷格的《概念文字》，緊隨在查爾斯·皮爾士獨立的公式化了存在圖之後。弗雷格的方法被證明更有影響，因為它被皮亞諾接受，儘管Pierce的邏輯最近更加引起邏輯學家對異類推理和圖表推理的興趣。

量化的第一個嚴格的表示法出現在弗雷格的《概念文字》。弗雷格使用在變量名下劃的曲線來指示在它隨後的公式中這個變量是被全稱量化的。弗雷格沒有給存在量化特殊的記號，而是使用等價的$\sim \forall x:\sim \ldots$。

在懷特海和羅素的《數學原理》中，弗雷格的記號被簡化了。使用公式「$(x)\phi$」來指示這個公式φ對於x的所有的值都是真的。存在量化被寫為「$(\exists x)\phi$」；∃符號自身是皮亞諾在1897年首次使用的。

∀符號是後來發明的，它是格哈德·根岑在1935年模仿皮亞諾的∃符號而發明。

參見

• 自由變量和約束變量
• 句子 (數理邏輯)

引用

• Jon Barwise and John Etchemendy, 2000. Language Proof and Logic. CSLI (University of Chicago Press) and New York: Seven Bridges Press. A gentle introduction to first-order logic by two first-rate logicians.
• Crosby, Alfred W.（1996）The Measure of Reality: Quantification and Western Society, 1250-1600. Cambridge University Press.
• Gottlob Frege, 1879. Begriffsschrift. Translated in Jean van Heijenoort, 1967. From Frege to Godel: A Source Book on Mathematical Logic, 1879-1931. Harvard Univ. Press. The first appearance of quantification.
• David Hilbert and Wilhelm Ackermann, 1950 (1928). Principles of Theoretical Logic. Chelsea. Translation of Grundzüge der theoretischen Logik. Springer-Verlag. The 1928 first edition is the first time quantification was consciously employed in the now-standar manner, namely as binding variables ranging over some fixed domain of discourse. This is the defining aspect of first-order logic.
• Charles Peirce, 1885, "On the Algebra of Logic: A Contribution to the Philosophy of Notation, American Journal of Mathematics 7: 180-202. Reprinted in Kloesel, N. et al, eds., 1993. Writings of C. S. Peirce, Vol. 5. Indiana Univ. Press. The first appearance of quantification in anything like its present form.
• Hans Reichenbach, 1975 (1947). Elements of Symbolic Logic, Dover Publications. The quantifiers are discussed in chapters §18 "Binding of variables" through §30 "Derivations from Synthetic Premises".
• Wiese, 2003. Numbers, language, and the human mind. Cambridge University Press. ISBN 0-521-83182-2.
• Westerstahl, Dag, 2001, "Quantifiers," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.

外部連結

• http://www.stanford.edu/group/nasslli/courses/peters-wes/PWbookdraft2-3.pdf （頁面存檔備份，存於網際網路檔案館）