1.1. 一阶语言

首先, 我们来描述什么是自然数.

定义 1.1.0.1 (自然数). 这些符号用来表示我们直觉接受的自然数.

当我们需要一个任意的自然数时, 我们会用小写字母 之一表达. 在没有特别标注时, 它们一定是任意自然数的意思.

如果我们有一种方法, 任给自然数 均可由这一方法确定唯一的自然数 , 则称这个方法是一个自然数到自然数的函数, 用 表示. 这一方法从 确定的自然数 记为 .

我们默认一切初等数论知识, 包括但不限于: 加法、乘法、数学归纳法、整除、素数、算术基本定理、同余、中国剩余定理.

评注. 对于自然数的标准性、我们如何认知自然数, 什么是自然数的相等, 以及为何允许谈论任意自然数, 什么是自然数到自然数的函数, 请看本章末尾的注记. 今后不再特别指出.

我们的一切定义都基于自然数. 现在, 我们来指定语言中允许的字符表.

定义 1.1.0.2 (一阶语言的字符). 一阶语言的字符表被我们列举如下:

1.

变元符号 , 任意变元用 表达.

2.

函数符号 , 任意函数符号用 表达.

3.

谓词符号 , 任意谓词符号用 表达.

4.

逻辑连接词符号 , 读作否定和蕴含.

5.

量词符号 , 读作对所有 (for all).

6.

括号 .

这里 总是跑遍自然数, 换言之任给自然数 均有一个自由变元符号 , 一个 元函数符号 和一个谓词符号 .

我们还有自然数到自然数的两个函数: 函数元数指示器 , 谓词元数指示器 . 它们不是字符表中的字符. 我们称 的元数, 的元数.

我们还有两个自然数: 函数个数 与谓词个数 . 我们总是只考虑下标 的函数符号 与下标 的谓词符号 .

我们总是特别地要求 , 且记 . 如果一个 使得 , 则称 是一个常数符号.

一个四元组 称作一个一阶语言 . 以下我们总是默认选定了一个一阶语言.

评注. 我们也可以认为上面全部都是奇数: 是第一个奇数 , 是后面两个奇数 , 是再后面的两个奇数 , .

接下来, 我们直觉地指出一个概念.

定义 1.1.0.3 (字符串). 我们归纳地定义一个字符表下长度为任意自然数 的字符串:

1.

长度为 的字符串是空串.

2.

长度为 的字符串是长度为 的字符串在后面串接一个字符表中的字符得到的新字符串.

进一步, 我们可以定义字符串的串接, 串接后的字符串长度变为被串接的两字符串长度之和.

我们认为这一递归定义确实归纳地指出所有的字符串.

评注. 我们也可以认为字符串是自然数: 长度 的字符串是 , 长度 的作为自然数的字符串 串接作为自然数的字符 得到的长度 的字符串对应的自然数是 , 这里 是第 个质数.

有了字符串的概念, 我们就可以定义我们所需的语言中的对象了.

定义 1.1.0.4 (项). 我们递归定义以下形式的字符串为项:

1.

是项.

2.

是函数符号, 是函数 的元数, 个项, 则 是项.

我们认为这一递归定义确实归纳地指出所有的项. 项通常用 表达.

评注. 这一递归定义成立是因为它事实上定义了一些满足要求的自然数, 这些自然数对应的字符串就是项. 以下的递归定义和归纳法都因此成立.

定义 1.1.0.5 (公式). 我们递归定义以下形式的字符串为公式:

1.

是谓词符号, 是谓词 的元数, 个项, 则 是公式.

2.

是公式, 则 是公式.

3.

是公式, 则 是公式.

4.

是公式, 是变元, 则 是公式.

我们认为这一递归定义确实归纳地指出所有的公式. 公式通常用 表达. 我们称形如 的公式为原子公式.

项和公式是我们要处理的全部语言对象. 它们本质上是满足特定规则的字符串. 接下来, 我们来给出它们的一些性质.

定义 1.1.0.6 (自由出现). 对每个 , 我们可以对所有项和所有公式讨论 在其中的自由出现性. 对项 而言, 中自由出现当且仅当字符 在字符串 中出现. 对公式而言, 归纳定义:

1.

形如 的公式, 在其中自由出现当且仅当它在这个字符串中出现.

2.

形如 的公式, 在其中自由出现当且仅当它在 中自由出现.

3.

形如 的公式, 在其中自由出现当且仅当它在 中自由出现或它在 中自由出现.

4.

形如 的公式, 在其中自由出现当且仅当它在 中自由出现且 不是 .

对项 , 我们通常将其中自由出现的变元全部列出, 记为 , 这里 是有限个互不相同的自然数. 对公式 , 我们同样将其中自由出现的变元全部列出, 记为 . 为了方便, 我们又会记 以忽略具体的 的值.

评注. 这一递归定义成立的理由仍然需要我们回到它们对应的自然数上去论证.

定义 1.1.0.7 (替换). 给定变元 与项 , 我们定义一个操作 , 它递归地将公式变为另一个公式:

1.

形如 的公式 , 这一字符串中所有 出现的地方都将 替换为 得到的新公式.

2.

形如 的公式 , .

3.

形如 的公式 , .

4.

形如 的公式 , 若 仍然是是 , 若 .

我们还要禁止一些改变语义 (虽然我们现在还没有严格定义语义) 的替换操作, 因此我们继续递归地对每个公式 定义 是否是无冲突替换.

1.

形如 的公式 , 总是无冲突替换.

2.

形如 的公式 , 是无冲突替换当且仅当 是无冲突替换.

3.

形如 的公式 , 是无冲突替换当且仅当 都是无冲突替换.

4.

形如 的公式 , 是无冲突替换当且仅当 不在 中自由出现, 或 是无冲突替换且 不在 中出现.

评注. 我们写 指的是这两个字符是同一个字符, 这与公式 并不是一个意思.

以上定义了为了能讨论证明这一概念所需要的所有前置概念.