目录
存在量化
在谓词逻辑中，存在量化是对一个域的至少一个成员的性质或关系的论断。使用叫做存在量词逻辑算子符号∃来指示存在量化。 它相对于声称某些事物对所有事物都为真的全称量化。.
查看 存在概括和存在量化
一阶逻辑
一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统。 過去一百多年，一階邏輯出現過許多種名稱，包括：一阶斷言演算、低階斷言演算、量化理論或斷言逻辑（一個較不精確的用詞）。一階邏輯和命題邏輯的不同之處在於，一階邏輯有使用量化變數。一個一階邏輯，若具有由一系列量化變數、一個以上有意義的斷言字母及包含了有意義的斷言字母的純公理所組成的特定論域，即是一個一階理論。 一階邏輯和其他高階邏輯不同之處在於，高階邏輯的斷言可以有斷言或函數當做引數，且允許斷言量詞或函數量詞的（同時或不同時）存在。在一階邏輯中，斷言通常和集合相關連。在有意義的高階邏輯中，斷言則會被解釋為集合的集合。 存在許多對一階邏輯是可靠（所有可證的敘述皆為真）且完備（所有為真的敘述皆可證）的演繹系統。雖然一階邏輯的邏輯歸結只是半可判定性的，但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯定理，如勒文海姆–斯科倫定理及緊緻性定理。 一階邏輯是數學基礎中很重要的一部份，因為它是公理系統的標準形式邏輯。許多常見的公理系統，如一階皮亞諾公理和包含策梅洛-弗蘭克爾集合論的公理化集合論等，都可以形式化成一階理論。然而，一階定理並沒有能力去完整描述及範疇性地建構如自然數或實數之類無限的概念。這些結構的公理系統可以由如二階邏輯之類更強的邏輯來取得。.
查看 存在概括和一阶逻辑
全称实例化
在逻辑中，全称实例化或全称列举（Universal Instantiation,简称UI,拉丁文中叫做"Dictum de omni"）是从关于一类个体的每个成员的真理到关于这个类的特定个体的真理的推理。它一般作为全称量词的量化规则给出，但也可以作为一个公理。它是量化理论的基本原理之一。 例子："所有的狗都是动物。Fido是狗。所以Fido是动物。" 作为一个公理模式： ∀xA → A(a/x)，A(a/x)是把A中所有x的自由出现替代为某个项a的结果。 作为一个推理规则: 从 ⊢ ∀xA 推出 ⊢ A(a/x)，A(a/x)同上。.
查看 存在概括和全称实例化
谓词逻辑
在数理逻辑中，谓词逻辑（Predicate logic）是符号形式系统的通用术语，比如一阶逻辑，二阶逻辑，多类逻辑或无穷逻辑等等。.
查看 存在概括和谓词逻辑
英语
英语（English，）是一种西日耳曼语言，诞生于中世纪早期的英格兰，如今具有全球通用语的地位。“英语”一词源于迁居英格兰的日耳曼部落盎格鲁（Angles），而“盎格鲁”得名于临波罗的海的半岛盎格里亚（Anglia）。弗里西语是与英语最相近的语言。英语词汇在中世纪早期受到了其他日耳曼族语言的大量影响，后来受罗曼族语言尤其是法语的影响。英语是将近六十个国家唯一的官方语言或官方语言之一，也是全世界最多國家的官方語言。它是英国、美国、加拿大、澳大利亚、爱尔兰和新西兰最常用的语言，也在加勒比、非洲及南亚的部分地区被广泛使用。它是世界上母语人口第三多的语言，仅次于汉语和西班牙语。英语是学习者最多的第二外语跟學習者最多的第一外語，是联合国、欧盟和许多其他国际组织的官方语言。它是使用最广泛的日耳曼族语言，至少70%的日耳曼语族使用者说英语。 英语有1400多年的发展史。公元5世纪，盎格魯-撒克遜人把他们的各种盎格鲁-弗里西语方言带到了大不列顛島，它们被称为古英语。中古英语始于11世纪后期的诺曼征服，这一时期英语受到了法语的影响。15世纪末伦敦对印刷机的采用、《钦定版圣经》的出版及元音大推移标志了近代英语的开端。通过大英帝国对全球的影响，现代英语在17世纪至20世纪中叶传播到了世界各地。通过各种印刷和电子媒体，随着美国取得全球超级大国地位，英语已经成为了国际对话中居领导地位的世界語言。它还是许多地区和行业（如科学、导航、法律等）的通用语。 现代英语和很多其他语言相比屈折变化较少，更多地依靠助動詞和语序来表达复杂的时态、体和语气，以及被動語態、疑问和一些否定。英语的各种口音和方言在发音和音位方面有显著差异，有时它们的词汇、语法和拼法也有所不同，但世界各地说英语的人能基本无碍地沟通交流。.
查看 存在概括和英语
推理规则
在逻辑中，特别是数理逻辑中，推理规则（推论规则）是构造有效推论的方案。这些方案建立在一组叫做前提的公式和叫做结论的断言之间的语法关系。这些语法关系用于推理过程中，新的真的断言从其他已知的断言得出。规则也适用于非形式逻辑和逻辑论证，但是形式化更加困难和有争议。 按照规定，推理规则的应用纯粹是语法过程。尽管如此它必须是有效的，或者更精确地说保持有效性。为了使保持有效性的要求有意义，某种形式的语义与推理规则有关和推理规则自身的断言是必需的。对于在推理规则和和语义之间相互关系的讨论请参见命题逻辑。 命题逻辑中推理规则的显著例子是肯定前件和否定后件规则。对于一阶谓词逻辑，推理规则需要处理逻辑量词。对这种论证的更详细的描述请参见有效性。在一阶谓词逻辑中把所有推理规则作为一个单一规则来统一处理请参见一阶归结。 注意有很多不同的形式逻辑系统，每个都带有合式公式、推理规则和语义的自己的集合。参见时间逻辑、模态逻辑或直觉逻辑的实例。量子逻辑也是一种不同寻常形式的逻辑。参见证明论。在谓词演算中，需要一个补充的推理规则。它叫做普遍化。 在形式逻辑的设置（和很多有关领域）中，推理规则通常用如下形式给出： 前提#1 前提#2 ...
查看 存在概括和推理规则
普遍化
普遍化是谓词演算的一个推理规则，它声称： "普遍化"可以缩写为GEN，而推理规则可以被总结为相继式 但是这引起了一个重要的限制：不能应用演绎定理（DT）于它而推导出 这个公式是错的，因为 x 在前提中是一个无约束的实例，在结论中是一个约束的出现，所以如果这个公式是正确的，则它的 x 的自由实例可以被任何常量（域的元素）所替代： 但这是不正确的。比如，如果 P(x) 意味着 "x 是素数" 而域是自然数集合，则 明显不是真的，因为从它和 "7 是素数"，可以通过肯定前件推出 "所有自然数都是素数"，这是个矛盾，所以反证法得出这个公式是错的。 这个限制适用于证明：如果 GEN 在一个证明中应用于一个公式，从而约束了它的自由变量 x，则 DT 不能应用于这个证明中把这个公式移动到十字转门的右侧。 注意 P(x) 符号化带有自由变量 x 的开放陈述，它的真实视 x 而定，但是 \vdash P(x) 符号化（对于 x 的所有值）有效的一个陈述，即使它的变量 x 是自由的。GEN 应用于这种有效陈述，约束自由变量并生成 \vdash \forall x P(x) 。 所以公式 \vdash \forall x P(x) 只是陈述已经被 \vdash P(x) 蕴涵的事情的更明确的方式。 在谓词演算中还有一个公理，它声称 它通过演绎定理的逆定理可变换成 这意味着从 \vdash \forall x P(x) 可以推导 \vdash P(x) 。把 GEN 和这个公理放在一起，你可以推出 它的意义不同于 它是错误的原因是 P(x) 可以是任何偶然的（contingent）、无效的、开放公式。为了从根本上防止这种错误的公式，在谓词逻辑中这个限制被增加到 DT 上。 十字转门符号 \vdash 不是合式公式的一部分：严格的说它既不属于命题演算也不属于谓词演算，而可以被认为是一个"元符号"。所以，最终 \vdash \forall x P(x) 实际上意义不多于 \vdash P(x) ，因为 \vdash 符号实际上不是公式 P(x) 的一部分；比喻来说，它只是用来"抓住"这个公式的一个"把手"。.
查看 存在概括和普遍化
另见
推理规则
谓词逻辑
- 一元谓词演算
- 一阶逻辑
- 全称实例化
- 分体论 (逻辑学)
- 原子公式
- 原子句子
- 句子 (数理逻辑)
- 子句 (逻辑)
- 存在概括
- 普遍化
- 概念文字
- 自由变量和约束变量
- 论域
- 谓词变量
- 量化 (数理逻辑)
- 饮者悖论
- 高阶逻辑