我们先来论证一个熟知的元定理.
对每个元自然数 n, ReS0 可证存在一个对应的集合 ┌n┐, 满足以下特质:
1. | ┌0┐=∅ |
2. | isOrd(┌n┐) |
3. | ┌n┐={┌k┐∣0≤k<n} |
证明. 我们采取元数学归纳法, 只需从需论证的第三个特质读出
┌n+1┐=┌n┐∪{┌n┐} 即可.
然而, 我们希望能直接在集合论中谈论自然数, 因此我们考虑以下对自然数的刻画.
我们定义 isNat(x) 为 x=∅∨(isSuccOrd(x)∧∀y∈x(isSuccOrd(y)∨y=∅)). 这时, x 将被称作一个自然数. 这是 Δ0 谓词.
如果集合 n 满足 isNat(n), 则存在一个元自然数 n 使得 n=┌n┐.
由于这个论题涉及的乃是我们对于 " 自然数 " 这一概念的直观理解 (你无法真的获得你对自然数的先天经验的一个完全的能形式化的刻画), 它永远只能是一个论题 (而不是一个命题), 你只能选择相信它或者不相信它, 为它辩护或为它的对立面辩护或者对某个你喜欢的观点辩护, 但你没办法证明它, 因为它根本不是一个能被形式化的句子, 没有人能定义对这种东西的 " 证明 " 是什么. 然而, 我们总能不依赖这个论题而证明一些简单的关于自然数的事实, 例如 (形式化的) 数学归纳法 (模式).
ReS0⊢(Fnd)Πn↔(Ind)Σn
证明. (Fnd)Πn 推 (Ind)Σn: 反证. 如果 ∃v0...∃vm−1(∀x(∀y(y∈x→φ(y,v0,...,vm−1))→φ(x,v0,...,vm−1))∧∃x(¬φ(x,v0,...,vm−1))), 这时记 ψ=¬φ, 由于 φ 是 Σn 的, 自然 ψ 是 Πn 的. 后半句话说 ∃x(ψ(x,v0,...,vm−1)), 于是 Πn(Fnd) 将它加强为 ∃x(ψ(x,v0,...,vm−1)∧∀y∈x(¬ψ(y,v0,...,vm−1))), 而这个后半句话带进反设的前半句又会指出 ¬ψ(x,v0,...,vm−1), 遂矛盾.
(Ind)Σn 推
(Fnd)Πn: 同反证, 细节略.
因此, 添加多强的基础公理模式就是添加相反的多强的归纳公理模式. 具体到自然数上, 我们有:
考虑以下两种归纳法.
1. | 任给一个公式 φ(x,v0,...,vn−1), 均有 ∀v0...∀vn−1((∃x(¬φ(x,v0,...,vn−1))→∃x(¬φ(x,v0,...,vn−1)∧∀y∈x(φ(y,v0,...,vn−1))))→(φ(∅,v0,...,vn−1)∧∀x(isNat(x)→φ(x,v0,...,vn−1)→φ(Succ(x),v0,...,vn−1))→∀x(isNat(x)→φ(x,v0,...,vn−1)))) |
2. | 任给一个公式 φ(x,v0,...,vn−1), 均有 ∀v0...∀vn−1((∃x(¬φ(x,v0,...,vn−1))→∃x(¬φ(x,v0,...,vn−1)∧∀y∈x(φ(y,v0,...,vn−1))))→(φ(∅,v0,...,vn−1)∧(∀x(isNat(x)→∀y∈x(φ(y,v0,...,vn−1))→φ(x,v0,...,vn−1)))→∀x(isNat(x)→φ(x,v0,...,vn−1)))) |
我们还能证明最小自然数原理: 任给一个公式 φ(x,v0,...,vn−1), 均有
∀v0...∀vn−1((∃x(φ(x,v0,...,vn−1))→∃x(φ(x,v0,...,vn−1)∧∀y∈x(¬φ(y,v0,...,vn−1))))→(∃x(φ(x,v0,...,vn−1))→∀x(φ(x,v0,...,vn−1)→isNat(x))→∃x(φ(x,v0,...,vn−1)∧∀y∈x(¬φ(y,v0,...,vn−1)))))
证明. 对第一种数学归纳法, 反证. 这个
x 将见证
∃x(¬φ(x,v0,...,vn−1)) 从而触发前提, 前提给出的这个特别的
x 既然又是自然数, 则它是某个自然数的后继或是空集, 均导出矛盾. 其余同理.
用归纳法的语言, 对 n≥1 我们有:
1. | Πn−ReS 可以形式化对 Σn 公式的数学归纳法, Σn−ReS 可以形式化对 Πn 公式的任意多重数学归纳法, Σn+1−ReS 可以形式化对 Σn 公式的任意多重数学归纳法. |
2. | Πn−ReS 可以形式化对 Σn 公式的第二数学归纳法, Σn−ReS 可以形式化对 Πn 公式的任意多重第二数学归纳法, Σn+1−ReS 可以形式化对 Σn 公式的任意多重第二数学归纳法. |
证明. 注意到 Π1−ReS 只有 Π1 的基础公理模式, 换言之数学归纳法只能归纳 Σ1 公式, 因此二重归纳 (先对 m 归纳再对 n 归纳, 换言之对 ω⋅m+n 进行超限归纳) 看起来就是不能进行的 (对 m 归纳的是一个 Π2 也就是 Σ3 句子), 这是一个非常讨厌的事实. 下面且举关键一例论证.
对
x0 归纳以证明
∀x0(isNat(x0)→∀x1(isNat(x1)→...→∀xm(isNat(xm)→φ(x0,...,xm,v0,...,vk−1)))) 时, 若
φ 是
Πn 公式, 则
∀x1(isNat(x1)→...→∀xm(isNat(xm)→φ(x0,...,xm,v0,...,vk−1))) 仍是
Πn 公式.
总之, 在不具有充足的基础公理模式的弱集合论中, 随意使用归纳法容易引发危险. 怎么才能丢掉这一大堆莫名其妙的基础公理模式, 而以最简单情形代之呢? 一个方案是考虑下列弱归纳法.
弱 Σ1 多重数学归纳法: 对 Δ0 句子 ψ(x,n1,...,nn),
Π1−ReS⊢∀n1...∀nn(isNat(n1)→...→isNat(nn)→∃xψ(x,n1,...,nn)↔∀m1∈n1...∀mn∈nn(∃xψ(x,m1,...,mn)))→∀n1...∀nn(isNat(n1)→...→isNat(nn)→∃xψ(x,n1,...,nn))
证明. n=1 早已得知, 不妨设 n≥2, 反设结论不对, 即有一组 Ni(i=1,...,n) 使得 ∀x¬ψ(x,N1,...,Nn) 且 isNat(Ni); 不妨设 N1 是诸 Ni 中极大者, 则它实际上满足 ∀Mi∀x(N1∈Mi→isNat(Mi)→¬ψ(x,M1,...,Mn)), 进而对其使用 Π1 基础公理模式我们可以额外要求 ∀N1′∈N1∃Mi∃x(N1′∈Mi∧isNat(Mi)∧ψ(x,M1,...,Mn)).
现在由一开始对诸 Ni 的条件, ∃ni∈Ni∀x¬ψ(x,n1,...,nn). 注意到它对每个 i 有推论 ∃ni∀x(ni∈Ni∧∃j=inj∈Nj(¬ψ(x,ni,...,nn))), 对其使用 Π1 基础公理模式得到这样一些 ni∈Ni, 满足两个条件:
1. | ∀x∃j=imj∈Nj(¬ψ(x,m1,...,ni,...,mn)) |
2. | ∀mi∈ni∃x∀j=imj∈Nj(ψ(x,m1,...,mn)) |
∀mi∈ni(∃xψ(x,m1,...,mn))
证明. 若不然, 取一组
mi∈ni 使得
∀x¬ψ(x,mi). 对每个
i 使用
ni 的第二个条件, 我们取得一组
xi 满足
∀j=ikj∈Nj(ψ(xi,k1,...,mi,...,kn)). 特别地取
i=1,
kj=mj 我们就得到
ψ(x1,m1,...,mn), 立即矛盾.
∃mi∈Ni∀x(ni∈mi∧¬ψ(x,m1,...,ni,...,mn))
证明. 若不然,
∀mi∈Ni∃x(ni∈mi∨ψ(x,m1,...,ni,...,mn)), 我们宣布
∀mi∈Ni∃x(ψ(x,m1,...,ni,...,mn)): 否则
mi∈Ni 使
∀x¬ψ(x,m1,...,ni,...,mn), 则须有
ni∈mi 总对, 换言之
mi∈ni 总对, 这和上一个断言矛盾. 但这句话本来就和我们对诸
Ni 的要求矛盾, 所以一开始的反设是错的.
于是, 这个断言中的
mi 可以完全取代
Ni 的每个作用. 如果
m1 是诸
mi 中的极大者, 则由我们对
N1 的额外要求, 有一些
Mi 使得
m1∈Mi(进而
mi∈Mi) 但
∃xψ(x,M1,...,Mn), 这与
∀x¬ψ(x,m1,...,mn) 矛盾. 如果
m1 不是诸
mi 中极大者, 假定
m2 是, 则它实际上又满足
∀Mi∀x(m2∈Mi→isNat(Mi)→¬ψ(x,M1,...,Mn)), 进而对其使用
Π1 基础公理模式我们可以额外要求
∀N2′∈m2∃Mi∃x(N2′∈Mi∧isNat(Mi)∧ψ(x,M1,...,Mn)). 继续同上操作, 这一过程必在
n 步之内终止, 进而停在一次矛盾上, 反证结束.
接下来, 我们考虑自然数上的算术结构. 由以上讨论, 我们不妨以 TAr 指代 Π1−ReS, 以表彰其对算术结构的刻画的有效性.
定义 Δ0 谓词 +a(f,m,n,d,s)↔isFunOn(f,d,s)∧isNat(m)∧isNat(n)∧isNat(s)∧d=m×n∧∀a∈m((∅∈n→f(a,∅)=a)∧∀b∈n(Succ(b)∈n→∃z∈s(z=f(a,Succ(b))=Succ(f(a,b))))).
我们接着宣称以下 Σ1 句子和 Π1 句子同时定义出一个 Δ1TAr 的函数符号: s=m+n↔∃u∃v∃f∃d∃t(m∈u∧n∈v∧+a(f,u,v,d,t)∧f(m,n)=s)↔∀u∀v∀f∀d∀t(m∈u∧n∈v∧+a(f,u,v,d,t)→f(m,n)=s).
证明. 我们先断言一个事实.
+a(f,m,n,d,s)→∀b∈n((∅∈m→f(∅,b)=b)∧∀a∈m(Succ(a)∈m→f(Succ(a),b)=Succ(f(a,b)))).
证明. 对
m 和
n 进行二重归纳, 这句子不过
Δ0, 显然是可以归纳的.
接下来是主要的断言.
∀u(isNat(u)→∀v(isNat(v)→∃f∃d∃t(+a(f,u,v,d,t)))).
证明. 被归纳的句子 Σ1. u=∅ 和 v=∅ 的情形无需多言, 因此我们直接拿到归纳假设来证明此事对 Succ(u),Succ(v) 同样成立. 归纳假设会告诉我们此事对 Succ(u),v 和 u,Succ(v) 已经成立, 我们不妨设前者由函数 f1 和值域 t1 计算, 后者由函数 f2 和值域 t2 计算, 我们宣称以下事实.
∀a∈u∀b∈v(f1(a,b)=f2(a,b)), 且 t1=t2.
证明. 对前一个命题反证, 若 ∃b∈v∃a∈u∃s∈t1(s=f1(a,b)∧s=f2(a,b)), 我们用 Δ0 分离得到 v 中满足这一条件的全体 b 构成的子集, 然后提取最小满足此条件的 b. 如果 b=∅, 这是矛盾的, 因为我们知道 f1(a,∅)=f2(a,∅)=a; 如果 b=Succ(b′), 这依然矛盾, 因为我们知道 f1(a,b′)=f2(a,b′), 从而也必须有 f1(a,b)=f2(a,b)=Succ(f1(a,b′)).
对后一个命题只需注意到
t1=t2=Succ(f1(m,n)), 其中
u=Succ(m) 而
v=Succ(n).
因此, 令
f=f1∪f2∪{((u,v),t1)},
t=Succ(t1), 不难验证它们确实满足条件.
这个主要的断言就告诉我们 Σ1 句子确实满足 ∀m∀n∃s. 接下来只要证明这个 s 唯一, 就能确认 Σ1 句子确实定义一个函数, 且顺带证明了 Π1 句子与 Σ1 句子定义了同一件事, 从而定义了同一个函数.
反证. 如果
s 不唯一, 则对应的
f 自然不同, 余下的过程不过是再把主要断言中引用的断言的证明再写一次.
将集合的卡氏积记为 ×Cart, 我们定义 Δ1TAr 谓词 ×a(f,m,n,d,s)↔isFunOn(f,d,s)∧isNat(m)∧isNat(n)∧isNat(s)∧d=m×Cartn∧∀a∈m((∅∈n→f(a,∅)=∅)∧∀b∈n(Succ(b)∈n→∃z∈s(z=f(a,Succ(b))=f(a,b)+a))).
我们接着宣称以下 Σ1 句子和 Π1 句子同时定义出一个 Δ1TAr 的函数符号: s=m×n↔∃u∃v∃f∃d∃t(m∈u∧n∈v∧×a(f,u,v,d,t)∧f(m,n)=s)↔∀u∀v∀f∀d∀t(m∈u∧n∈v∧×a(f,u,v,d,t)→f(m,n)=s).
证明. 我们先断言一个事实.
×a(f,m,n,d,s)→∀b∈n((∅∈m→f(∅,b)=∅)∧∀a∈m(Succ(a)∈m→f(Succ(a),b)=f(a,b)+b)).
证明. 采用这句子的
Σ1 形式对
m 和
n 进行二重归纳.
接下来同样是主断言.
∀u(isNat(u)→∀v(isNat(v)→∃f∃d∃t(×a(f,u,v,d,t)))).
证明. 采取被归纳句子的 Σ1 形式, u=∅ 和 v=∅ 的情形无需多言, 我们同样拿到归纳假设来证明此事对 Succ(u),Succ(v) 同样成立. 归纳假设会告诉我们此事对 Succ(u),v 和 u,Succ(v) 已经成立, 我们不妨设前者由函数 f1 和值域 t1 计算, 后者由函数 f2 和值域 t2 计算, 我们再次宣称以下事实.
∀a∈u∀b∈v(f1(a,b)=f2(a,b)), 且 t1+v=t2+u.
证明. 对前一个命题反证, 若 ∃b∈v∃a∈u∃s∈t1(s=f1(a,b)∧s=f2(a,b)), 我们用 Δ0 分离得到 v 中满足这一条件的全体 b 构成的子集, 然后提取最小满足此条件的 b. 如果 b=∅, 这是矛盾的, 因为我们知道 f1(a,∅)=f2(a,∅)=∅; 如果 b=Succ(b′), 这依然矛盾, 因为我们知道 f1(a,b′)=f2(a,b′), 从而也必须有 f1(a,b)=f2(a,b)=f1(a,b′)+a.
对后一个命题只需注意到
t1+v=t2+u=f1(m,n)+u+v, 其中
u=Succ(m) 而
v=Succ(n).
因此, 令
f=f1∪f2∪{((u,v),f1(m,n)+u+n)},
t=t1+v, 不难验证它们确实满足条件.
这个主要的断言就告诉我们
Σ1 句子确实满足
∀m∀n∃s. 接下来只要证明这个
s 唯一, 就能确认
Σ1 句子确实定义一个函数, 且顺带证明了
Π1 句子与
Σ1 句子定义了同一件事, 从而定义了同一个函数. 反证手法与加法一模一样.
因此, 我们事实上证明了如下事实.
TAr 有 Σ1−PA 的解释, 此处 Σ1−PA 指的是在 PA 中将数学归纳法限制到 Σ1 算术句子的版本. 进一步, 鉴于 Σ1−PA 已有 Godel 第二不完备性定理, 不弱于 TAr 的理论均有 Godel 第二不完备性定理.
我们也可以证明递归函数的可表示性.
TAr 有所有递归函数的 Δ1TAr 表示.
证明. 我们只需要依次处理初始函数、复合函数、正则极小化和原始递归四个过程. 对于初始函数, 我们事实上有一个论证起来并不更加困难的断言.
算术语言中的项诱导出的函数都是可在 TAr 中由 Δ1TAr 公式表示的.
证明. 我们归纳. 这个项显然是用后继、加法和乘法三种符号拼出来的, 所以分类施以讨论. 我们将项 t 定义的函数记为 ft, ft 的表示是 φt.
1. | 如果这个项只有一个函数符号, 它必然形如 S(x) 或 x+y 或 x+x 或 x×y 或 x×x. ReS0 就知道 y=Succ(x) 是 Δ0 的, z=x+y 和 z=x+x 和 z=x×y 和 z=x×x 是 Δ1TAr 的. |
2. | 这个项 r 是某个项外面加一个后继符号, 即形如 S(t). 归纳假设指出 φt 是 Δ1TAr 的, 注意 φr 既可以是 ∃x(x=ft∧y=Succ(x)) 也可以是 ∀x(x=ft→y=Succ(x)). |
3. | 这个项 r 是某两个项外面加一个加法符号, 即形如 t+s. ∃xt∃xs(xt=ft∧xs=fs∧y=xt+xs)↔∀xt∀xs(xt=ft∧xs=fs→y=xt+xs). |
4. | 这个项 r 是某两个项外面加一个乘法符号, 即形如 t×s. ∃xt∃xs(xt=ft∧xs=fs∧y=xt×xs)↔∀xt∀xs(xt=ft∧xs=fs→y=xt×xs). |
接下来处理函数复合, 手法照旧.
若 h1(x1,...,xn),...,hm(x1,...,xn),g(x1,...,xm) 都有 Δ1TAr 表示, 则
f(x1,...,xn)=g(h1(x1,...,xn),...,hm(x1,...,xn)) 也有 Δ1TAr 表示.
证明. ∃z1...∃zm(z1=h1(x1,...,xn)∧...∧zm=hm(x1,...,xn)∧y=g(z1,...,zm))↔∀z1...∀zm(z1=h1(x1,...,xn)∧...∧zm=hm(x1,...,xn)→y=g(z1,...,zm)).
接下来处理正则极小化.
若已知对每组 x1,...,xn 均存在 y 使得 f(x1,...,xn,y)=0, 且 f 有 Δ1TAr 表示, 则 g(x1,...,xn)=μy(f(x1,...,xn,y)=0) 同样有 Δ1TAr 表示.
证明. y=g(x1,...,xn) 由
f(x1,...,xn,y)=∅∧∀z∈y(f(x1,...,xn,y)=∅) 定义.
最后处理原始递归, 我们同样用哥德尔的巧妙技术来编码计算历史.
证明. 回忆定义.
1. | α(c,d,i)=μr(∃q<c(c=q×(1+d×(i+1))+r)) |
2. | J(a,b)=21(a+b)(a+b+1)+a |
3. | K(p)=μa<p(∃b<p(J(a,b)=p)∨J(a,p)=p), K(0)=0 |
4. | L(p)=μb<p(∃a<p(J(a,b)=p)), L(0)=0, L(1)=1 |
5. | β(s,i)=α(K(s),L(s),i) |
若 g(x1,...,xn) 和 h(x1,...,xn+2) 都是有 Δ1TAr 表示递归函数, 则它们原始递归生成的函数 f(x1,...,xn+1) 也是有 Δ1TAr 表示的递归函数.
证明. 令
F(x1,...,xm,y)=μs(β(s,0)=g(x1,...,xm)∧∀i∈y(β(s,Succ(i))=h(x1,...,xm,y,β(s,i)))), 以前的断言使它
Δ1TAr 可表示, 所以
f(x1,...,xn,xn+1)=β(F(x1,...,xn,xn+1),xn+1) 同样
Δ1TAr 可表示.
综合上述断言证毕.
特别地, 我们知道 Con(ZFC−(Inf)), Con(ReS) 和 Con(PA) 等价.