范畴逻辑引论

代数理论 (algebraic theory) 是对于结构的描述, 其完全基于操作 (operation) 和等式 (equation). 所有这样的代数概念都共有着一些相当深刻而广泛的性质, 从自由代数的存在性到Lawvere的对偶理论. 这些之中最基本的内容在本章呈现. 这里的发展也充当着函子语义(functorial semantics)的一般模式 (general scheme) 的第一个例子和模板, 之后的章节里也要用于其他逻辑概念.

第1.1节句法和语义

我们从诸如群, 环, 格之类的代数结构的一般方法开始. 这些是由公理化 (axiomization) 所刻画的, 其只牵涉单一种类 (sort) 的变量和常量, 操作, 以及等式. 操作在每一处都有定义是重要的, 这排除了两个重要的例子: 域, 鉴于

0

的(乘)逆没有定义, 以及范畴, 鉴于复合只对特定的态射序对有定义.

让我们从相当基础的代数理论开始: 群的理论. 在一阶逻辑之中, 一个群可以被描述为一个集合

G

带有一个二元操作

\cdot : G \times G \to G

, 其满足两条一阶公理:

\forall x, y, z \in G . (x \cdot y) \cdot z = x \cdot (y \cdot z)

\exists e \in G . \forall x \in G . \exists y \in G . (e \cdot x = x \cdot e = x \land x \cdot y = y \cdot x = e)

更仔细地观察这些公理的逻辑形式, 我们会发现第二条公理 (其表达了单位元和逆元的存在性) 有点不尽如人意, 因为它牵涉嵌套的量词. 不仅这会使得解释复杂化, 而且其也并非真正必要, 鉴于一个群中的单位元和逆元是唯一确定的. 因此, 我们可以将它们添加到结构之中并重新表述如下. 单位元以一个特别 (distinguished) 的常量

e \in G

表示, 而逆则是一个幺元操作

^{- 1} : G \to G

. 然后, 我们可以得到一个等价的表述, 其中所有的公理都可以被表达为(全称量化的)等式:

(x \cdot y) \cdot z = x \cdot (y \cdot z)

\begin{array}{l} x \cdot e = x & e \cdot x = x \\ x \cdot x^{- 1} = e & x^{- 1} \cdot x = e \end{array}

全称量词

\forall x \in G

\forall y \in G

在陈述公理时不再必要, 因为我们可以将所有的变量解释为遍历

G

的每个元素 (因为我们限制于考虑完全定义操作). 在描述中显式提及特定的集合

G

也无真正的必要. 最后, 既然常量

e

可以被视为一个零元操作, 即一个函数

e : 1 \to G

, 对于群的概念的描述可以仅有操作和等式构成. 这将我们引向了以下对于代数理论的一般定义.

定义1.1.1. 一个代数理论的一个签名(signature)

Σ

由一个集合族

{Σ_{k}}_{k \in ℕ}

构成.

Σ_{k}

的元素被称为 $k$ 元操作( $k$ -ary operation). 特别地,

Σ_{0}

的元素被称为零元操作或者常量.
一个签名

Σ

的项(term)是由以下规则归纳构造的表达式:

变量 $x, y, z, \dots$ 是项,
如果 $t_{1}, \dots, t_{k}$ 是项而 $f \in Σ_{k}$ 是一个 $k$ 元操作, 那么 $f (t_{1}, \dots, t_{k})$ 是一个项.

定义1.1.2. (参见定义1.2.10). 一个代数理论

𝕋 = (Σ_{𝕋}, A_{𝕋})

由一个签名

Σ_{𝕋}

和一个公理集

A_{𝕋}

给出, 其中公理是项之间的等式 (形式化地, 项的序对).

代数理论也被称为等式理论(equational theory). 我们并不假定集合

Σ_{k}

或者

A_{𝕋}

有限, 但是单独的项和等式只牵涉有限多个变量.

例子1.1.3. 一个含幺交换环的理论是一个代数理论. 存在两个零元操作 (常量)

0

和

1

, 一个幺元操作

-

, 还有两个二元操作

+

和

\cdot

. 等式为:

\begin{matrix} (x + y) + z = x + (y + z) & (x \cdot y) \cdot z = x \cdot (y \cdot z) \\ x + 0 = x & x \cdot 1 = x \\ 0 + x = x & 1 \cdot x = x \\ x + (- x) = 0 & (x + y) \cdot z = x \cdot z + y \cdot z \\ (- x) + x = 0 & z \cdot (x + y) = z \cdot x + z \cdot y \\ x + y = y + x & x \cdot y = y \cdot x \end{matrix}

例子1.1.4. 既没有操作也没有等式的空或者平凡理论

𝕋_{0}

是一个集合的理论.

例子1.1.5. 只有一个常量而没有等式的理论是一个带点集合的理论, 参见例子A.4.11.

例子1.1.6. 令

R

是一个环. 存在一个左

R

模的理论. 其有一个常量

0

, 一个幺元操作

-

, 一个二元操作

+

, 并且对于每个

a \in R

有一个操作

\overline{a}

, 其被称为乘上 $a$ 的标量乘法. 以下等式成立:

\begin{matrix} (x + y) + z = x + (y + z) & x + y = y + x \\ x + 0 = x & 0 + x = x \\ x + (- x) = 0 & (- x) + x = 0 \end{matrix}

对于每个

a, b \in R

, 我们也有等式

\overline{a} (x + y) = \overline{a} x + \overline{a} y, \overline{a} (\overline{b} x) = \overline{(a b)} (x), \overline{(a + b)} (x) = \overline{a} x + \overline{b} x

乘上

a

的标量乘法通常记作

a \cdot x

而非

\overline{a} x

. 如果我们将环

R

替换为一个域

𝔽

, 那么我们就得到了

𝔽

上的一个向量空间的代数理论 (尽管域的理论并非代数的!). {译注: 译者感觉向量空间的代数理论还需要另外的一条公理保证域的幺元和向量空间的元素的标量乘法仍然得到相同的这个向量空间元素.}

例子1.1.7. 在计算机科学之中, 归纳数据类型是代数理论的例子. 例如, 带有以整数标记的叶子的二叉树或许可以在某个编程语言中定义如下:

type tree = Leaf of int | Node of tree * tree

这对应于对于每个整数

n

都有一个常量

Leaf n

且还有一个二元操作

Node

的代数理论. 实际上, 当计算机科学家定义像这样的一个数据类型时, 他们在心中有一个特定的理论模型, 称为自由(free)模型.

范畴逻辑引论

第1章代数理论

第1.1节句法和语义

第2章命题逻辑

第3章一阶逻辑

第4章类型论

第5章依赖类型论

范畴逻辑引论

第1章 代数理论

第1.1节 句法和语义

第2章 命题逻辑

第3章 一阶逻辑

第4章 类型论

第5章 依赖类型论

第1章代数理论

第1.1节句法和语义

第2章命题逻辑

第3章一阶逻辑

第4章类型论

第5章依赖类型论