一阶逻辑是使用于数学、哲学、语言学及电脑科学中的一种形式系统，也可以称为：一阶断言演算、低阶断言演算、量化理论或谓词逻辑。一阶逻辑和命题逻辑的不同之处在于，一阶逻辑包含量词。 高阶逻辑和一阶逻辑不同之处在于，高阶逻辑的断言符号可以有断言符号或函数符号当做引数，且容许断言量词或函数量词。在一阶逻辑的语义中，断言被解释为关系。而高阶逻辑的语义里，断言则会被解释为集合的集合。 在通常的语义下，一阶逻辑是可靠（所有可证的叙述皆为真）且完备（所有为真的叙述皆可证）的。虽然一阶逻辑的逻辑归结只是半可判定性的，但还是有许多用于一阶逻辑上的自动定理证明。一阶逻辑也符合一些使其能通过证明论分析的元逻辑定理，如勒文海姆–斯科伦定理及紧致性定理。 一阶逻辑是数学基础中很重要的一部份。许多常见的公理系统，如一阶皮亚诺公理、冯诺伊曼-博内斯-哥德尔集合论和策梅洛-弗兰克尔集合论都是一阶理论。然而一阶逻辑不能控制其无穷模型的基数大小，因根据勒文海姆–斯科伦定理和康托尔定理，可以构造出一种“病态”集合论模型，使整个模型可数，但模型内却会觉得自己有「不可数集」。类似地，可以证明实数系的普通一阶理论既有可数模型又有不可数模型。这类的悖论被称为斯科伦悖论。但一阶的直觉主义逻辑里，勒文海姆–斯科伦定理不可证明，故不会有以上之现象。 简介. 在命题逻辑里，「苏格拉底是哲学家」、「柏拉图是哲学家」只能简单标记为 formula_1 及 formula_2 。 而一阶逻辑先设符号 formula_3 意为 「 "x" 是哲学家」，然后以 formula_4 代表苏格拉底、 formula_5 代表柏拉图，则 formula_6 对应 formula_1 ； formula_8 对应 formula_2 。也就是赋予断言符号「formula_3 」语意的解释。这个解释预设一个「所有人类的群体」（也就是语义解释的论域），并将变数 formula_11 解释为自群体中取出来的某人。 断言符号可以包含一个以上的变数。例如：设 formula_12 意为「 x 与 y 是夫妻」，则 formula_13 意为「苏格拉底和 "y" 是夫妻」。 一阶逻辑和命题逻辑相同，断言符号和变数还能与逻辑符号组成更复杂的叙述。例如：设断言符号 formula_14 意为 formula_11 是学者。则「若 "x" 为哲学家，则 "x" 为学者」可表示为： formula_16 而「对所有 "x" ，若 "x" 为哲学家，则 "x" 为学者」则记为： formula_17 也就是自左方开始阅读，以 formula_18 表示「对于所有 "x" 」，可以将之理解为「对于所有 "x" ， formula_18 右方的叙述为真。」其中，formula_18 这个符号被称为 formula_11 的全称量词。 直观上有「若所有"x"是哲学家，那"x"的长子也会是哲学家」这样“合理”的叙述。若设 formula_22 意为 「 "x" 的长子」，那么这段“合理”叙述可记为： formula_23 formula_24 表示“与 formula_11 有唯一对应的那个对象”，被称为函数符号。这段直观为真的叙述，经过适当的扩展以后就是一阶逻辑其中的一条公理。 而对于「有 "x" 是哲学家」这一叙述，则引入另一种量词表记为： formula_26 自左方开始阅读，以 formula_27 代表「存在 "x" 」，可以将之理解为「有 "x" 使 formula_27 右方的叙述为真」。其中，formula_27 被称为 formula_11 的存在量词。全称量词和存在量词一起被简称为量词。 直观上，「并非所有 "x" 不是哲学家」，和「有 "x" 是哲学家」是等价的；且「不存在 "x" 不是学者」也与「所有的 "x" 是学者」等价。所以只要有「否定」这个逻辑概念，那么一阶逻辑就能以全称量词为基础，作以下的符号定义（ formula_31 解释为 「否定」， 而 formula_32 代表一段＂叙述＂）： formula_33 由此，存在量词被定义为全称量词的衍伸。 形式理论. 一阶逻辑的形式理论可分成几个部份： 基本符号. 一套理论能容许多少符号，取决于人类能运用物理定律来塑造多少符号，但目前无法确知宇宙是不是有限，或是以可无限制地分割。虽然所有的公理化集合论都以量词的形式隐晦的承认跟自然数一样多的无穷（如ZF集合论的无穷公理），甚至以这样的可数无穷为基础，去建构出不可数的实数，但将抽象的理论对应到现实时，还是需要回答物理上有没有可数或不可数的无穷。所以谨慎起见，如果没有特别申明的话，以下各种类符号的数目上限都是有限的。 逻辑符号. 一阶逻辑通常拥有以下的符号： 并非所有的符号都不可或缺的，像谢费尔竖线「formula_54」（或异或）可以用来定义量词以外的所有逻辑符号，换句话说： 另外，一些作者不区分语义解释和形式理论，所以会将表示真值的符号纳入形式理论里，也就是说，用 T 、V"pq" 或 formula_55 来表示「真」，并用 F 、 O"pq" 或 formula_56 来表示「假」。 断言符号. 「他们两人是夫妻」，是一个关于两个“对象”的断言，而「他是人」、「三点共线」则表明断言容许一个或者多个对象。所以对于自然数 formula_57 、formula_58 约定： formula_59 为一阶逻辑的合法词汇。它在直观上表示一个有 formula_57 个“对象”的断言，称为 formula_57 元断言符号。下标的自然数 formula_58 只是拿来和其他同为 formula_57 元的断言符号作区别。 实用上只要有申明，不至于和其他词汇引起混淆的话，可以用任意的形式简写一个断言符号。如：公理化集合论里的双元断言符号 formula_64 也可以表示为 formula_65 。 函数符号. 「物体的颜色」、「夫妻的长子」这种断言说明了一组对象所唯一对应的对象。但不同的夫妻有不同的长子；不同的物体有不同的颜色。据此，形式上对于自然数 formula_57 、formula_58 约定： formula_68 为一阶逻辑的合法词汇，直观上表示 formula_57 个“对象”所对应到的东西，称它为 formula_57 元函数符号。需要特别注意，这种“唯一对应”的直观想法，必须配上关于“等式”的性质（详见下面的等式定理章节），才能在形式理论中被实现。 与断言符号一样，只要不引起混淆，就可以用任何的形式简写函数符号。如：公理化集合论里的 formula_71 是依据联集公理而定义的新函数符号（请参见下面函数符号与唯一性章节），也可以冗长的表记为 formula_72 。 常数符号. 「刻度0」、「原点」、「苏格拉底」是直观上＂唯一不变＂的对象。据此，对自然数 formula_58 约定 formula_74 为一阶逻辑的合法词汇，直观上表示一个“唯一不变”的对象，称为常数符号。同样的。“常数的不变性”需配上等式的性质（详见下面等式定理）才能被实现。 为了不和变数的表记混淆，常数符号一样可以用任何的形式简写，如公理化集合论里的 formula_75 是根据空集公理和函数符号与唯一性，而定义的新常数符号。亦可冗长的表示为 formula_74 。 语法. 和自然语言（如英语）不同，一阶逻辑的语言以明确的递回定义判断一个给定的词汇是否合法。大致上来说，一阶逻辑以「项」代表讨论的对象，而对「项」的断言组成了最基本的原子（合式）公式；而原子公式和逻辑符号组成了更复杂的合式公式（也就是“叙述”）。 项. 「那对夫妻的长子的职业」、「formula_77」、「formula_78」代表变数可以与函数符号组成更一般的物件。据此形式，递回地规定一类合法词汇——项为： 习惯上以大写的西方字母（如英文字母、希伯来字母、希腊字母）代表项，如果变数不得不采用大写字母，而可能跟项引起混淆的话，需额外规定分辨的办法。 原子公式. 为了比较简洁地规定甚么是合式公式，先规定原子公式为：（若 formula_79 是项） formula_80 这样的形式。 公式. 一阶逻辑的合式公式（简称公式或 formula_81 ）以下面的规则递回地定义： 另外成对的中括弧跟大括弧，符号辨识上视为成对的小括弧，而草书的大写西方字母为公式的代号。 举例来说， formula_82 是公式而 formula_83 则不是公式。 而接下来只要对任意公式formula_32 、 formula_85 与变数 formula_11，做以下符号定义 这样所有的逻辑连接词与量词就纳入了合式公式的规范。 施用. 所谓的施用/作用，是以下公式形式的口语说法：（其中 formula_32 与 formula_85 都是公式） 就类似于运算子作用在它们身上。 自由变数和约束变数. 量词所施用的公式被称为量词的范围（scope）。同一个变数在公式一般来说不只出现一次，若变数 formula_11 出现在 formula_18 的范围内，称这样出现的 formula_11 为不自由/被约束的 formula_11 （not free/bounded）；反过来说，不出现在 formula_18 的范围内的某个 formula_11 被称为自由的 formula_11。 例如，对于公式： formula_121 formula_122 就是量词 formula_18 的范围；而 formula_124 里的 formula_11 就是不自由的；反之 formula_126 里的 formula_127 就是自由的。 说 formula_11 于公式 formula_32 完全自由，意为于 formula_32 出现的 formula_11 都是自由的；反之，说 formula_11 于公式 formula_32 完全不自由/完全被约束，意为 formula_32 内根本没有 formula_11 ，或是 formula_32 内没有自由的 formula_11 。若 formula_32 内所有的变数都完全不自由，formula_32 特称为封闭公式/句子（closed formula/sentence）。 括弧的简写. 括弧是为了保证语意解释符合预期，但太多的括弧书写不易，为此规定以下的“重构法”（反过来就是“简写法”），从表面上不合法的一串符号找出作者原来想表达的公式： 举例来说 formula_141 的重构过程如下 #formula_142 （优先施用 formula_143） #formula_144 （施用 formula_35） #formula_146 （最后施用 formula_24） 可以被重构为公式的一串符号则宽松的认定为“合式公式”。（最明显的例子就是合式公式最外层的括弧可以省略） 波兰表示法. 波兰表示法将逻辑连接词前置于被施用的公式而非传统的中间。如果沿用以上的＂施用顺序＂，这个表示法允许舍弃所有括弧。如公式 formula_148 转成波兰表示法的过程如下 formula_149 （转成波兰表示法的顺序） formula_150 （逻辑连结词的符号转换） 推理规则. 一阶逻辑通常只有以下的推理规则（因为将普遍化视为推理规则会有不直观的限制） 直观意义非常明显，就是"p"=>"q"且"p"可以推出"q"。 在只以谢费尔竖线「formula_54」为基础逻辑连接词的公理系统里，MP律会被改写成 公理. 逻辑公理. 它们实际上是公理模式，代表著“跟自然数一样多”条的公理。 在有（A1）与（A2）的前提下，（A3）等价于以下的公理模式：（证明请参见下面否定一节。） 另外，在只以谢费尔竖线「formula_54」为基础逻辑连接词的公理系统里，上面三条公理模式等价于下面这条公理模式： 量词公理. 它们实际上也是公理模式。 等式和它的公理. 根据不同作者的看法，甚至是理论本身的需求，「等式」在形式理论里可能是断言符号或是一段公式（如 "a" 等于 "b" 可定义为对所有的 "x" ， "x" 属于 "a" 等价于 "x" 属于 "b" ）。而如何刻划直观上「等式的性质」，有一开始就将「等式的性质」视为公理（模式），但也有视为元定理的另一套处理方法，以下暂且以公理模式的方式处理。以元定理处理的方法会在等式定理详述。 事实上这两个公理模式也确保了函数符号“唯一对应”和常数符号的“唯一性”，但证明这些性质需要一些元定理，简便起见合并于下面的等式定理一节讲述。 标准语义. 一阶逻辑的标准语义源于波兰逻辑学家阿尔弗雷德·塔斯基所著《On the Concept of Truth in Formal Languages》。根据上面语法一节，公式是由原子公式递回地添加逻辑连结词而来的，而原子公式是由断言符号与项所构成的。所以要检验一条公式在特定的论域下正不正确，就要规定项的取值，然后检验这样的取值会不会落在断言符号所对应的关系里。由此延伸出所有公式的“真假值“。 也就是一套一阶逻辑的语义解释，要包含 通常一套解释方法（简称为解释）会以代号 formula_153 表示。 项的取值. 量词的解释需要指明变数取值范围的论域——也就是一个集合 formula_154 。而变数可能跟自然数一样多，换句话说，所有变数在论域 formula_154 取的值可以依序以自然数标下标——也就是一个在 formula_154 取值的数列。如果以 formula_157 的代号（不一定是变数本身的表示符号）来列举变数，那么从 formula_154 的某套变数取值就以 formula_159 或较直观的符号 formula_160 来表示。 一套解释 formula_153 会将 formula_57 元函数符号 formula_163 解释成某个 formula_164 的 formula_57 元函数；而常数符号 formula_166 解释成特定的 formula_167 （亦称为 formula_166 的取值为 formula_169），这样就可以用上面语法一节定义项的方式，递回地规定项的取值： 真假的赋值. 直观上要解释关系最直接的方法，就是列举所有符合关系的对象；例如如果想说明夫妻关系，可以列举所有（老公, 老婆）的双元有序对，但并非所有的人类有序对都会在这个关系中。 以此为基础，若以 formula_170 代表所有以 formula_171 个 formula_154 中的元素构成的 formula_171 元有序对的集合（也就是 formula_171 元笛卡儿积） ，那一套解释 formula_153 会将 formula_171 元断言符号 formula_177 解释为一个 formula_178 的formula_171 元有序对子集合。 这样就可以依据语法的递回定义，以下面的规则对每条公式赋予真值。（这种赋值方式称为T-模式，取名于逻辑学家阿尔弗雷德·塔斯基） 下，formula_180 为真，意为「对所有的 formula_181 ， formula_85 于变数取值 formula_183 下为真」。（也就是把变数 formula_184 的取值换为论域的任意元素仍然为真） 更进一步的来说 代数化语义. 另一种一阶逻辑语义的方法可经由命题逻辑的林登鲍姆-塔斯基代数扩展而成。有如下几种类型： 这些代数都是纯粹扩展两元素布林代数而成的格。 塔斯基和葛范德于1987年证明，没有超过包在三个以上的量化内的原子句子的部份一阶逻辑，其表示力和关系代数相同。上述部份一阶逻辑令人十分地感到有兴趣，因为它已足够表示皮亚诺算术和公理化集合论，包括典型的ZFC。他们亦证明了，具有简单有序对的一阶逻辑和具有两个有序的投影函数的关系代数等价。 空论域. 上述的语义解释都要求论域为非空集合。但在如自由逻辑之中，设定空论域是被允许的。甚至代数结构的类包含一个空结构（如空偏序集），当允许空论域时，这个类只能是一阶逻辑中的一个基本类，不然就要将空结构由类中移除。 不过，空论域存在著一些难点： 因此，若空论域是被允许的，通常也必须被视成特例。不过，大多数的作家会简单地将空论域由定义中排除。 常用的推理性质. 定理与证明. 以下介绍一些基本用语和符号 \mathcal{A} 代表有一列公式 formula_188 满足： *formula_191 为 formula_193 的公理。 *存在 formula_194使得 formula_195 为 formula_196 （也就是由前面的公式以MP律组合出来） 口语上会称公式 formula_32 （或 formula_198 ） 为 formula_193 下的定理（theorem）。而这列formula_188 会称为formula_198 的证明。 例如定理formula_202 formula_203 的证明： 以上其实是蕴含了无限多定理的元定理的证明(因为没有给出合式公式的明确形式)。方便起见，这种元定理还是会称为定理并以同样的形式来表达。 直观上的证明，总是会有一些“前提假设”，对此，若以 formula_204 代表一列有限数目的公式，那 \mathcal{A} 代表有一列公式 formula_188 满足： *formula_191 为 formula_193 的公理。 *formula_191 为 formula_204 中的其中一条公式。 *存在 formula_194使得 formula_195 为 formula_196 （也就是由前面的公式以MP律组合出来） 这样称 formula_188 为在前提 formula_204 下， formula_32 的证明；或是说 formula_32 是 formula_204 的推论结果。 若要特别凸显 formula_204 里的一条＂前提条件＂ formula_85 对＂证明过程＂的重要性，可以用 formula_223 的符号去特别凸显。若 formula_204 里的公式列举出来有 formula_225 ，那亦可表示为 formula_226 证明过程没有被引用的公式尽可能不写出来。另一方面从以上对于证明定义可以发现，依怎样的顺序列举前提条件，对于证明本身是不会有任何影响的。 本节所介绍的符号，在引用哪个理论很显然的情况下，formula_227 的下标formula_193 可以省略。 实际的证明常常会＂引用＂别的（元）定理，严格来说，就是照抄（元）定理的证明过程，然后作一些修改使符号一致。为了节省证明的篇幅，引用时只会单单列出配合引用（元）定理所得出的公式（形式），并在后面注明引用的（元）定理代号。 演绎元定理. 从公理（A1）和（A2）会得出不但直观且实用的演绎元定理： \mathcal{C} ，则有 formula_229 因为 formula_204 代表的是有限条公式，所以透过演绎元定理可以将证明过程必要的前提条件递回地移到 formula_231 后，直到不需要任何前提为止；然后由MP律可以知道，若有 formula_229 ，则有 formula_233，如此一来透过演绎元定理搬到推论结果的合式公式，也可以任意的搬回来。所以 formula_234 等价于某定理 formula_235 。因此也会将 formula_234 称为一个定理。 而从演绎元定理和MP律，会有以下直观且实用的元定理 以下如果需要将引用的定理以演绎元定理进行＂搬移＂，会省略掉搬移的过程并在搬移后得到的结果后标注（D）。如果引用以上的（D1）和（D2）也会省略过程，单有结果和代号标注。 否定. 以下的证明会分成使用（A3）的部分跟将公理（A3）取代为（T1）的部分，用以证明两者的等价性。 上面两定理表达了双否定推理上等价于于原公式，引用两者任一会都以（DN）简写。 注意到（T2）的证明引用了（T1）+（DN），但之前已经证明了（A1）+（A2）+（A3）可以推出（T1）；还有（A1）+（A2）+（T1）也可以推出（DN），所以注明使用（T1）即可。 以上二定理说明 formula_237 推理上等价于 formula_238 ，引用这两个定理中任一都以（T）表示。 至此，已经可以证明（A1）+（A2）+（T1）可以推出（A3）： 所以综合以上所述，在有（A1）+（A2）的前提下，公理（T1）等价于公理（A3）。 由（T）可以得到类似于公理（A3）的定理 实质条件. 以下的定理重现了实质条件的直观理解。 逻辑与和逻辑或. 且与或的交换性. 以下为逻辑与的交换性 类似的，（C2）正是逻辑或的交换性： 且与或的直观意义. ＂且＂的直观意义是实质条件元定理的直接结果 从（AND）和 formula_47 的符号定义可知，formula_240 的证明可以拆成两部分；习惯上会以「（ formula_24 ） 」标示 formula_242 部分的证明，而「（ formula_243 ） 」标示 formula_244 部分的证明。 类似的，＂或＂的直观意义是（M0）跟（D）的直截结果 以下的定理则是（A3'）的直截结果 且与或的结合律. 对于＂且＂，展开符号定义后，可以从直观意义轻松地得到 ＂或＂也有类似的性质 且与或的分配律. ＂且＂和＂或＂之间还有分配律 德摩根定律. 以下的元定理的名字来自于英国逻辑学家奥古斯塔斯·德摩根。 普遍化元定理. 公理模式（A7）可以稍加延伸成以下的元定理 更进一步，有以下元定里 （GEN）可以稍加修饰，以套用在含有存在量词的公式上 等价代换. 以下的定理，说明两条「等价」的公式可以互相代换 这些定理通常是混合使用，以达到「等价代换」的结果，例如，考虑到「逻辑与」是以下的符号定义： formula_245 那如果假设 formula_246 ，就有： 换句话说，从「 formula_246 」可以得到「 formula_250」，直观上相当于，把 formula_32 都代换成 formula_85 则两式等价。日后像这样递回地套用上述定理来得到「代换则某两式等价」，都简单地以「引用（Equv）」来表示这段实际的推演过程。 量词的可交换性. 由普遍化，很容易证明以下关于＂交换性＂的定理 注意最后（3）一般来说是不能反向的，只要想到＂对每个 formula_253，都有一个数（也就是 formula_254 ），使 formula_255＂，但是任取一个 formula_253 的数 formula_257 和任意的数 formula_5 ， formula_259 并不一定会为零。 量词的简写. 数学中常常有 ＂对所有 formula_260 有...＂，或是 ＂存在 formula_261 使的...＂。而两句话比较清晰，接近一阶逻辑语言的说法是 ＂对所有 formula_262 ，只要 formula_260 则...＂ 与 ＂存在 formula_264 ， formula_261 且...＂。「大于」直观上是一个二元关系，也就是说，在公理化集合论里对应于一条 formula_262 （ 或 formula_264 ） 在里面完全自由的合式公式。据此，可做以下的符号定义 但直观上也会说 ＂对所有 formula_268 和 formula_269 有...＂，这样连续，带有条件的全称量词也是有＂交换性＂的。 为了讨论这个问题，首先需要一些前置的定理 这样就可以证明以下定理 如果再加上 ＂项 formula_270 里没有 formula_11 ＂ 那就是 ＂对所有 formula_268 和 formula_269 有...＂，也就是以上所讨论的情况了。以这个定理配上全称量词本身的交换性定理，那这句话就可以等价的说成 ＂对所有 formula_171 和 formula_57 若 formula_268 且 formula_269 则...＂，所以根据＂且＂的可交换性，可以进一步的说成 ＂对所有 formula_269 和 formula_268 有...＂，所以连续带有条件的全称量词是＂可交换的＂。也就是说 但对于带条件的存在量词，首先可以得到以下非等价的定理。 这是因为一般来说， formula_280 不总是能推出 formula_281 。虽说如此，只要对公式做出一些限制，就会有以下交换的直观定理： 也就是直观上，「存在x使得 x>0 且 y>0」与｢y>0 且存在x使得 x>0」是一样的意思。 等式定理. 一般来说，等式 formula_282 会被视为某个合式公式 formula_283 的简写。若使用元定理的形式刻划等式的性质，会作如下的定义 \mathcal{E}(x,\,x) 。 formula_291 formula_296 并在这种状况下，规定 formula_282 为 formula_283 的简写。 上面的定义符合函数符号直观上的＂唯一对应＂。为了证明常数符号的＂唯一性＂，需要以下元定理 \mathcal{E}(x, \,y)\Rightarrow(\mathcal{A}\Rightarrow\mathcal{A}_y) 从上面可以得知，如果等式符号仅仅为断言符号，那等式和它的公理一节的等式公理模式，是等价于本节的（E1）+（E2'）+（E2＂）。 由上面的元定理，对带有等式符号的 formula_193 可以证明以下的等式性质 T=T 证明提示： 对任意常数符号 formula_305 ，上列元定理确保了 formula_306 formula_307 也就是常数符号的＂唯一性＂。 函数符号与唯一性. 唯一性. 数学讨论中，常常唯一存在某个符合特定条件的数，像是「存在唯一的实数 formula_308 使的对所有的实数 formula_309 ， formula_310 」；更精确地来说，这句话的意思是： 「存在 formula_308 使的对所有的实数 formula_309 ， formula_310」且「对所有的 formula_314 和所有 formula_309，若 formula_310 且 formula_317 则 formula_318 」 这样一般来说，可以对任意变数 formula_11 和合式公式 formula_320 做以下的符号定义： 注意到要能定义唯一性，一阶逻辑理论一定要带有等号。 新旧理论的等效条件. 上节所提到的例子，实际上就是所谓的实数 formula_321 ，但常数符号不能凭空从理论中冒出来，所以仔细来说，「定义实数 formula_321 」的过程应该是在原来的理论添加新的常数符号「 formula_321 」与以下的公理： 「对所有的实数 formula_309 有 formula_325 」 这样的话，「 formula_326」就是一条含有新常数符号的叙述，它应等价于： 存在 formula_308 使「formula_328 且对所有的 formula_329 ， formula_330」 也就是说，添加「 formula_321 」创造了一套新理论，新理论的每条新叙述会对应到旧理论的某条旧叙述，且照理来说，新的对旧的也会对，反之亦然。 更一般的来说，如果新的一阶逻辑理论，是在旧的理论增添一些新符号跟新公理（并额外要求新符号与旧公理相容），那为了让新旧理论等效，对于任意新理论的合式公式 formula_332 ，都要有某条相应的旧理论公式 formula_333 满足以下条件： 从条件（2）事实上就可以推出「若 formula_334 ，则有 formula_335 」，因为 formula_334 的话， 新理论只是扩张旧理论而没改变旧理论固有的定理，所以有 formula_337 ，但这样根据条件（2）跟MP律就会有 formula_335。所以条件（2）事实上是比「旧的对那新的也对」强的条件，但在之后的推导上（2）会比较方便。 预备定理. 在以严谨的方式实践以上提及的直观动机前，需要一个预备定理 新理论的假设. 一般来说，如果变数 formula_339 在 formula_340 完全自由，且旧理论里有： （formula_341）formula_342 那所谓的新理论，就是添加一个函数符号 formula_343 和以下的新公理： （formula_344）formula_345 如果仅仅是： formula_346 的话，添加的是常数符号 formula_347 与以下的新公理： （formula_341）formula_349 添加常数符号的情况可视为添加函数符号情况的特例，因为常数符号可以视为「零变数」的函数符号。 但不管如何，还需假设 formula_343 和新理论的逻辑公理、量词公理相容，也就是所有公理模式须涵盖内含 formula_343 的项。特别像是（A4）这种将自由变数代换成项的公理模式，也就是说，若项 formula_352 内含 formula_343 ，且公式 formula_354 内自由的 formula_11 都不在 formula_352 的变数的量词范围内，那 formula_357 仍然是新理论的公理。 另外还需要考虑到 formula_343 与等号的相容性（换句话说，新理论仍须是带等号的一阶逻辑理论），这样的话，考虑到上面等式定理所述的条件（E2"），需额外假设： 这样就有以下直观的定理 换句话说，「 formula_359 」在新理论里等价于 「对所有的实数 formula_309 ， formula_310」。 一阶逻辑的元定理. 下面列出了一些重要的元逻辑定理。 转换自然语言到一阶逻辑. 用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中，formula_362意味着“要么p要么q要么二者”，就是说它是“包容性”的。在英语中，单词“or”有时是包容性的（比如，“加牛奶或糖？”），有时是排斥性的（比如，“喝咖啡或茶？”，通常意味着取其中一个或另一个但非二者）。类似的，英语单词“some”可以意味着“至少一个，可能全部”，有时意味着“不是全部，可能没有”。英语单词“and”有时要按“or”转换（比如，“男人和女人可以申请”）。 一阶逻辑的限制. 所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。 难于表达if-then-else. 带有等式的FOL不包含或允许定义if-then-else断言或函数if（c,a,b），这里的c是表达为公式的条件，而a和b是要么都是项要么都是公式，并且它的结果是a如果c为真，或者b如果它为假。问题在于FOL中，断言和函数二者只接受（“非布尔类型”）项作为参数，而条件的明确表达是（“布尔类型”）公式。这是不幸的，因为很多数学函数是依据if-then-else而方便的表达的，而if-then-else是描述大多数计算机程序的基础。 在数学上，有可能重定义匹配公式算子的新函数的完备集合，但是这是非常笨拙的。 断言if（c,a,b）如果重写为formula_363就可以在FOL中表达，但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况断言叫做“if（条件，a, b）”（这里a和b是公式）和／或函数“ite（条件，a, b）”（这里的a和b是项），它们都接受一个公式作为条件，并且等于a如果条件为真，或b如果条件为假。这些扩展使FOL易于用于某些问题，并使某类自动定理证明更容易。 其他人进一步扩展FOL使得函数和断言可以在任何位置接受项和公式二者。 类型（种类）. 除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。 某些人争辩说缺乏类型是巨大优点 ，而很多其他人发觉了定义和使用类型（种类）的优点，比如帮助拒绝某些错误或不想要的规定 想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂，并也容易导致错误。 单一参数断言可以用来在合适的地方实现类型的概念。例如： formula_364， 断言Man（x）可以被认为是一类“类型断言”（就是说，x必须是男人）。 断言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如： formula_365（“存在既是男人又是人类的事物”）。 容易写成formula_366，但这将等价与formula_367（“存在不是男人的事物或者存在是人类的事物”），这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如： formula_368（“对于所有x，如果x是男人，则x是哺乳动物）。 难于刻画模型大小. 从Löwenheim–Skolem定理得出在一阶逻辑中不可能刻画有限性或可数性。若一阶理论有任意有限大的模型，则也有无穷大的模型，所以说不能刻划有限性。:1而若理论有某个无穷基数大小的模型，则也必有任意更大的模型，所以不能刻划可数性。:45另一个例子，是无法用一阶语言将实数系公理化，因为不论用何种一阶理论描述，既然该理论有实数系此种无穷模型（大小为formula_369），所以必有比实数系更大（比如formula_370）的另一个模型，从而该理论不是（唯一地）刻划实数系的性质。实数系满足的公理中，有上确界性质一项，它声称实数的所有有界的、非空集合都有上确界。一阶逻辑祗能对元素量化，但此公理中，要对模型的全部子集量化，这就需要二阶逻辑了。:30 图可及性不能表达. 很多情况可以被建模为节点和有向连接（边）的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用断言逻辑完全表达。换句话说，没有断言逻辑公式f，带有u和v作为它的唯一自由变量，而R作为它唯一的（2元）断言符号，使得f在一个有向图中成立，如果在这个图中存在从关联于u的节点到关联于v的节点的路径。 参见. 参考文献. 来源.