Steam Community :: Guide :: Prove You Can Win 全成就指南

Store Page

Prove You Can Win

All Discussions Screenshots Artwork Broadcasts Videos News Guides Reviews

Prove You Can Win > Guides > lxqd小理鱼呀's Guides

Not enough ratings

Prove You Can Win 全成就指南

By lxqd小理鱼呀

Prove You Can Win 全成就指南

Award

Created by

lxqd小理鱼呀
Offline

Category: Achievements, Gameplay Basics, Walkthroughs

Languages: Simplified Chinese

Posted

Updated

6 May @ 11:50am

6 May @ 4:20pm

42	Unique Visitors
2	Current Favorites

Guide Index

Overview

优化游玩体验

命题逻辑知识

模板代码

开放题

非开放题

Comments

优化游玩体验

请先参阅游戏中的"显示"->"盲点"，里面有写玩家可能会忽略的功能。这里说两个我认为最能显著优化游玩体验的地方。

自定义名称

相比于令人难以记住的rule几点几，我更喜欢重命名这些rule。以下是我的重命名方式（可直接复制）：

add, rule1.1; subchain, rule1.2; cut, rule1.3; initial_single_key, rule2.1; flow, rule2.2; key_once_open, rule2.3; contradiction, rule3.1; disconnected, axiom2; useless_lock, rule3.2; useless_key, rule3.3; inout_check, axiom3; enlarge_range, rule4.1; two_range, rule4.2; replace, rule4.3; vertex_range, rule4.4; tautology, axiom4; condition_holds, rule5.1; by_contradiction, rule5.2; out_to_not, rule5.3; add_any, rule5.4; not_any, rule5.5; in_particular, rule5.6; brute_force, axiom5; useless_vertex, rule6.1;

自定义名称的位置：进入主界面，然后一直点位于屏幕左侧的左箭头←，直到点到头。

步骤编号

步骤编号可以是负整数，例如-1表示上一步，-2表示上两步，等等。负整数的好处在于它记录的是相对位置。如果之后想要作相似的证明想要复制代码，负整数编号会使得代码基本不需要因为行数改变而改动。

命题逻辑知识

几个重言式

第四章命题的证明会涉及到大量的重言式。在本科的数理逻辑课上会积累海量的重言式，但由于我个人不喜欢记忆东西，实际上我没有记住几个。当然，知道的重言式越多肯定越好，但实际上就我的数学学习经验而言，掌握以下几个重言式，不论是对于数学（非逻辑方向）还是对于这个游戏都足够用了。以下是我记忆中最重要的四部分：

或、且与蕴含的转化

(p蕴含q) 等价于 ((非p)或q)
从而，(非(p蕴含q)) 等价于 (p且(非q)) 。这是利用反证法证明蕴含命题的基础。

上述是将蕴含转化为或与且。下面描述反方向的，即从或与且转化到蕴含。有时它更有用，因为蕴含是最重要的，它会结合rule5.1来推出真正想要的东西。

(p或q) 等价于 ((非p)蕴含q)
(p且q) 等价于非(p蕴含(非q))

连续蕴含：Currying

以下重言式从左到右叫currying,从右到左叫uncurrying。这是我最喜欢的重言式。

((p且q)蕴含r) 等价于 (p蕴含(q蕴含r))

currying有用之处在于将含有且的表达式转化为连续的蕴含，而连续的蕴含搭配rule5.1更有用。

或、且关于非的对偶：De Morgan's law

非(p或q) 等价于 ((非p)且(非q))
非(p且q) 等价于 ((非p)或(非q))

恒真、恒假与vacuous truth

恒真等价于 (p或(非p))
恒假等价于 (p且(非p))

vacuous truth是指：在命题"p蕴含q"。如果条件p本身假，那么整个命题"p蕴含q"便自动真。结合上面说过的关于恒假的描述，我们获得了一个重言式：

(p且(非p))蕴含q

模板代码

利用反证法证明蕴含命题

对于形如p蕴含q的命题，最好的策略是反证法。"p蕴含q"的否定是p且(非q)。

以下提供利用反证法证明蕴含命题的模板代码。假定目标goal()是p蕴含q的形式。一上来直接先复制粘贴如下代码：

assumption(not(goal())); tautology(imp(not(imp(p(1),p(2))),and(p(1),not(p(2)))),operand(goal(),1),operand(goal(),2)); condition_holds(1,2); tautology(imp(and(p(1),p(2)),p(1)),operand(step(-1),1),operand(step(-1),2)); tautology(imp(and(p(1),p(2)),p(2)),operand(step(-2),1),operand(step(-2),2)); condition_holds(-3,-2); condition_holds(-4,-2);

