（若想正确察看数学文章，还请阅读文后所附图片，或索取pdf文档）
§Φ5 函词与项伪公式
(Φ5.1)任给定变元u,v．则：
(1)设q为单纯项．我们定义单纯项qu[v]如下：
áauu[v]=v．
áb设w≠u为变元．则wu[v]=w．
ác设a为个词．则au[v]=a．
(2)对每公式A我们递归定义公式Au[v]如下：
设q,q′为单纯项．则(qq′)u[v]=qu[v]q′u[v]．
设A′,B′为公式．则[A′B′]u[v]=[A′u[v]B′u[v]]．
设A′为公式，w≠u为变元．则(wA′)u[v]=wA′u[v]．
设A′为公式．则(uA′)u[v]=uA′．
(Φ5.2)(1)设u1,u2为变元；令v是{u1,u2}的最小变元．则公式
u1u2v[vu1vu2]．
(2)设A为公式，u为变元；令v1,v2分别是不在A中的最小变元,次最小变元．则：
公式!!uAv1v2[Au[v1]∧Au[v2]v1v2]，
公式!uAuA∧!!uA．
[Φ5.3]设A为公式，u为变元，Q{,,!!,!}．则：
[1]freQuA＝freA\{u}．
[2]设v≠u为变元，a为个词．则(QvA)u(a)QvAu(a)．
[3]设a为个词．则(QuA)u(a)＝QuA．
[4]若A′A，则QuA′QuA．
显然，只须处理Q＝!!的情形．为不挤占正文版面，我们把它列于§附录Ⅲ．l
(Φ5.4)设A为áu1…unv-公式．则称3元序组áA,v,áu1…un为n元函词，并将此序组
记为A(u1…vun)．
(Φ5.5)我们归纳定义项的概念如下：
单纯项是项．
设为n元函词，s1,…,sn为项．则n+1元序组á,s1,…,sn是项，称为复合项，
并将此序组记为(s1…sn)。
根据“序组相等的充要条件”容易验证，本归纳定义是正则的．
注记1两序组áx1,…,xn,áy1,…,ym相等的充要条件是：n＝m且xi＝yi(i＝1,…,n)．
(Φ5.6)(1)对每个项s我们递归定义变元有限集vars如下：
设a为个词．则vara=．
设u为变元．则varu={u}．
设为n元函词，s1,…,sn为项．则var(s1…sn)=vars1∪…∪varsn．
vars的元称为s的实质变元．无实质变元的项称为闭项．
(2)设U为变元有限集，s为项．则：
如果varsU，则称s为一个U-项．
{u}-项íu是变元简称u-项．
{u1…un}-项í诸ui是互异变元称为áu1…un-项．
(3)设s1,…,sn为项．则变元有限集var(s1…sn)vars1∪…∪varsn．
(4)设s1,…,sn为项；
把var(s1…sn)的所有元排成v1＜…＜vm，并令k使v1+…+vm＝mk(见(F4.1)(2))．
则：
自然数
s1…sn
k，
公式t(s1…sn)[v1v1v1v1]∧…∧[vmvmvmvm]。
Ffret(s1…sn)＝var(s1…sn)．
注记2(4)中的t(s1…sn)是以var(s1…sn)为自由变元集的“永真”公式，引入它的目的后见．
(Φ5.7)(1)设X为自然数有限集．我们定义自然数maxX如下：
áamax=0．
áb如果X≠，则maxX=‘X中的最大元’．
(2)对每个项s我们递归定义s的层数，P(s)，如下：
设s为单纯项．则P(s)=0．
设(s1…sn)为项．则P((s1…sn))=max{P(s1),…,P(sn)}+1．
(3)设s1,…,sn为项．则P(s1…sn)=max{P(s1),…,P(sn)}．
(Φ5.8)(1)任给定变元u及闭项s．则对每个项s我们递归定义项su(s)如下：
(su(s)读作“把u＝s代入s而得的项”)
uu(s)=s．
设q≠u为单纯项．则qu(s)=q．
设(s1…sn)为项．则(s1…sn)u(s)=(s1u(s)…snu(s))．
(2)设s为项，u1,…,un为互异变元，s1,…,sn为闭项．则项
su1…un(s1…sn)su1(s1)…un(sn)。
施归纳于项s易证：若‘i1…in’是‘1…n’的全排列，则
sui1…uin(si1…sin)＝su1…un(s1…sn)．
[Φ5.9][1]设s为项，u为变元，s为闭项．则：
su(s)＝suvars．(施归纳于项s)
[1′](系)设s′,s为闭项，u为变元．则s′u(s)＝s′．
[Φ5.10]设s为项，u1,…,un为互异变元，s1,…,sn为闭项．则
varsu1…un(s1…sn)＝vars\{u1,…,un}．（只需施归纳于项s而证出n＝1的情形）
(Φ5.11)(1)我们归纳定义伪公式的概念如下：
设s,t为项．则序组ás,,t是伪公式，记为st．
设M1,M2为伪公式．则序组áM1,,M2是伪公式，记为[M1M2]．
设M为伪公式，u为变元．则序组áu,,M是伪公式，记为ΠuM．
根据序组相等的充要条件(即各相应坐标相等)易验证，本归纳定义是正则的．与[F2.4]的证明不同，这里正则性的证明要简单得多，因为我们是用3元序组来定义定义伪公式的．
(2)对每公式A我们递归定义伪公式corA如下：
设q1,q2为单纯项．则cor(q1q2)=q1q2．
设A1,A2为公式．则cor[A1A2]=[corA1corA2]．
设A0为公式，u为变元．则cor(uA0)=Πu(corA0)。
直觉地说，corA是指由将A中所有的,,分别换以,,Π而得的伪公式．
(Φ5.12)对每伪公式M我们递归定义公式cor1M如下：
设q1,q2为单纯项．则cor1(q1q2)=q1q2．
设s,t为项但不全为单纯项．则cor1(st)=m1m1(也可规定为任何其它的公式)．
设M1,M2为伪公式．则cor1[M1M2]=[cor1M1cor1M2]．
设M为伪公式，u为变元．则cor1(ΠuM)=u(cor1M)．
[Φ5.13][1]设A为公式．则cor1(corA)＝A．
[2]设A,B为公式．若A≠B则corA≠corB．
◆1*施归纳于公式A．
◆2a如果corA＝corB，则A＝B
corA＝corBcor1(corA)＝cor1(corB)([1])A＝B．l
(Φ5.14)形如corA的伪公式，íA是公式，称为仿公式．
为方便计，我们将依[F5.13][2]而把‘公式’与‘仿公式’等同起来．
(Φ5.15)对每伪公式M我们递归定义变元有限集freM如下：
设s,t为项．则fre(st)=var(st)．
设M1,M2为伪公式．则fre[M1M2]=freM1∪freM2．
设M为伪公式，u为变元．则fre(ΠuM)=freM\{u}。
F对每公式A皆立fre(corA)＝freA(施归纳于公式A)．因此，本定义确是(F2.5)(1)的推广．
(Φ5.16)(1)设q为单纯项，u1,…,un为互异变元，s1,…,sn为项．则
sk(当q＝uk，1≤k≤n)
q(当q{ui})。
显然，若s1,…,sn是闭项则qu1…un[s1,…,sn]＝qu1…un(s1,…,sn)．
(2)所谓代入组，是指形如
áA,áu1,…,un,ás1,…,sn
的3元序组，其中：A是公式，u1,…,un是互异变元，s1,…,sn是项．
(3)对每代入组A≡áA,áu1,…,un,ás1,…,sn我们递归定义伪公式
substA＝Au1…un[s1…sn]
如下：
设q,q′为单纯项，u1,…,un是互异变元，s1,…,sn是项．则
(qq′)u1…un[s1…sn]=qu1…un[s1…sn]q′u1…un[s1…sn]．
设A′,B′为公式，u1,…,un是互异变元，s1,…,sn是项．则
[A′B′]u1…un[s1…sn]=[A′u1…un[s1…sn]B′u1…un[s1…sn]]．
设A′为公式，u1,…,un是互异变元，s1,…,sn是项，v{ui}为变元．则
(vA′)u1…un[s1…sn]=ΠvA′u1…un[s1…sn]．
设A′为公式，u1,…,un是互异变元，s1,…,sn是项，1≤k≤n．则
(ukA′)u1…un[s1…sn]=ΠukA′u1…u^k…un[s1…s^k…sn]。
本递归定义的合法性是由其唯一生成性命题之成立所确保的．该命题是：
设A为代入组，则下列四条件恰有一个成立：
(a°)存在唯一的单纯项q,q′，互异变元u1,…,un，项s1,…,sn，使
A＝áqq′,áu1,…,un,ás1,…,sn．
(b°),(c°)（省略）．
(d°)存在唯一的公式A′，互异变元u1,…,un，项s1,…,sn，自然数k：1≤k≤n，使
A＝áukA′,áu1,…,un,ás1,…,sn。
由公式之归纳定义的正则性[F2.4]易看出，此唯一生成性命题确实成立．
注意：本定义不能仿照(F2.6)(1)进行——那里的u,a是预先设定的，而这里ui,si，由于④中之右式的缘故，不能预先设定；另外，也不能依照(F2.6)(2)进行——事实上，伪公式Au1…un[s1…sn]与Au1[s1]…un[sn]不必相等．
[Φ5.17]设áA,áu1…un,ás1…sn为代入组．则：
[1]设‘i1…in’是‘1…n’的全排列．则Aui1…uin[si1…sin]＝Au1…un[s1…sn]．
[2]存在Xvar(s1…sn)使：freAu1…un[s1…sn]＝(freA\{ui})∪X．
◆1*施归纳于公式A．
◆2a把适合“uifreA”的所有i排成k1,…,km．则
freAu1…un[s1…sn]＝(freA\{ui})∪var(sk1…skm)
施归纳于公式A．l
(Φ5.18)(1)任给定自然数n．则对每公式A我们递归定义公式An如下：
设a,b为个词，u,v为变元．则：
(ab)n=ab，(au)n=aun，(ua)n=una，(uv)n=unvn．(见(F4.1)(2))
设A′，B′为公式．则[A′B′]n=[A′nB′n]．
设A′为公式，u为变元．则(uA′)n=unA′n．
(2)设áA,áu1…un,ás1…sn为代入组；令k＝
s1…sn
．则
伪公式Au1…unás1…snAku1k…unk[s1…sn]．
[Φ5.19]设áA,áu1…un,ás1…sn为代入组，‘i1…in’是‘1…n’的全排列．则
Aui1…uinási1…sin＝Au1…unás1…sn．
由[F5.17][1]立得．l
(Φ5.20)设A为公式，u为变元；令v0,v1分别是≠u的最小变元,次最小变元．则公式
A!u[!uAA]∧[!uAv0[v1(v0v1)v0u]]．
[Φ5.21][1]设A为公式，u为变元．则freA!u＝freA∪{u}．
[2]设A为áu1…unv-公式．则u1…un!vA!v．
[1]是显然的．[2]的证明列于§附录Ⅳ．l
(Φ5.22)对每伪公式M我们递归定义伪公式Mw如下：
设q1,q2为单纯项．则(q1q2)w=q1q2．
设≡A(u1…vun)为函词，q为单纯项，s1,…,sn为项．则：
(q(s1…sn))w=[t(qs1…sn)Πv0[A!vu1…unvás1…snv0qv0]]，
((s1…sn)q)w=[t(s1…snq)Πv0[A!vu1…unvás1…snv0qv0]]．
其中，v0是var(qs1…sn)的最小变元．
设≡A(u1…vun)及g≡B(x1…yxm)为函词，s1,…,sn,t1,…,tm为项．则：
((s1…sn)g(t1…tm))w=
[t(s1…snt1…tm)Πv0v1[A!vu1…unvás1…snv0[B!yx1…xmyát1…tmv1v0v1]]]．
其中，v0,v1分别是var(s1…snt1…tm)的最小变元,次最小变元．
设M1,M2为伪公式．则[M1M2]w=[M1wM2w]．
设M0为伪公式，u为变元．则(ΠuM0)w=ΠuM0w。
F对于仿公式A——或由(F5.14)而等同地——公式A，我们有：
Aw＝A．
注记3t(…)虽是公式，但在本定义中却理解为它所对应的仿公式．
注记4定义中引入的t(…)(见(F5.6)(4))并非多余，它是为了增加必要的自由变元；若删掉它，则下面的[F5.23]中的“＝”就只能减弱为“”，这不好．
[Φ5.23]设M为伪公式．则freMw＝freM．
◇φa设A为公式，u1,…,un为变元．如果freA＝{u1…un}，则
freAk＝{u1k…unk}
(施归纳于公式A)．
◇φb设áA,áu1…un,ás1…sn为代入组．如果freA{u1…un}，则
freAu1…unás1…snvar(s1…sn)
令k
s1…sn
．
{如果,φa}freAk{uik}1.freAk\{uik}＝．
lt＝freAku1k…unk[s1…sn]([F5.17][2])(freAk\{uik})∪var(s1…sn)＝(1)var(s1…sn)．
◆φ*施归纳于伪公式M——奠基处要用φb及[F5.21][1]．l
(Φ5.24)(1)设M为伪公式．施归纳于M易证存在n使
Mw…w是仿公式
——此种n的最小者记为m
(M)．
(2)设M为伪公式．显然，Mw
…w在n≥m(M)时是不变的仿公式，或由(F5.14)，它
也可视为公式．我们把它记为MW．
[Φ5.25]设M为伪公式，n为自然数．则：
[1]如果Mw…w是
公式，则它＝MW．
[2](Mw)W＝MW．
[3]freMW＝freM．
[1]为显然．[2]由[1]立得．[3]由[F5.23]立得．l