一阶语言first-order logic

陈述

一阶语言 $\mathcal{L}$ 由一张符号表给定，符号分两类：

• 逻辑符号（所有一阶语言共用）：可数多个变元 $v_{0}, v_{1}, v_{2}, \ldots$；连接词 $\neg$；量词 $\forall$；等号 $=$；括号。
• 非逻辑符号（每个语言自己的）：常元符号、$n$ 元函数符号、$n$ 元关系符号，每一种都带一个确定的元数 $n$。

由符号表，用三条语法规则生成全部的项与公式：

1. 变元、常元符号是项；若 $f$ 是 $n$ 元函数符号而 $t_{1}, \ldots, t_{n}$ 是项，则 $f(t_{1}, \ldots, t_{n})$ 是项；
2. 若 $R$ 是 $n$ 元关系符号而 $t_{1}, \ldots, t_{n}$ 是项，则 $R(t_{1}, \ldots, t_{n})$ 是原子公式；
3. 公式由原子公式出发，经 $\neg$、$\wedge$、$\vee$、$\to$、$\forall v_{i}$、$\exists v_{i}$ 反复组合而成。

例：$\mathcal{L} = \{ \in \}$（$\in$ 是一个二元关系符号）就是集合论的语言 —— ZFC 的全部公理都写在这门语言里。