此时，你看到的倒数第二行便是p，倒数第一行便是(非q)。你的任务便是要推出矛盾 (下述...处自行填写）：

by_contradiction(1, ... , ...);

推出矛盾后，紧跟着直接复制下面代码便证明成功。

tautology(imp(imp(and(p(1),p(2)),p(3)),imp(p(1),imp(p(2),p(3)))),operand(operand(step(-1),1),1),operand(operand(step(-1),1),2),operand(step(-1),2)); condition_holds(-2,-1);

关于"并非"与"不属于/不能过关"

这个游戏里有两个"否定"的概念。它们分别是：

"真正通用的否定"：并非
"只对顶点/关卡起作用的否定"：不属于/不能过关

从"不属于/不能过关"转化到"并非"

请使用rule5.3。

在rule5.3之前，我们不能从"不属于/不能过关"转化到"并非"。因此，命题5.9不可证明，可直接跳过。

从"并非"转化到"不属于/不能过关"

假设第n步你得到了这样的命题："并非x(1)属于{x(2)}"。现在想要得到"x(1)不属于{x(2)}"。请复制粘贴如下代码（注意改动n，x(1)，x(2)的值！）

assumption(in(x(1),{x(2)})); tautology(imp(p(1),imp(not(p(1)),p(2))),step(-1),in(0,{})); tautology(imp(p(1),imp(not(p(1)),p(2))),step(-2),out(0,{})); condition_holds(-3,-2); condition_holds(-4,-2); condition_holds(n,-2); condition_holds(n,-2); contradiction(-7,-2,-1);

证明空关卡不能过关（命题3.3）

直接复制如下代码：

assumption(beatable([{},<>])); add(-1,1); add(-1,2); disconnected(1,2); contradiction(-4,-2,-1);

颠倒（命题4.11, 6.11）

假设第n步你得到了这样的命题："x(1)属于{x(2)}"。现在想要得到"x(2)属于[x(1)}"。请复制粘贴如下代码（注意改动n，x(1)，x(2)的值！）

assumption(out(x(2),{x(1)})); replace(n,-1); replace(n,-3); contradiction(-3,-2,-1);

开放题

不可能证明的开放题列表

命题1.5 不可能证明的原因：该关卡不能过关。
命题3.10 不可能证明的原因：为了证明带一次性钥匙的关卡不能过关，需要用到rule3.3。但rule3.3的要求是带钥匙的顶点需要能通到w。因此，需要一直保留住通路1--w，直到使用rule3.3在顶点1上加上钥匙K*(0)。但一旦你保留住通路1--w，注意到关卡还有一个通路0--1，这就构成了0--1--w，它就可以过关了，与它本来不能过关矛盾。也就是说，为了能够使用rule3.3，一定其中会有某一步破坏了它与原来关卡的等价性。
命题4.5 不可能证明的原因：该命题错误。有可能x(2)=x(4)，这将导致x(1)可能不属于x(3)。
命题5.9 不可能证明的原因：关于"并非与不属于/不能过关"，前者能够推出后者是由于axiom4和rule5.1的存在，我们可以使用vacuous truth（(p且非p)推出q）使得在同时假设"某个命题"与"并非某个命题"的时候可以推出任何命题，特别地可以推出不属于/不能过关。但不引入rule5.3的情况下后者推不出前者，因为预先地"不属于/不能过关"并不是语义上"属于/能过关"的否定，axiom4对其不起作用。我们可操作的是能从同时假设"属于"与"不属于"的情况下推出某类指定类型的命题，但"并非..."并不属于那种指定的类型。
命题5.20 不可能证明的原因：没有rule5.6这样的将一个变量的值代入命题的规则。因为你如果要证明一个存在性命题，你就要代入一个特别的值发现它成立。但没有代入规则你就做不了这件事。有些做过命题5.24的会觉得既然rule5.4有错误那它应该能推出任何命题，而命题5.20的时候是可以用rule5.4的，所以有些人会认为命题5.20可以证明。但事实上，在你证明命题5.24的时候必然会用rule5.6。实际上尽管直觉上rule5.4"有误"，但从可操作的层面来讲，只有将rule5.4与rule5.6搭配起来才"有误"。

可做的开放题的解法提示

命题2.8 第二个关卡可以过关。加东西的顺序：4处的钥匙K(0)---后面的两把锁---一次性钥匙与最前面的那把锁。
命题4.14 用反证法。利用rule4.4可以限制x(1),x(2)的范围{0,w}，并结合w--w--w--w不能过关导出矛盾。
命题4.17 两个关卡过关的充要条件是三个顶点中至少有一个0和至少有一个w，而这是与钥匙无关的条件。因此，可以利用这个与钥匙无关的充要条件作为桥梁。
命题5.6 使用重言式 (p蕴含(q蕴含(p且q)))。这个重言式背后的原理是前文提过的currying。
命题5.10 先做命题5.11，并利用前文提过的"或与蕴含的转化"将命题5.11的蕴含形式转化成本命题的或形式。
命题5.11 参见前文提到的"从"并非"转化到"不属于/不能过关"的模板代码。
命题6.6 用axiom1从0开始连接所有顶点（注意是所有）直到最后的w，然后用rule1.3和rule1.2。
命题6.7 与命题6.6一样"一笔画"，只不过最开始axiom1的时候就要加钥匙，然后中途加锁。
命题6.8 用反证法。先与命题6.6一样用"一笔画"证明{0--w,w--1,1--2}能过关，然后w上加一次性钥匙同时w--1上加锁，再将w处的一次性钥匙转移到0处，则此时还是能过关的。但在反证法的假设下可以证明此时不能过关，矛盾。
命题6.14 用反证法。假设不能过关的前提下证明x(1)不属于{0,w}。然后证明不带钥匙的{x(1)--x(1)--w}不能过关。最后加上钥匙并拿掉x(1)--w。

非开放题

反正估计没人看，我就懒得写了。如果有人在这里留言问哪个题怎么解再更新那个题。

1 Comments

< >

zqh——123 [developer] 6 May @ 11:27pm

非常详细，点赞了。感觉列出的这些模板代码会很有用。

< >