查看“︁量化 (数理逻辑)”︁的源代码

在[[语言]]和[[逻辑]]中，'''量化'''是用量词指定一个[[谓词]]的有效性的广度的构造，就是说指定谓词在一定范围的事物上成立的程度。产生量化的语言元素叫做'''量词'''。结果的[[句子]]是量化的句子，我们称我们已经量化了这个谓词。量化在[[自然语言]]和[[形式语言]]中都使用。在自然语言中，量词的例子有“所有”、“某些”；“很多”、“少量”、“大量”也是量词。在[[形式]]语言中，量化是从旧[[公式]]产生新公式的[[公式构造子]]（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公理|Zermelo Fraenkel]]集合论中，变量范围是在所有[[集合 (数学)|集合]]之上。在这种情况下，可以监控量词来模拟更小的量化范围。如上述例子中
:对于所有自然数''n''，''n''·2 = ''n'' + ''n''
在Zermelo-Fraenkel集合论中，你可以说
:对于任意''n''，如果''n''属于'''N'''，则''n''·2 = ''n'' + ''n''，这里的'''N'''是所有自然数的集合。

== 量词的记号 ==
全称量词的传统符号是∀，它倒过来的字母[[A]]，表示单词“all”。存在量词的相应的符号是∃，它是反过来的字母[[E]]，表示单词“exists”。相应的量化表达式构造如下：
: <math> \exists{n}\, P  \quad \forall{n}\, P </math>
这里的''P''指示一个公式。有很多变体被使用了，比如
: <math> \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  </math>
所有这些变体都同样适用于全称量化和存在量化。

二十世纪早期的文献不使用∀符号。典型的记号是用（''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''是自由的，如果它不在这个变量的量化范围内。所以在
:<math> \forall x(\exists y  B(x,y)) \vee C(y,x)</math>
中，''x''和''y''二者在''C''（''y'',''x''）中的出现是自由的。

[[File:IMG_Tree.gif|thumb|323px|left|展示范围和变量捕获的语法树]]
一阶谓词演算的释义假定给出一个个体域''X''。自由变量是''x''<sub>1</sub>, ..., ''x''<sub>n</sub>的一个公式''A''被解释为''n''个参数的一个[[布尔值函数]]''F''（''v''<sub>1</sub>, ..., ''v''<sub>''n''</sub>），这里的每个参数都定范围在域''X''上。布尔值意味着这个函数采用值'''T'''（解释为真）或'''F'''（解释为假）中的一个。公式
:<math> \forall x_n A(x_1, \ldots , x_n)</math> 
的释义是''n''-1个参数的函数''G''，使得''G''（''v''<sub>1</sub>, ...,''v''<sub>''n''-1</sub>） = '''T'''，当且仅当对于在''X''中所的''w''有''F''（''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>, ''w''） = '''T'''。如果对于至少''w''的一个值，有''F''（''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>, ''w''） = '''F'''，则''G''（''v''<sub>1</sub>, ..,''v''<sub>''n''-1</sub>） = '''F'''。类似的，公式
:<math> \exists x_n A(x_1, \ldots , x_n)</math> 
的释义为''n''-1个参数的函数''H''，使得''H''（''v''<sub>1</sub>, ...,''v''<sub>''n''-1</sub>） = '''T'''，当且仅当对于至少一个''w''有''F''（''v''<sub>1</sub>, ...,''v''<sub>''n''-1</sub>, ''w''） = '''T'''，否则''H''（''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>） = '''F'''。

[[唯一量化]]的语义要求带有等号的一阶谓词演算。这意味着这里要有一个显著的二元谓词"="；语义也要相应的修改来使"="总是被解释为在''X''上的二元等价关系。
:<math> \exists !   x_n A(x_1, \ldots , x_n)</math> 
被解释为''n''-1个参数的函数，它是如下两个释义的逻辑''与'' 
:<math> \exists  x_n A(x_1, \ldots , x_n)</math> 
:<math> \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\}</math>

== 几个、多个和其他程度的量词 ==

我们只考虑了在数学中的全称、存在和唯一量化。它们都不能用来量化如下 

* 今晚在舞场有很多舞女。

尽管在本文中我们没有考虑自然语言的语义，我们将尝试用如下类型的自然语言为断言提供语义

* 有很多''n'' < 100的整数，使得''n''能被2或3或5整除。

一种可能的解释机制可以获得如下：假设除了语义域''X''之外，我们还给出在''X''上定义一个[[概率测度]]P和截断数0 < ''a'' ≤ ''b'' ≤  1。如果''A''是带有自由变量''x''<sub>1</sub>,...,''x''<sub>''n''</sub>的公式，它的释义是变量''v''<sub>1</sub>,...,''v''<sub>''n''</sub>the的函数''F''，则
:<math> \exists^{\mathrm{many}} x_n A(x_1, \ldots, x_{n-1}, x_n)</math>
的释义是''v''<sub>1</sub>,...,''v''<sub>''n''-1</sub>的函数，它是'''T'''当且仅当
:<math> \operatorname{P} \{w: F(v_1, \ldots, v_{n-1}, w) = \mathbf{T} \} \geq b </math>
，否则是'''F'''。类似的，
:<math> \exists^{\mathrm{few}}  x_n  A(x_1, \ldots, x_{n-1}, x_n)</math>
的释义是''v''<sub>1</sub>,...,''v''<sub>''n''-1</sub>的函数，它是'''T'''当且仅当
:<math> 0< \operatorname{P} \{w: F(v_1, \ldots, v_{n-1}, w) = \mathbf{T}\} \leq a </math>
，否则是'''F'''。我们已经完全避免了关于释义函数的[[测度性]]的技术问题的讨论；其中某些技术问题要求[[Fubini定理]]。

我们还要警告读者这种语义相应的''逻辑''是非常复杂的。

== 形式化的历史 ==

在[[形式逻辑]]中的量化的第一个基于变量的处理直到19世纪才出现，尽管[[词项逻辑]]以同在自然语言很紧密的方式处理量化，但不适合于形式分析。[[亚里士多德]]逻辑在公元前1世纪给出了“所有”、“某些”和“没有”量词和对[[真势模态]]的处理。

第一个基于变量的逻辑处理是[[弗雷格]]的《[[概念文字]]》，紧随在[[查尔斯·皮尔士]]独立的公式化了[[存在图]]之后。弗雷格的方法被证明更有影响，因为它被[[皮亚诺]]接受，尽管Pierce的逻辑最近更加引起逻辑学家对[[异类推理]]和[[图表推理]]的兴趣。

量化的第一个严格的表示法出现在[[弗雷格]]的《[[概念文字]]》。弗雷格使用在变量名下划的曲线来指示在它随后的公式中这个变量是被全称量化的。弗雷格没有给存在量化特殊的记号，而是使用等价的<math>\sim\forall x:\sim\ldots</math>。

在[[怀特海]]和[[罗素]]的《[[数学原理]]》中，弗雷格的记号被简化了。使用公式“<math>(x)\phi</math>”来指示这个公式φ对于''x''的所有的值都是真的。存在量化被写为“<math>(\exists x)\phi</math>”；∃符号自身是[[皮亚诺]]在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 {{Wayback|url=http://www.stanford.edu/group/nasslli/courses/peters-wes/PWbookdraft2-3.pdf |date=20120716183245 }}

{{数理逻辑}}
{{形式謬誤}}
[[Category:數理邏輯|L]]