一阶语言
在逻辑学中, 一阶语言是一类形式语言, 是一阶逻辑使用的语言. 大部分现代数学都基于一阶逻辑, 例如主流数学的基础 ZFC 集合论便是由一阶语言写出的.
1定义
我们认为一阶逻辑是严格讨论数学的基础, 故在有一阶语言之前并无所谓 “严格”, 以下定义也不是严格写的, 而是用自然语言或者说元语言写的. 认为集合论比一阶逻辑更基本的读者大可用集合论写以下定义.
一个一阶语言 由如下几部分符号组成:
• |
• |
• | 变量, 即用于指代不固定对象的符号. |
以及逻辑符号:
• | 元谓词 , 代表矛盾, 或者说假. |
• |
• | 量词 , , 代表任意、存在. |
2例子
• | Peano 公理的语言有一个 1 元函数 即 “取后继” 的操作, 两个 2 元函数 , 即加法和乘法, 以及一个 2 元谓词 . |
• | ZFC 集合论的语言没有函数, 只有一个谓词 , 为 2 元. (这里不需要 , 而可以用外延公理将 视为 的简写.) |
3句法
以下这些概念的定义和上面一样也是用自然语言写的.
项
项递归定义如下:
• | 单个变量是项. |
• | 如 是 元函数, 是项, 则 是项. |
公式
公式递归定义如下:
• | 如 是 元谓词, 是项, 则 是公式. 这种公式称为元公式. |
• | 如 是公式, 则它们的逻辑连接 , , 是公式. 称为逻辑连接词. |
• | 如 是公式, 是变量, 则 , 是公式. 称为量词. |
实际书写公式时还会使用 , 的记号; 是 的简写, 是 的简写.
变量
主条目: 变量
变量在项和公式中的出现递归定义如下:
• | 变量 在项 中有一次出现. |
• | 在项 中的一次出现, 指的是一个 , 以及 在项 中的一次出现.
|
• | 在 中的一次出现指的是其在 中的一次出现. 在 , 中的一次出现指的是其在 中的一次出现或其在 中的一次出现. |
• | 在 , 中的一次出现指的是其在 中的一次出现. 这种出现称为绑定的. |
不绑定的出现称为自由的. 注意同一个公式中一个变量可以同时绑定出现和自由出现: 比如 中, 的第一次出现就是自由的, 第二次出现就是绑定的. 一个公式中如所有变量的所有出现都绑定, 则称其为闭的. 闭公式也称为语句.
演绎
一个相继式定义为一个表达式 , 其中 是一个公式集, 是一个公式.
一段演绎是一个有限树, 每一个节点是一个相继式, 节点之间的关系满足一些推导规则.
如果存在一段演绎使得其全部的分支的前提总是没有条件的相继式、而最终结论是 , 我们说 证明 (或句法蕴涵) , 也记作 .
有时也把演绎直接称为证明.
4语义
假设 是一个一阶语言.
结构
一个 -结构是一个二元组 , 其中 是一个集合, 而 是一个指派:
• | 对于 元函数 , 指派一个 元函数 . |
• | 对于 元谓词 , 指派一个 元关系 . |
项的翻译
假设 是一个 -结构, 一个参数指的是一个函数 . 其中 是所有变量组成的集合.
假设 是一个项, 则 在参数 下的翻译 递归定义为:
• | 如果 是变量 , 则 . |
• | 如果 是 , 则 . |
可满足性
给一个 -结构 与参数 , 那么对于任意公式 我们可以如下归纳定义:
• | . |
• | 对于任意元公式 , 定义 如果 . |
• | 定义 如果 . |
• | 定义 如果 且 . |
• | 定义 如果 或 . |
• | 定义 如果对于任意参数 满足 , 有 . |
• | 定义 如果存在参数 满足 , 使得 . |
如果 , 就说 在参数 下可满足, 否则称其为不可满足.
一个语句的可满足性不依赖于参数的选取, 故此时简记为 或 .
模型
设 是一个公式集.
一个 -结构 与一个参数 是 的一个模型, 如果任意公式 , 有 . 如果 的一个模型存在, 则称 是可满足的.
又设 是一个公式.
称 语义蕴涵 , 记作 , 如果 的任意模型都是 的模型.
5性质
完备性
参见: Gödel 完备性定理
一阶逻辑有完备性, 即 Gödel 完备性定理: 语义蕴涵等价于句法蕴涵. 假设 是一个一阶语言, 则对于任意公式集 和公式 , 有它建立了模型论和证明论之间的关系.
紧性
主条目: 紧性定理
一阶逻辑具有紧性, 即公式集 有模型等价于它的每一个有限子集有模型. 这是一个常用的构造模型的方法.
它可以直接由 Gödel 完备性定理推出.
Löwenheim–Skolem 定理
主条目: Löwenheim–Skolem 定理
Löwenheim–Skolem 定理说的是, 对于所有 -结构 , 以及满足如下条件的基数 , 则存在势为 的 -结构 , 使得:
• | 如果 , 那么 是 的初等子模型. |
• | 如果 , 那么 是 的初等扩张. |
6参考文献
• | H.-D. Ebbinghaus, J. Flum, W. Thomas (1994). Mathematical Logic, 2ed. Springer. |
术语翻译
一阶语言 • 英文 first-order language • 德文 Sprache erster Stufe • 法文 langage du premier ordre • 拉丁文 lingua ordinis primae • 古希腊文 γλῶττα πρώτου βαθμού
函数 • 英文 function • 德文 Funktion (f) • 法文 fonction (f) • 拉丁文 functio (f) • 古希腊文 συνάρτησις (f)
项 • 英文 term • 德文 Term (m) • 法文 terme (m) • 拉丁文 terminus (m) • 古希腊文 ὅρος (m)
公式 • 英文 formula • 德文 Ausdruck (m) • 法文 formule (f) • 拉丁文 formula (f) • 古希腊文 τύπος (m)
语句 • 英文 sentence • 德文 Satz (m) • 法文 énoncé (m) • 拉丁文 sententia (f) • 古希腊文 πρότασις (f)