NIK WEAVER在理性机构的悖论上

卢克·穆罕沃斯:在韦弗(2013)你讨论了理性机构的一些悖论。你能解释哪些“悖论”是什么，对于可能不是熟悉可证明逻辑的人来说，这些“悖论”是什么？

NIK WEAVER.： 当然。首先，这些是“悖论”在高度逆行的意义上 - 它们并不完全矛盾。

它们都涉及基本呼吸困难，如果您在固定的公理系统中的原因，并且您知道某些语句A在S中可以证明，您通常无法推断A是真实的。亚博体育苹果app官方下载这可能是你和我愿意制作的推理，但如果你试图将它建造成一个正式的系统，那么系统变得不一致。亚博体育苹果app官方下载因此，对于指定的公理系统内的原因的理性剂，知道证据存在并不像实际上具有证据那么好。亚博体育苹果app官方下载

这导致了一些非常令人沮丧的后果。让我们说我想建立宇宙飞船，但首先我需要确保它不会爆炸。我有一个关于如何证明这一点的想法，但它非常繁琐，所以我编写一个程序来解决证明的细节并验证它是否正确。好消息是，当我运行该程序时，它会告诉我它能够成功填写详细信息。坏消息是，我现在知道船不会爆发的证据，但我仍然不知道这艘船不会爆发！我将必须自己检查证明，按行顺线。这是完全浪费时间，因为我知道程序正常运作（我们可以假设我已证明这一点），所以我知道一行一行的验证都是正确的，但我还是要这么做。

你可能会说我被编程得很糟糕。编写我的源代码的人应该允许我接受“有证据表明这艘船不会爆炸”，以此作为建造这艘船的充分理由。这可以是一个通用规则:对于任何语句a，让“存在a的一个证明”许可a许可的所有操作。我们并没有反驳Löb的定理，我们仍然不能从知道A的一个证明推导出A，但是我们通过规定知道A的一个证明就足够了来巧妙地处理它。但仍然存在问题。假设我可以证明，如果黎曼假设为真，那么飞船就不会爆炸，如果黎曼假设为假，那么就有证据证明飞船不会爆炸。那我就知道我的处境了任何一个a是真的或者有一个证据是真的，但我不知道哪一个。所以即使有了更自由的牌照条件，我仍然无法建立我可爱的宇宙飞船。

卢基：本文第2节开发了一种通过概念解决这种问题的方法保证断言。这是如何运作的？

尼克：“保证断言”是一种哲学术语，在数学环境中，指的是可以以完美理性的理由所置信的陈述。我的想法是，这一概念可以帮助这些Löbian类型问题，因为它比以某种方式更好，而不是正式可加速。例如，在任何一致的公理系统中，有一个语句A（n）的属性对于n的每个值，我们可以证明（亚博体育苹果app官方下载n），但对于所有n，a（n）没有单一证明““。但是，如果每个A（n）保证，则始终是“对于所有N，A（n）”也是保证的。

因此，我介绍了一个谓词框（a）来表达“a是保证的”，并给出了一个合适的公务化（这是一个小微妙），我表明我们可以随时推断出框（a）框（a）知道有一个证据。We still can’t infer A — Löb’s theorem is not violated — but, along the lines I suggested earlier, we can program our agents to accept Box(A) as licensing the same actions that A licenses. Thus, it suffices to prove that the statement “the ship won’t blow up” is warranted. If you go this route then all the paradoxes seem to disappear. If an agent is able to reason about warranted assertibility, then it gets to perform all the actions it intuitively ought to be allowed to perform.

卢基：在纸质中，你写道：

[Yudkowsky＆Herreshoff（2013年）]涉及正在寻求的理性代理商......一般许可委托给第二代理的行动绩效......在考虑修改自己的源代码的智能计算机的情况下，出现了相同的问题（为了使自己更聪明，说）。在这样做之前，它希望确保其后阳离子状态将正确理解，即，在修改后的任何定理实际应该是真实的。这进入了熟悉的Löbian困难，即代理商甚至无法确认其预先修正推理的声音。

