Deductrium的一些游玩指南
Deductrium的一些游玩指南。
注：这里记录的是最优解，也就是在尽可能少地消耗推理素
命题逻辑阶段
a1,a2阶段
记得去解锁进度层，获得1μg推理素
推理层会解锁mp, a1, a2两个推理规则
mp是$0>$1, $0 ⊢ $1 也就是说需要在定理列表中选择$0>$1和$0两个定理，然后就可以得到$1。 $0和$1是占位符，可以是任意一个命题，但是相同的占位符必须对应同一个命题。 mp相当于把$0>$1拆成$1
a1是$0>($1>$0),a2是($0>($1>$2)) > ($0>$1) > ($0>$2)。
#p是需要定理解锁的门。
第一个是a>a>a,不难发现使用a1,传入a a就可以了。
a>(a>a)>a,使用a1,传入a a>a，然后获得1μg。
推出a>a，使用a2 a a>a a得到(a>(a>a)>a)>(a>(a>a))>(a>a)，以及a1 a a>a得到a>((a>a)>a)
然后mp 前面得到的定理 后面得到的定理得到(a>(a>a)) > a>a，然后再用mp把a>a>a去掉就行了。
对b>b, (a>b)>(a>b)也是同样的道理，然后会获得2μg。 现在应该有4μg。
有个a>(c>(b>a))。
a1 a>(b)>a
a1 (b>a)>(c>(b>a))
a1[(b>a)>(c>(b>a)),a] (((b > a) > (c > (b > a))) > (a > ((b > a) > (c > (b > a)))))
mp 上一个，上两个 (a > ((b > a) > (c > (b > a))))
a2 [a, b>a, c>(b>a)] ((a > ((b > a) > (c > (b > a)))) > ((a > (b > a)) > (a > (c > (b > a)))))
然后就可以得到a>(c>b>a)
解锁录制宏,获得+8μg，然后旁边有个#d的门是⊢$0>$0 意思就是推理列表里有⊢$0>$0就可以通过。（#d提示那边可以获得1μg, 13）
我们先清空定理列表，开始证明⊢$0>$0，和a>a方法一样。证明完$0>$0后，点击录制宏按钮，得到第一个宏⊢$0>$0。可以解锁假设，后面可以获得1μg(14)。然后有一个$0>(($0>$1)>$0)，不要被他绕晕了，其实就是a1传入$0 $0>$1，可以获得2μg(16)。
接下来是假设的使用。 看到$0>($1>$2)⊢($0>$1) > ($0>$2)，⊢左边有$0>$1>$2.这里我们就可以假设$0>($1>$2)，在录制宏的时候这些假设会放到⊢旁边。
以下是$0>($1>$2)⊢($0>$1) > ($0>$2)的证明步骤:
hyp $0>($1>$2)
a2[$0,$1,$2] (($0 > ($1 > $2)) > (($0 > $1) > ($0 > $2)))
mp 1 0 ($0>$1)>($0>$2)
证明完后使用录制宏按钮录制宏，可以获得1μg(17)。
在2μg门（拆门）那里有一个门$0>($1>$2),$0>$1⊢$0>$2，证明步骤：
hyp $0>($1>$2)
hyp $0>$1
a2[$0,$1,$2] (($0 > ($1 > $2)) > (($0 > $1) > ($0 > $2)))
mp 2 0 (($0 > $1) > ($0 > $2))
mp 3 1 ($0 > $2)
可以获得1μg(18)，解锁拆门技能（通过一个门后该门会被移除）。绕到后面可以解锁否定定理a3和符号~。
接下来有些命题可能比较复杂，比如说$0>($0>$1)⊢$0>$1，证明步骤:
hyp $0>($0>$1)
a2[$0,$0,$1] (($0 > ($0 > $1)) > (($0 > $0) > ($0 > $1))) 这里比较巧妙。
之前的一个宏 $0>$0
依次执行 mp 1 0, mp 3 2得到($0 > $1)。
得到4μg(22)。
【这里就可以把$0>($1>$2),$0>$1⊢$0>$2删除了，基本上没啥用。$0>($0>$1)⊢$0>$1留着。】
否定阶段
介绍a3,(~$0>~$1)>($1>$0)，一个命题的逆否命题成立。
~~a>a有点难，双重否定表肯定。 我们先证明$0>$1,$1>$2 ⊢ $0>$2。利用a1可以得到$1>$2 > $0>$1>$2，拆解就可以得到$0>$2了。
我们可以录制一个~~$0>$0的宏
a1 (~~$0 > (~~~~$0 > ~~$0))
a3 ((~~~~$0 > ~~$0) > (~$0 > ~~~$0))
a3 ((~$0 > ~~~$0) > (~~$0 > $0))
不难发现有一个a>b>c>d的链条。接下来用（$0>$1,$1>$2 ⊢ $0>$2）拼成~~$0>(~~$0>$0)，就推出~~$0>$0了。
这里会获得一个奖励和序数有关，序数基底-1(-1)，以后会写成base-1。
这里证明$0>~~$0
~~~$0>~$0
((~~~$0 > ~$0) > ($0 > ~~$0))
$0>~~$0
很简单，得到5μg(27)
(~a>~a)>(a>a)可以使用a3传入a a就可以了。获得2μg(29)
~a>~~a ⊢ ~a>a用a3代入a, ~a就可以了。 获得2μg(31)。
接下来是$0>$1|-(~$1>~$0)，这里比较难。思路是先证明$0>$1 > (~~$0>~~$1)。
假设$0>$1,已知$1>~~$1，可以得出$0>~~$1,然后再用~~$0>$0，就可以得出~~$0>~~$1。最后用a3就可以得出~$1>~$0了。获得3μg(34)。
接下来是(($0 > $1) > (~$1 > ~$0))
这里有点狠，证明$0>$1 > ~~$0>~~$1。因为我们还没解锁演绎元定理，所以这里证明会很难。
这里可以强行证明。+10(44)
我们先回到a>a>a附近。有几个命题可以解决。 ~~a>(~~~~a>~~a)，+1(45)，然后之前证的可以+9(54)。(~~~~a>~~a) > (~a>~~~a)。 ~~a>(~~a>a)是之前的. ~~a>~~a > (~~a>a)可以+5(59),序数base-1(-2)
指南针那边序数base-1(-3),还有指南针
接下来没事干可以去序数，ω2可以去ω^2,ω17+7可以去ω^3
我们开始证明$0|-(~$0>$1)，以下是证明过程
+4(63)。
接下来证明a>(~a>b),以下是证明过程
+8(71)
接下来证明否定爆炸$0,~$0|-$1。用$0|-(~$0>$1)就可以了。 变体可以证明$0,~$0|-~$1和 ~$0,$0|-~$1, +4(75)
回到条件演绎元那边，证明($0>~~$1)|-($0>$1)，这里比较简单就不给出证明了。+5(80)，解锁条件演绎元定理。
接下来是$0>($1>$2),($0>($1>($2>$3)))|-($0>($1>$3))，乍一看很复杂，但是他可以简化成$2,($2>$3)|-($3)。 这里$2,($2>$3)|-($3)的证明很简单，不再叙述。
这里我们来讲mcdt的作用，简单来说，就是把a,b,….|-d，改写成$0>a, $0>b, ….|-$0>d。
利用这个操作，可以把$2,($2>$3)|-($3)改写成$0>($1>$2),($0>($1>($2>$3)))|-($0>($1>$3)),+10(90)。
回过头我们证明$0>($0>$1)>$1。证明如下（解锁了演绎元定理就很好搞了）,+5(95)
。
由于wxyhly补将亮新，所以我们直接强行证明(($0 > ($1 > $2)) > (($0 > ($1 > ($2 > $3))) > ($0 > ($1 > $3))))。 （这里需要先证明$0,($0>$1)|-($1)）
[$0>$1>$2] (($0 > ($1 > $2)) > ($0 > ($1 > $2)))
a1[$0>$1>$2, $0>$1>$2>$3] ($1 > ($2 > $3))
a1[(($0 > ($1 > $2)) > (($0 > ($1 > ($2 > $3))) > ($0 > ($1 > $2)))), $0>$1>$2] ((($0 > ($1 > $2)) > (($0 > ($1 > ($2 > $3))) > ($0 > ($1 > $2)))) > (($0 > ($1 > $2)) > (($0 > ($1 > $2)) > (($0 > ($1 > ($2 > $3))) > ($0 > ($1 > $2))))))
mp 2,1; cmp 3,0;
($0>$1>$2>$3)>($0>$1>$2>$3)
a1[($0>$1>$2>$3)>($0>$1>$2>$3), $0>$1>$2]
mp 6,5; cccc($0,($0>$1)|-($1)) 4, 7;
+1(96),解锁演绎元定理。演绎元定理就是a,b,…,z |- $0 变成a,b,… |- z>$0。
接下来是证明(~$0>~$1)|-($1>$0)，直接证明就完了，+1(97)。
回到深入#K那里，证明($0>~$1)>($1>~$0)。
这里假设$0>~$1。使用(~~$0 > $0)，拼接得到~~$0>~$1。
用a3得到((~~$0 > ~$1) > ($1 > ~$0))
可以得到($1>~$0)。
录制宏，用演绎元就可以了。
证明(~$0>$1)>(~$1>$0)。
这里假设~$0>$1。
根据$1>~~$1,得到~$0>~~$1。
用a3得到((~$0 > ~~$1) > (~$1 > $0))
可以得到(~$1>$0)。
录制宏，用演绎元就可以了。
拆完后得到#K(ω,K),+15(112)。这里我们能解锁一阶逻辑，但是先不要这样做。
我们还需要拆#L门，可以解锁完备性元定理。
到拆门技能那边，先证明~($0>$1)|-~$1。
a1 $1>($0>$1)
~~$1>$1
($0>$1)>(~~$0>$1)
把1,0拼接成~~$1>($0>$1)
把3,2拼接成(~~$1 > ~~($0 > $1))
a3[~$1,~($0>$1)], mp 5,4
(~($0 > $1) > ~$1)。
假设之后就可以了。
~($0>$1)|-$0。
>[$0|-(~$0>$1)] ~$0>(~~$0>$1)
c[$0>~~$0] ~$0>($0>~~$0)
c[$0>$1, $1>$2 |- $0>$2][1,0] (~$0 > ($0 > $1))
($0>$1)>~~($0>$1)
拼接2,3 (~$0 > ~~($0 > $1))
a3 ((~$0 > ~~($0 > $1)) > (~($0 > $1) > $0))
mp 5,4 (~($0 > $1) > $0)
可以解锁逻辑符号and和or。需要解锁<->才能用。
<>阶段
这里我们证明$0,~$1|-~($0 > $1)。
拆除了门<>(↔)，序数base-1((ω,K,<>(↔)),-4)。
回到门<>(↔)，解锁当且仅当。
右边有一些付费的元定理:逆演绎元和组合元。
对一个推理规则(dA)，逆演绎元相当于进行了如下操作
hyp dA的条件的第一项…最后一项
提取dA的结论中(infer P)>(???)， 假设P。
接着使用dA[a,b,c,….]，结果记作Q;
然后使用Q, P
就是结果。
举个例子，比如说a1($0>($1>$0))，<a1就是$0|-$1>$0。
回到门#<>(↔)那里，有一些推理规则要证明
a<>b拆解成a>b，使用~($0>$1)>$0结合。
a<>b拆解成b>a, 使用~($0>$1)>~$1结合。
a>b，b>a组合成a<>b, 使用$0,~$1|-~($0>$1)辅助构造。
$0>$1, $1>$0|-($0<>$1)，+10(122)。
a<>a，很简单，证明过程不再叙述，+10(132)。
$0<>$1|-$0>$1，+10(142)。
$0<>$1|-$1>$0，+10(152)。
接下来是$0<>$1 |-$1<>$0，拆解出来再组装回去就好了，+10(162)。
($0<>$1) <> ($1<>$0)，很简单，+10(172)
$0<>$1, $1<>$2 |-$0<>$2，传递，+10(182)。
$0<>~~$0，+10(192)。
接下来这个比较果糕。 $0<>$1|-(~~$0>$2)<>($1>$2)。 不难发现他是$0<>$1|- ($0>$2)<>($1>$2)的变体。
我们先证明$0<>$1|-, ($1>$2)>($0>$2)。
然后证明$0<>$1|-, ($0>$2)>($1>$2)。提示:$1>($0>$2)
到这里拼出来$0<>$1|-(~~$0>$2)<>($1>$2)了，然后证明$0<>$1|-(~~$0<>$1)。
证明完毕，+100(292)。旁边那个130μg的门是#L,就是解锁完备性原定理的最后一道门。
逻辑符号阶段
回到逻辑符号那里，
($0&$1)>~($0>~$1)，+10(302)。
~($0>~$1)>($0&$1)，+10(312)。
$0,$1|-($0&$1)，注意到$0,~~$1可以构建~($0>~$1)，秒了，+10(322)。
($0&$1)|-($0)，使用|-~($0>$1)>$0即可，+10(332)。
($0&$1)|-($1)，使用|-~($0>$1)>~$1即可，+10(342)。
($0&$1)|-($1&$0)，先把$0&$1拆成$1,$0再组装回去即可，+10(352).
($0&$1)&$2|-$0&($1&$2)，拆成$0,$1,$2再组装回去即可，+10(362)。
这里我们证明反证法： ~$0, ($1>$0) |- ~$1，使用$0>$1|-(~$1>~$0)即可。
~$0|-~($0&$1)，使用($0&$1)>$0然后反证法即可，+10(372)。
~$0|-~($1&$0)，+10(382)。
这里我们去解决一些遗留的命题,$0>($1>$2)>($1>$0>$2)。
hyp $0>($1>$2)
a1[$0>($1>$2), $1] (($0 > ($1 > $2)) > ($1 > ($0 > ($1 > $2))))
mp 1,0 $1>($0>($1>$2))
a1 $1>($0>$1)
ccmp 2,3 $1>($0>$2)
+20(402)。
(($0 | $1) > (~$0 > $1))，+10(412)。
((~$0 > $1) > ($0 | $1))，+10(422)。
$0|-$0|$1，用$0|-(~$0>$1)即可，+10(432)。
$1|-$0|$1，需要(~$0>$1) > (~$1>$0)），+10(442)。
$0|$0|-$0,可以构造出~$0>$0，这里证明(~$0>$0)>$0就可以了，+10(452)。
$0|$1 |- $1|$0,核心是((~$0 > $1) |- (~$1 > $0))，+10(462)。
($0|$1)|$2 |- $0|($1|$2)，这里不好证明。+10(472)
~$0,~$1|-~($0|$1)，先构造出~(~$0>$1)，然后反证法。+10(482)
接下来是(~$0|~$1)<>~($0&$1)。
首先是(~$0|~$1)>~($0&$1)
~($0&$1)>(~$0|~$1)
+10(492)。
接下来是p | ~p，很简单。+9，base-1(501,-5)
~(p&~p)，用反证法证明。+18,base-1(519,-6)
接下来是皮尔士定律。需要~($0>$1)>$0,($0>$1, ~$0>$1 |- $1), (~$0>~$1,~$0>$1 |-$0), (~$0>$0|-$0)，很简单，不给出过程。+50(569)
到#l3门那边，解决$a1<>$a2,$b1<>$b2|-($a1>$b1)<>($a2>$b2)，+24(593)。 还有上面的>改成<>的，+24(617)。
接下来是证明~(a>~b)>c <> a>(b>c)。 ~(a>~b)是a&b的变体，一部分是a&b>c|- a>(b>c)，a&b可以拆成(a>b>(a&b))，然后需要证明$0>$1>$2, $2>$3, $0|-$1>$3，证明完后就可以证明~(a>~b)>c > a>(b>c)。
接下来是证明a>(b>c) > ((a&b)>c)。 可以使用a>(b>c),a&b|- c解决。 然后再证明a&b>c |- ~(a>~b) >c。
至此证据链补足，就可以证明完a>(b>c) <> ((a&b)>c)了,+20(637)。
为了方便后续证明，这里我们需要一个如下的定理:($0>($1&~$1)) > ~$0，即X推出矛盾即X为假，反证法矛盾式，这里很简单证明。
剩下三个：
~($0<>$1)<>(~$0<>$1)
(~$0<>$1)>~($0<>$1)
首先假设~$0<>$1和$0<>$1。
假设$0：
拆解两个<>发现：$0>$1>~$0。
因此$0>~$0。
拼接成$0&~$0。
根据上文的反证法矛盾式，我们得到在(~$0<>$1),~$0<>$1的情况下$0|-$0&~$0。 利用同样的方法可以证明(~$0<>$1),~$0<>$1的情况下~$0|-~$0&~~$0。
可以构造矛盾~$0和~~$0，因此~($0<>$1)。 综上(~$0<>$1)>~($0<>$1)。
~($0<>$1)>(~$0<>$1)，可以先证明~$0>$1,然后$1>~$0。
首先假设~($0<>$1),~$0, ~$1。经过一些神秘的构造(要用$0|-~$0>$1)后发现有矛盾，叉出去。
所以~($0<>$1)|-~$0>$1。
接下来是~($0<>$1)|-$1>~$0，
这里我们要先证明$0<>$1|-~$0<>~$1（另外~$0<>~$1|-$0<>$1），很简单，这里不写出过程。
假设$1,$0。我们可以通过$0|-~$0>$1得到~$0<>~$1，然后$0<>$1，可以发现矛盾，叉出去。
所以~($0<>$1)|-$1>~$0。
所以~($0<>$1)|-(~$0<>$1) （作者写到这里的时候游戏不小心证明反了） 整理得~($0<>$1)<>(~$0<>$1)
$a1<>$a2,$b1<>$b2|-($a1&$b1)<>($a2&$b2)，很简单,解锁#l3(ω,K,<>(↔),l3)，+29(666)。
接下来是$a1<>$a2,$b1<>$b2|-($a1|$b1)<>($a2|$b2)。
我们需要证明$0>$2,$1>$2|-($0|$1)>$2。
首先是$a1<>$a2,$b1<>$b2,($a1|$b1)|-($a2|$b2)。根据构造不难发现$a1>($a2|$b2)[$a1>$a2],$b1>($a2|$b2)[$b1>~$b2]。因此$a1<>$a2,$b1<>$b2,($a1|$b1)|-($a2|$b2)。
反向的也是。
至此证明$a1<>$a2,$b1<>$b2|-($a1|$b1)<>($a2|$b2)。+29(695)。
接下来是 (b>a),(c>a)|-(a&b<>a&c)<>(b<>c)，+37(732)。
(b>~a),(c>~a)|-(a|b<>a|c)<>(b<>c)，+37(769)。
至此命题逻辑阶段已完成。
一阶逻辑阶段
全是量词
消耗100μg推理素(669+100)，解锁一阶逻辑。
a4:(V$0:$1)>#rp($1 $0>$2)，对于一个V$0:$1，可以把$1中的$0变量替换成$2。
a5: ((V$0: ($1 > $2)) > ((V$0: $1) > (V$0: $2))), 我也不知道这是啥
a6: 如果一个表达式没有$0,那么可以加上V$0。
接下来是V$2:($0>($1>$0))，对a1使用mq(va1)即可。
V$0:$1 > $1，对a4传入$0,$1,$0即可。解锁等词公理a8（现在不能直接用）。
Vx:x@y > Vx:x@y，直接用$0>$0即可（Vx:x@y），解锁等词公理a7和量词符号Exists。
Vx:x=x,va7即可，+10（679+100）。
接下来是$0=$1|-$1=$0。
a8的作用是传入$0=$1,可以把$2中的部分$0替换成$1。
例如$0=$0，可以使用$0=$1，将$0=$0的前一个$0变成$1=$0。
这个是等号的一个基本性质,+30(709+100)。
$0=$1,$1=$2|-$0=$2,用$1=$2把$0=$1的后一个$1替换即可。
为了准备级后期的通关，这里先消耗一些推理素。
回到推理层符号那边,-101(608+201),base-1(-7)，解锁常见命题逻辑大礼包
公理a4解读那边-100(508+301)，base-1(-8)，解锁条件概括元定理。
接下来是V$0:($1&$2) <> (V$0:$1)&(V$0:$2)，使用.<>, v.&，v.&1和v.&2即可。+40(548+301)
接下来是(V$0:V$1:$2) > $2，用a5脱掉外壳即可。-100+40(448+401),base-1(-9)，解锁概括元定理。
概括元定理说的是只要条件和结果里没有$#0，直接就可以V$#0:xxx，是a6的变式。
回到一阶逻辑大礼包，处理一些：
(V$0: ($1 & #nf($2, $0))) <> (V$0: ($1)) & (#nf($2,$0))
从左到右，用v.&1和v.&2, a4就可以拆出来。
从右到左，((V$0: $1) & #nf($2, $0))拆出来(V$0: $1)和#nf($2, $0)(a6得到V$0:#nf($2,$0))，组合。
接下来是$a1=$a2,$b1=$b2|-($a1@$b1)<>($a2@$b2)，a8乱用就行了。
接下来是(V$0: ($1 > #nf($2, $0)))<>(E$0:$1)>#nf($2,$0)，很简单。
| .E | 可以解锁门#l2(ω,K,<>(↔),l3,l2),+123（571+401） |
((V$2: ($0 <> $1)) > ((V$2: $0) <> (V$2: $1)))解锁门#l1(ω,K,<>(↔),l3,l2,l1),+1000(1571+401)，解锁互推替换元定理。
ZFC,Peano,Type Theory并行
-100(1471+501)，解锁皮亚诺公理，ZFC集合论外延公理，类型层。
首先证明((V$0: ($1 > $2)) ⊢ ((V$0: $1) > (V$0: $2)))（记住这个东西，后面有用，这里记作s31）
接下来是(Vx: (Vy: ((Vz: ((z @ x) <> (z @ y))) > (x = y))))：
(Vx: (Vy: ((Vz: ~(((z @ x) > (z @ y)) > ~((z @ y) > (z @ x)))) > (x = y))))
vvvd<>1, (Vx: (Vy: (Vz: (((z @ x) <> (z @ y)) > ~(((z @ x) > (z @ y)) > ~((z @ y) > (z @ x)))))))
vvs31[1] (Vx: (Vy: ((Vz: ((z @ x) <> (z @ y))) > (Vz: ~(((z @ x) > (z @ y)) > ~((z @ y) > (z @ x)))))))
vv.t[2,0] (Vx: (Vy: ((Vz: ((z @ x) <> (z @ y))) > (x = y))))
证明完后解锁分离公理，谓词包含符号。
这里先放一下ZFC，玩一下Peano和类型论。
首先有个U，直接在定理列表中输入True或False。然后与后面有U2，直接输入U1即可，+333(1804+501)（注意U9007199254740992的类型等于自身）
False解不了，跳过
True，找到对应的类型，输入true。
接下来是
Lx:True.true
Lx:False.x
La:U.a
La:U,Lx:a,x(+1000, 2804+501)
Lx:True,Ly:False,x
La:U,Lb:U,Lx:a,Ly:b,x，解锁简写非依赖函数类型符号“→”（->）
La:U,Lb:U,Lc:U,Lx:a,Ly:b,x
(λa:U.(λb:U.(λc:U.(λh’:(a→(b→c)).(λh’’:(a→b).(λh’’‘:a.((h’ h’’’) (h’’ h’’’)))))))) 对应 Pa:U,Pb:U,Pc:U,(a->b->c)->(a->b)->(a->c)
解锁简写否定符号not
左边的Pa:U,((not (not a))->a)不可证明，
(λa:U.(λh’:a.(λh’’:(a→False).(h’’ h’)))) 对应 (Πa:U,(a→(not (not a))))
(λa:U.(λb:U.(λh’:(a→b).(λh’’:(b→False).(λh’’‘:a.(h’’ (h’ h’’’))))))) 对应 (Πa:U,(Πb:U,((a→b)→((not b)→(not a)))))
(λa:U.(λh’:(((a→False)→False)→False).(λh’‘:a.(h’ (λh’’’:(a→False).(h’’’ h’’)))))) 对应 (Πa:U,((not (not (not a)))→(not a)))
解锁相等类型
rfl:((eq (refl true)) (refl true))，解锁自然数nat类型，Bool类型， ind_True, ind_False, ind_Bool
rfl:(eq true true)
rfl:(eq False False), +2000(4804+501)
rfl: (eq (False->False) (not False))，解锁rfl与相应证明策略（这里有点71高效，因为没解锁rfl就先用rfl）
rfl: (eq 0b 0b)，+1000（5804+501）
(λa:U.(λh’:False.((ind_False (λh’:False.a)) h’))) 对应 (Πa:U,(False→a))，+2000(7804+501)
(λh’:False.((ind_False (λh’:False.(eq 0b 1b))) h’)) 对应 False->(eq 0b 1b), +2000(9804+501)
ind_False主要是传入一个(x: False)=>????, 再传入一个False类型的变量，就可以证明一切（比如说eq (add 1 1) 3）。
OK，这里回去，到ZFC公理。
首先我们可以看到$0 < $0(这里的<是包含)。 第一次你可能会获得#nf($x,$0) < #nf($x,$0)这个神秘表达式，局部变量就是让#nf暂时“失效”，#nf($0,#x)会直接变成$0。我们就可以顺利得到$0<$0了,+30(9834+501)。
接下来是(x < y) > (y< z) > (x< z)。 利用前面两个可以推出(V#x: ((#x @ x) > (#x @ y)))和(V#x: ((#x @ y) > (#x @ z))),用v.t,+50(9884+501)
接下来是x < y, y < x 则x=y。 我们可以得到(Vz: ((z @ x) > (z @ y)))和(Vz: ((z @ y) > (z @ x)))，得到(Vz: ((z @ x) <> (z @ y)))，可以应用( ⊢ (Vx: (Vy: ((Vz: ((z @ x) <> (z @ y))) > (x = y)))))。
这时候化简到((Vz: ((z @ x) <> (z @ y))) > (x = y))，就可以得到x=y了。+150(10034+501)
这里由于某些原因我们可以使用< a1, < a3, < a4和< a6。
($x < $y) & ($y < $x) > $x=$y,这里按左边的提示就可以了,+198(10232+501)。
接下来是分离公理( ⊢ (∀#nf($x$y,$z):¬(∀#nf($y$x,$z):¬(∀#nf($z$x,$y):¬(((#nf($z$x,$y)∈#nf($y$x,$z))→¬((#nf($z$x,$y)∈#nf($x$y,$z))→¬#nf($0$y)))→¬(¬((#nf($z$x,$y)∈#nf($x$y,$z))→¬#nf($0$y))→(#nf($z$x,$y)∈#nf($y$x,$z))))))))，
“对任意集合x和任意对x的元素有定义的逻辑谓词P(z)，存在集合y，使z∈y当且仅当z∈x而且P(z)为真”。
由分离公理模式可以简单地由任何集合的存在性证明空集公理，只要使P(z)为矛盾式。