（若想正確察看數學文章，還請閱讀文後所附圖片，或索取pdf文檔）
§Φ4 等值性
(Φ4.1)設u≡mn、v≡mm為變元，p為自然數．則：
(1)如果n＜m，則說 u小於v，記作 u＜v ．
(2) 變元 u+vmn+m．
變元 upmn+p．
(Φ4.2)(1)設A為{u1…un}-公式．則u1…unA顯然是閉公式，稱為A的一個閉包．
(2)設A為{u1…un}-公式．如果
u1＜…＜un且freA＝{u1…un}，
則u1…unA是A的閉包，且由A唯一界定，稱為A的主閉包，記為 A ．
(3)設A,B為公式．如果
freA＝freB且[AB]，
則說 A,B等值，記作 AB ．
[Φ4.3]等值關係是「等價關係」．即：設A,B,C為公式．則：
[1](反身性)AA．
[2](對稱性)如果AB，則BA．
[3](傳遞性)如果ABC，則AC．
【證】◆2*AB1.fre A＝fre BU——把U的所有元排成u1＜…＜un．
任取「新的」互異個詞a1,…,an．
AB[AB] ＝u1…un[AB](())[AB]u1…un(a1…an)＝＝[Au1…un(a1…an)Bu1…un(a1…an)]H[Bu1…un(a1…an)Au1…un(a1…an)]＝[BA]u1…un(a1…an)((+))u1…un[BA]＝[BA](1)BA．l
(Φ4.4)在[F4.3]的證明◆2*中，所謂「新的」個詞，是指不在A,B中的個詞．
一般地，對於任意給定的有限多的詞——特別地，包括公式，我們總能找到任意有限多個不在其中的「新的」個詞以供使用；因為，只要令這種個詞足夠長即可．
今後，我們將常類似地引用「 新個詞」這一術語。自然，該術語的含義要由那裡的
上下文來確定．
[Φ4.5]設a,b為閉公式，A為公式，u1,…,un為變元，Q1,…,Qn,Q{,}．則：
[1]abaHb．
[2]如果諸uifre A，則Q1u1…QnunAA．特別，Q1u1…QnunaHa．
[3]設『i1…in』是『1…n』的全排列．則Qu1…unAQui1…uinA．
[4]如果a,b都是A的閉包，則aHb．
【證】◇2a設u為變元．則QuaHa分兩種情形：
cs[Ⅰ]「Q＝」任取新個詞a．
uaau(a)＝([F2.11][2])a1.uaa．
{[F2.11][2]}a＝au(a)aau(a)aua(1)uaHa．
cs[Ⅱ]「Q＝」auaH(cs[Ⅰ]) uaua2.uaa．
aua＝auaauaH(cs[Ⅰ])aaaua(2)uaHa．
◇2b設ufreA為變元．則QuAA
ufreA1.fre QuA＝freAK．
把K的所有元排成v1＜…＜vm，於是u≠vj．
任取互異新個詞a1,…,am．下面採用通項約定．
顯然Avj(aj)是閉公式(2a)QuAvj(aj)HAvj(aj)[QuAvj(aj)Avj(aj)]＝[QuAA]vj(aj)v1…vm[QuAA]＝[QuAA](1)QuAA．
◆2*由2b立得．
◇3a如果A是{u1…un}-公式，則Qu1…unAHQui1…uinA
任取互異新個詞a1,…,an．
u1…unAAu1…un(a1…an)＝Aui1…uin(ai1…ain)u1…unAui1…uinA且同理ui1…uinAu1…unA1.u1…unAHui1…uinA．
Au1…un(a1…an)＝Aui1…uin(ai1…ain)ui1…uinAu1…unAui1…uinA且同理ui1…uinAu1…unAu1…unAHui1…uinA(1)Qu1…unAHQui1…uinA．
◆3*可由3a證出，猶如2b之由2a證出．
◆4*寫a≡u1…unA，
A≡v1…vmA．
顯然{u1…un}{v1…vm}存在u′1,…,u′nm使：
áu′1…u′nmv1…vm＝áui1…uin，í『i1…in』是『1…n』的全排列．
A＝v1…vmAH([2])u′1…u′nmv1…vmAH([3],[1])u1…unA＝a且同理AHb．l
[Φ4.6]設A,B,A′,B′為公式，u為變元，a為個詞，*{,∧,∨,}，Q{,}．則：
[1]如果AA′，則AA′．
[2]如果AA′，BB′，則[A*B][A′*B′]．
[3]如果AA′，則QuAQuA′．
[4]如果AA′，則Au(a)A′u(a)．
【證】◇φa如果AA′，BB′，則[AB][A′B′]甚易，留給讀者．
◆φb[1]，[2]成立由φa易得．
◇φc設A,B為u-公式．則u[AB][uAuB]甚易，留給讀者．
◇φd如果AA′，則uAuA′
AA′fre A＝fre BU——把U的所有元排成u1＜…＜un．
任取互異新個詞a1,…,an．
分兩種情形：
cs[Ⅰ]「uU」．([F4.5][2])uAA且uA′A′(AA′)uAuA′．
cs[Ⅱ]「u≡ui0U」．把U\{u}的所有元排成v1＜…＜vn1．
對每公式X令：X*Xv1…vn1(a1…an1)．
AA′[AA′]＝u1…un[AA′]H([F4.5][3])v1…vn1u[AA′](u[AA′])*＝u[AA′]*＝u[A*A′*](φc)[uA*uA′*]＝[uAuA′]*v1…vn1[uAuA′]＝[uAuA′]uAuA′．
◆φe[3]成立由φd立得．
◆φf[4]成立令U及u1,…,un如φd．分兩種情形：
cs[Ⅰ]「uU」．([F2.11][1])Au(a)＝A且A′u(a)＝A′(AA′)欲證者．
cs[Ⅱ]「u≡ui0U」．令v1,…,vn1如φd之cs[Ⅱ]．
AA′[AA′]＝u1…un[AA′]H([F4.5][3])uv1…vn1[AA′](v1…vn1[AA′])u(a)＝v1…vn1[Au(a)A′u(a)]＝[Au(a)A′u(a)]欲證者．l
(Φ4.7)任給定公式A．我們歸納定義A的等值替換如下：
若A′A，則A′是A的等值替換．特別，A是其自身的等值替換．
若A′,B′分別是A,B的等值替換，則[A′*B′]是[A*B]的等值替換．
這裡，*{,∧,∨,}．
若A′是A的等值替換，則A′是A的等值替換．
若A′是A的等值替換，則QuA′是QuA的等值替換．
這裡，Q{,}，u是變元．
粗略地說，「A的等值替換」是指由將A中某些「子公式」換以與之等值的公式而得的公式．
[Φ4.8]設A,A′為公式．如果A′是A的等值替換，則A′A．（[F4.6]）
[Φ4.9]設A,B,C,A1,…,An為公式，a為閉公式，u1,…,un為變元．則：
[1](對合律)AA．
[2](交換律)A∧BB∧A；
A∨BB∨A．
[3](結合律)[A∧B]∧CA∧[B∧C]；
[A∨B]∨CA∨[B∨C]．
[4](分配律)A∧[B∨C][A∧B]∨[A∧C]；
A∨[B∧C][A∨B]∧[A∨C]．
[5](換位律)[AB][BA]．
[6](排中律)a∨a．
[7](DeMorgan律之一)[A1∧…∧An][A1∨…∨An]；
[A1∨…∨An][A1∧…∧An]．
[8](DeMorgan律之二)u1…unAu1…unA；
u1…unAu1…unA．
(Φ4.10)設A,B為公式，u1,…,un為互異變元，v1,…,vn為互異變元．在§附錄Ⅱ中，我們將證下列二條件等價——此時就說
A關於(u1…un;v1…vn)而等值於B，
記作
A
B，
或按通項約定而簡為
A
B．
二等價條件是：
(1°)存在不在A,B中的互異個詞a1,…,an使Au1…un(a1…an)Bv1…vn(a1…an)．
(2°)對不在A,B中的任互異個詞p1,…,pn皆立Au1…un(p1…pn)Bv1…vn(p1…pn)。
F本定義是(F4.2)(2)的推廣，即：
等值關係是這裡的n＝0時的特殊情形．
[Φ4.11]設A,B,A′,B′為公式，u1,…,un為互異變元，v1,…,vn為互異變元．則：
[1]假定freA＝freA′．如果A
A′，則AA′．
[2]如果A
A′，則A
A′．
[3]設*{,∧,∨,}．如果A
A′，B
B′，則[A*B]
[A′*B′]．
[4]設Q{,}，1≤k≤n．如果A
A′，則QukA關於(u1
…uk…un;v1…v
k…vn)而等值於QvkB．(「^」表示去掉該元素)．
【證】◆1*可令U＝freA＝freA′．
把U\{ui}的所有元排成u′1＜…＜u′m．
{如果}存在不在A,A′中的互異個詞a1,…,an使
1.Au1…un(a1…an)A′u1…un(a1…an)．
任取不在A,A′中的互異個詞b1,…,bm．
以下採用通項約定．
{1,[F4.6][4],[F4.5][1]}Aui(ai)u′j(bj)HA′ui(ai)u′j(bj)[Aui(ai)u′j(bj)A′ui(ai)u′j(bj)]＝[AA′]ui(ai)u′j(bj)＝[AA′]uiu′j(aibj)u1…unu′1…u′m[AA′]H([F4.5][3][1])[AA′] (1)AA′．
◇4a假定A是{ui}-公式，A′是{vi}-公式．如果A
A′，則unA
vnA′
任取互異新個詞a1,…,an．
G(unA)u1…un1(a1…an1)＝unAu1…un1(a1…an1)(())Au1…un(a1…an)HH(如果,假定,[F4.5][1])A′v1…vn(a1…an)((+))GvnA′v1…vn1(a1…an1)＝(vnA′)v1…vn1(a1…an1)D且同理DGGHD欲證者．
◆4b如果A
A′，則QunA
QvnA′分兩種情形：
cs[Ⅰ]「Q＝」可由4a證出，猶如[F4.5]的證明中的2b之由2a證出．
cs[Ⅱ]「Q＝」由cs[Ⅰ]及[2]立得．l
[Φ4.12](約束變元的無關性)設A,B為公式，u1,…,un為互異變元，v1,…,vn為互異變元，Q1,…,Qn{,}．如果AB，則
Q1u1…Qnu
nAQ1v1…QnvnB．
【證】由n次使用[F4.11][4]而得．l
[Φ4.13]設A,B為公式，u1,…,un為互異變元，a1,…,an為不在A,B中的互異個詞．
如果
freA＝freB，Au1…un(a1…an)HBu1…un(a1…an)，
則AB．
【證】由[F4.11][1]立得．l