在[Yudkowsky & Herreshoff(2013)]的第4节中，我们给出了一个独立行为者的无限序列的两个结构，每个结构都可以为激活下一个提供可证明的证明，但没有一个结构的演绎能力低于最初规定的水平。这些建筑很巧妙，但它们有一种不标准的味道。这可能是不可避免的，除非问题描述以某种基本方式改变。在这一节的剩余部分，我们提出另一种解决方案，使用非标准的论断推理。

您能否描述您继续展示的解决方案 - 再次，缺乏可证明逻辑中的背景可能能够理解，至少以直观的方式了解？

尼克： 我会尝试！首先，关于我的评论，只有非标准解决方案似乎可能，我应该提及现在由于Herreshoff，Fallenstein和Armstrong造成的定理这使得这种想法是精确的。重点是它不清楚我应该被允许建立自己的重复副本，并将我的目标委托给它，因为担心它会做同样的事情，并在AD Infinitum（“拖延问题”）。

现在，回到我的宇宙飞船榜样，让B成为船不会爆炸的声明。自信的基本特征是我们有一个普遍的法律，即暗示框（a），但我们没有交谈。所以框（b）比b“弱”，我的提议是我们应该允许我们的代理人接受Box（b）授权B所做的相同行动（建立宇宙飞船）。这有助于Löbian问题，因为B是可证明的陈述并不意味着B，但它确实暗示了盒子（b）。

但如果盒子（b）足够好，为什么不接受甚至较弱的声明框（框（b））？或盒子（框（b盒（b）））？让我写箱^ k（b）用k框。The idea about delegating tasks to successors is that if I am willing to accept Box^9(B), say, then I should be willing to build a successor who can’t accept Box^9(B) but can accept Box^8(B). I can reason that if my successor proves Box^8(B), then Box^8(B) is provable, and therefore Box^9(B) is true, which is good enough for me. Then my successor should be happy with a subsequent model that is required to prove Box^7(B), and so on. So we can create finite chains in this way, without doing anything nonstandard.

获得无限链的方法是引入非标准的“无限”自然数Kappa，并以验证框^ Kappa（b）所需的初始代理。然后它可以建立一个需要验证框^ {kappa - 1}（b）等所需的继承人。所得到的序列中的所有代理具有相同的正式强度，因为简单的换位（用kappa + 1替换kappa）将每个代理转换为其前身，而不会影响它们能够证明的东西。

卢基：现在让我询问这类类型的研究。亚博体育官网您如何有用的是如何有用的模型是什么？亚博体育官网它与当前构建实际软件代理的方法相当遥远。

尼克：是的，这是非常理论的，毫无疑问。一个模型是纯数学，其实际上是我的背景。在纯粹的数学中，我们正在研究没有任何直接实际应用的问题。我认为经验表明，这种工作偶尔会变得非常重要，而大多数情况下都没有，但这很难预测哪些方向会突然出来。

或者，你知道，也许我们都生活在尼克博斯特罗姆说的那样的模拟里面。在这种情况下，我们试图弄清楚如何帮助机器使自己更聪明的事实可能是对这种模拟性质的线索。

卢基：您认为一些“有前途的途径”是为了通过理性代理机构的“悖论”来推理我们的方式进行额外进展？

尼克： 我不知道。如果你在谈论呼吸障碍，我觉得我们当前的问题描述中缺少了重要的东西。在现在可以使用的指示中，我的偏好是对于Benja Fallenstein的参数多态性。但我也认为我们应该看看修改问题描述的方法。

卢基：您对理性机构悖论的兴趣是什么？

尼克：我一直在考虑周围的真理和循环的问题大约五年。（我刚检查过：我的最早的论文在2009年5月的数学arxiv发布了这个问题。）这是纯粹的理论上的工作，来自对数学和逻辑的基础的兴趣。

我对理性代理悖论的参与是由Eliezer Yudkowsky和Marcello Herreshoff的纸上的浮动障碍。事实上，我认为我从那篇论文中获得了“理性代理人的悖论”一词。当我读它时，我立即反应，我对分离性的想法应该是相关的，所以这就是我感兴趣的方式。

卢基：谢谢，尼克！