什么是逻辑形式系统? - Sam

22-09-14 banq

为什么上学目的是为了辨别哪些理论是在胡说八道?
为什么数学家和物理学家可以在纸上写一些有趣的符号,对它们进行逻辑运算,产生一些新的有趣的符号排列,并确信这些新的符号实际上告诉他们一些关于宇宙的真实情况?(注意,并不是因为他们已经成为数学家或物理学家,他们的话才是真的)

这些需要掌握逻辑的形式系统(formal system)。

一个形式系统由以下部分组成:
  • 一个可允许的字符的集合,我们可以用它来组成字符串(字符序列)。
  • 一个被称为 "公理 "的字符串的集合
  • 一组规则,或称 "推理规则",用于将一些字符串变为其他字符串。

让我们从一个简单的、无意义的例子开始,这个例子叫做MIU-系统。

MIU-系统:

1、允许的字符:
“M”、“I”和“U”三个字符(所以字符串可以是它们的组合,如“M”、“UMM”、“MIMMIUM”、“UMIIMUMUUIMIM”等等。)

2、公理:
MI

3、规则:

规则一:
给定一个以“I”结尾的字符串,你可以在结尾处加一个“U”。
例子:从“UMI”出发,形成“UMIU”

规则二:
给定一个“Mx”形式的字符串,其中“x”由“M”、“I”和“U”组成,你可以组成“Mxx”字符串
例子:从“MIU”,形成“MIUIU”

规则三:
给定任何内部出现“III”的字符串,你可以用“U”替换“III”
例如:“MIIII”你可以转换成“MUI”(通过用U替换中间的III)。你也可以组成“MIU”(通过用“U”替换结尾的“III”)。

规则四:
给定任何内部出现"UU"的字符串,你可以删除“UU"
例子:对于"MUUI",可转换为"MI"

如果你能用推理规则从公理MI中产生一个字符串,我们就把它称为定理。
例如,我声称字符串“MUIIU”是一个定理;为了支持这一点,我提供了以下 "证明"。

  • (1) MI(公理)
  • (2) MII(使用规则II)
  • (3) MIIII(使用规则II)
  • (4) MIIIIU(使用规则I)
  • (5) MUIU(使用规则III)
  • (6) MUIUUIU (使用规则II)
  • (7) MUIIU (使用规则IV)

你确定了“MUIIU”是一个定理(正如沿途得到的所有字符串一样)。

等一下,公理?定理?看过一些数学逻辑的读者可能会明白这是在干什么。

选择这个术语是为了暗示以下情况。我们设,类似于经典逻辑中的规则,如 "给定'P'和'如果P则Q',你可以得出'Q'的结论。" 我们设想,我们系统的字符串是用某种形式语言写成的逻辑语句。而我们想象公理是一些我们假设为真的逻辑语句。
所以上面的 "证明 "类似于从一个已知的公理出发,用逻辑推理的规则来推导出一些想要的定理,有点像证明!。

形式化系统是一种机械地编码逻辑推理的方式;人们可以很容易地写一个程序,从公理开始,递归地应用推理规则,产生一个不断增长的定理列表。

进阶
在这个例子中,MIU-系统似乎并没有反映出我们所关心的任何东西的结构。相比之下,下一个例子和半个例子则反映了这一点:它们是为了模拟自然数的乘法。

tq系统:

1、允许的字符:
t,q,-

2、公理:
-t-q-

3、规则:

  • 规则一:给定一个字符串xtyqz,其中x,y,z是只由连字符组成的字符串,你可以组成x-tyqzy
  • 规则二:给定一个字符串xtyqz,其中x,y,z是只由连字符组成的字符串,你可以组成x-tyqzx

与MIU系统不同,tq系统带有一个解释,它将形式系统的字符串转换为某些语境中的有意义的语句。在本例中,背景是 "乘法",解释看起来像:

t ⇒ 乘以
q ⇒ 等于 
- ⇒一
--⇒二


以此类推。这种解释将tq系统的公理“-t-q-”变成了 "一乘以一等于一 "的乘法,将定理“-t--q------”(在下面证明)变成了 "二乘以三等于六 "的乘法。

证明:
  1. (1) -t-q- (公理)
  2. (2) --t-q--(规则I)
  3. (3) --t--q---- (规则二)
  4. (4) --t--q------ (规则二)


解释是赋予形式系统以意义:
在没有解释的情况下,-t--q------ 是一串无意义的字符,与MU系统的字符串相同。
但如果配备了上述解释,这个字符串就意味着乘法 "2乘3等于6"。
打个比方:对于一个对世界一无所知的孩子来说,地球仪只是一个旋转的玩具,上面覆盖着无意义的图片。但是一旦孩子知道地球仪上的图片(形式系统)代表(解释为)实际地球上的土地质量(背景),地球仪的各个方面就开始有了意义:
标有 "亚洲 "的绿色斑点比标有 "澳大利亚 "的斑点大,这就意味着亚洲大陆的土地质量比澳大利亚大陆的大。
(请注意,形式的“系统-解释-背景上下文”关系与“地图-领土”关系非常相似)。

在这一点上,有三点需要注意的。

首先,你不应该认为一个形式系统必然只有一种解释。例如,这里是tq系统的另一种解释,现在是在除法的背景下。

t⇒等于
q ⇒除以
- ⇒一
--⇒二


以此类推,因此,“-t--q------” 现在解释为 "二等于三除以六"。
在这种情况下,争论“-t---q------” 的 "真正含义 "是错误的;到底代表前面的乘法还是代表除法?
正确的看法是:两种含义同时被编码。它证明了乘法的结构与除法的结构是 "相同的"(借用数学中的一个词,Hofstadter会说乘法和除法是 "同构的")。

第二,并不是所有tq系统的字符串在解释下都是有意义的。tq系统也包含像ttq-t这样的字符串,它并不对应于任何乘法。如果一个字符串在我们选择的解释下确实带有意义,我们就称它为格式良好的字符串。这包括像-t-q--这样的字符串,它确实意味着什么(1乘以1等于2),尽管这个东西是假的。

第三,tq系统的所有定理不仅形式良好,而且还代表真正的乘法。例如,定理“-t-q-”和“-t--q------”,解释为真正的乘法 "一乘以一等于一 "和 "二乘以三等于六"。(格式良好的字符串-t-q--并不如此,但这也没关系,因为它不是一个定理)。这真的很重要,所以让我们把它作为一个要求:如果我把某个东西称为一个形式系统的 "解释",我将永远意味着这些定理是形式良好的,并且在这个解释下是真的。
举个反例,如果我们把'-'改成'二',那么我们就不再有一个解释了,因为定理”-t-q-“将代表 "二乘二等于二 "的乘法,而这并不是真的。

增强tq系统
作为形式化系统的最后半个例子,让我们增强tq系统,使其能够证明代表 "6是组合的 "这样的语句的定理。

tqCP-系统:
允许的字符:t,q,-,C,P
公理:与tq系统相同
规则:与tq系统相同,外加:
规则三:给定一个字符串xtyqz,其中x,y,z至少由两个连字符组成,你可以组成Cz

我打算将这个tqCP系统解释为 "算术语句 "的背景,看起来与tq系统相同,另外。

Cx ⇒ x 是组合的
Px ⇒ x不是组合的(或者等同于,x是素数)。

推理规则不允许P出现在定理中,那么有P是怎么回事?稍后再谈这个问题。

跳出形式系统
我在上面声称,对tq系统的给定解释是有效的,也就是说,它将系统的定理转化为真正的乘法。我怎么知道的呢?当然我举了两个例子,定理-t-q-和-t--q------,但我怎么能确定tq系统的每一个定理都能解释为真正的乘法呢?

我将这样论证。首先,公理”-t-q-“解释为真正的乘法(一乘一等于一)。其次,我们注意到,给定一个代表真乘法(x乘y等于z)的字符串xtyqz,规则I产生一个代表真乘法((x加1)乘y等于z加y)的字符串。规则二也是如此。由于我们的公理是真实的,而且我们的推理规则保持了真实性,所以我们所有的定理也必须是真实的!

上一段的推理是在哪里进行的?这当然不是 "tq系统内部 "的证明,因为那些证明看起来就像遵守推理规则的tq字符串的列表。
相反,这是一个 "跳出系统 "的例子:
我们用普通推理来推理tq系统,而不是用tq系统的内部形式逻辑
毕竟,系统并不 "知道 "我们给它的解释--也就是说,我们对解释的选择与tq系统的公理或推理规则没有关系,而这些规则是决定哪些字符串是定理的唯一因素。
所以我们不可能希望通过在tq-系统内工作来证明解释的有效性。我们必须走出去。

这里是另一个跳出系统的例子。我们刚刚看到,tq系统的每个定理都代表了一个真正的乘法。事实上,反过来也是如此,即每个真正的乘法都由tq系统的一个定理来代表!
如果你有兴趣,你可能希望证明这一点--这需要走出系统。
然后,利用这一观察,你可以 "从外面 "推导出tq系统的定理:例如,由于”---t--q---------“ 代表一个真正的乘法,我们知道它一定是一个tq定理。
同样,这不是形式意义上的 "证明",因为证明是通过应用规则产生的一串tq字符串。这是一个来自系统外的证明(在非形式意义上)。

读到这里也许你会暂停一下,看看自己是否口渴或需要上厕所。也许你现在正试图做一些我没有告诉你的事情,只是为了证明你真的可以跳出系统。

将此与图形计算器运行一个基本程序的行为进行对比,这个程序会打印出一个tq定理的列表。图形计算器永远不会停止执行它的代码,退后一步调查数据,注意到模式,并打印出 "你这个蠢货,这就是多重计算"。
当然,人最终是一些程序,尽管是一个非常复杂的程序,在一个极其强大的计算机上运行。

因此,有一些系统是我们无法跳出的,就像生物进化无法退后一步,看一看数据,然后对着虚空大喊:JUST KEEP MAKING MORE CRABS YOU DUMMY。
这里重点不是说人类的智慧在某种程度上是 "特殊 "的,而纯粹的机械推理是无法复制的。
关键点是更简单:智能系统似乎能够识别和运行子任务,以及从外部监测这些子任务并决定何时停止做这些任务。

真理与可证明性

"雪是白色的 "是真的,当且仅当雪是白色的。

- 阿尔弗雷德-塔斯基


在这一点上,你有可能把真理和可证明性这两个概念混为一谈。如果是这样,请不要感到难过:在整个逻辑学的历史上,直到1930年,几乎所有人都是这样做的。
那时,德国逻辑学家库尔特-哥德尔(Kurt Gödel)宣布了与他同名的不完备性定理,其结果是,真理和可证明性确实必须被视为独立的概念。
在本节中,我将解释真理和可证明性之间的区别,并陈述哥德尔定理。但首先,要讲一个关于哥德尔的故事。

1930年代末欧洲的生活对哥德尔并不友好。首先,他无法找到一个学术职位,因为他有太多的犹太朋友(作为一个数学家的常见副作用)。而更糟糕的是,他被征召到德国军队。因此,哥德尔做了一件合乎逻辑的事情:他逃到了美国,在普林斯顿得到了一个职位,并与他的好友爱因斯坦混在一起(爱因斯坦承认,他出现在工作场所的唯一原因是 "有特权与哥德尔一起走回家")。在为他的美国公民资格考试学习时,哥德尔声称他发现了一个奇怪的技巧,可以合法地将美国变成一个独裁国家(反法西斯分子恨他!)。尽管爱因斯坦警告说一定不要提这个问题,但哥德尔在入籍面试时完全提了出来。幸运的是,爱因斯坦在那里作为证人,也认识面试官,他设法使一切顺利进行。哥德尔成为了一名公民。我不知道有什么寓意,但希望这能让你领略到库尔特-哥德尔的思想。

思考真理/可证性区别的一个好方法是:可证性来自形式系统,真理来自解释+背景上下文。

可证明性比较简单,所以我们先来解决它。把形式系统中的一个字符串称为可证明性,只是把它称为一个定理的一种花哨的方式。也就是说,"可证明字符串 "和 "定理 "是同义词。
这应该是有意义的:记住,"定理 "只是指你可以用推理规则从公理中推导出来的东西,也就是说,你可以 "证明 "的东西。
例如,在上面的tqCP系统中,字符串"-t-q-"和"C------"是可以证明的,但"-t-q--"是不可以的。
在MIU系统中,MI和MUIIU是可以证明的,但是(破坏者!)MU不是。
请注意,可证明性是一个纯粹的形式概念,也就是说,它只取决于形式系统,而不取决于你对它的任何解释。

另一方面,真理则依赖于对解释的选择。给定一个带有解释的形式系统,如果该系统的一个字符串在给定的解释下显示为真,我们就说它是真。例如,"--t--q------" 是真的,因为2乘以3确实等于6,但"P----"是假的,因为4不是质数。我们不能说MIII或MMU是真的,因为我们心中并没有对MU系统的解释。

由于我们所有的解释都能将定理转化为真实的陈述。
我们知道:

在一个有解释的形式系统中,该系统的所有可证字符串也是真的。

或者更简洁的说:如果可以证明,那么就是真的。
这真的很重要:这就是为什么数学家和物理学家可以在纸上写一些有趣的符号,对它们进行逻辑运算,产生一些新的有趣的符号排列,并确信这些新的符号实际上告诉他们一些关于宇宙的真实情况。

你可能会被诱惑去相信相反的说法:形式系统中的每一个真实的陈述也是可以证明的。(至少,如果我没有一整节题为 "真理与可证明性 "的话,你可能会被诱惑这样想)。但是考虑一下tqCP系统的字符串P--,它被解释为 "二是素数"。这个字符串当然是真的,因为二是素数。但是它在tqCP系统中是不可证明的--事实上,该系统的所有规则都不允许你用P这个字符产生一个定理。

你可能在想,这表明tqCP系统在某些方面是糟糕的,或者至少是非常不完整的。
也许你很想在tqCP系统中增加一条新的规则:如果对于某个只由连字符组成的x,Cx不是一个定理,那么Px就是一个定理。
但这里有一个问题:应用这个规则需要列出tqCP系统的所有(无限多)定理,并检查Cx是否在其中。
但这并不是我们的形式系统所允许的那种简单的、机械的规则:你永远不可能写完所有的定理并检查”C--“不在其中。
你也许能够从系统外证明”C--“不是一个定理,但是这种 "系统外 "的推理对系统内的可证明性没有影响。

自我参照Self-reference和哥德尔定理 的证明
假设我走进你的房间并说:

我说的是谎言。

由于我是一个不被信任的陌生人,你可能会怀疑我在撒谎。但如果是这样的话,那么 "这句话是个谎言 "就是事实,所以我说的就是事实......这是一个矛盾!如果是这样的话,那么 "这句话是个谎言 "就是事实。
同样地,如果你认为我说的是实话,你会发现我在撒谎,这又是一个矛盾。

这就是所谓的说谎者悖论,也是哥德尔定理证明背后的基本思想。这个问题的核心是,我们有一个系统(英语)试图对自己进行建模,而我们已经展示了一个句子,其解释的意义正是参考了这个句子。这种 "蛇吞象 "的病理现象可以被安排来创造其他类似的悖论。

你可能认为我们可以用一个简单的规则来解决这样的事情,比如 "对一个形式系统的解释不能让上下文在那个相同的系统"。不幸的是,事情并不那么容易。考虑一下下面这个两步版的说谎者悖论。

下面的德语句子是假的。

Der obige englische Satz ist wahr. ("上面的英文句子是真的。")


在这里,"英语句子 "系统具有足够的解释力,英语句子能够对任意的德语句子提出主张。但是,关于 "德语中的句子 "系统有足够的表现力来对英语中的任意句子提出主张,这也是真实的。尽管每个句子本身是完全无害的,但整体是自相矛盾的

(请注意,"英语/德语句子 "并不是之前定义的真正意义上的形式系统,但它们在以下意义上是相似的,即它们是字符串的集合,可以被赋予解释,从而赋予字符串意义。因此,上述内容应该被看作是对下面要阐述的观点的一个纯粹的非正式的说明)。

问题的一部分是英语太丰富了。也就是说,它能够谈论像 "真理 "和 "虚假 "这样的概念,并支持自我参照。
它也足够丰富,可以对系统(如德语)进行建模,而这些系统本身也足够丰富,可以对英语进行建模,从而使两步式的说谎者悖论成为可能。
这些都不是容易修补的问题;目前还不清楚我们需要删除多少英语内容才能使其 "表达能力不强"。也许在这样做的时候,我们会破坏我们说任何有用的东西的能力。

英语太模糊了,所以哥德尔用数论的陈述来工作--比如 "二加二等于四 "和 "四是八的因子"。结果是,虽然数论的表达能力不足以谈论数论语句的真实性,但它的表达能力足以谈论数论语句的可证明性。

(我不会在这篇评论中进一步介绍,但数论之所以有足够的表现力来谈论可证明性,更深层的原因是它能够支持递归(关键事实是 "定理 "是由递归应用规则产生的字符串)。再深入一点,数论之所以能做递归,是因为它有一个归纳公理)

哥德尔证明的想法是将骗子悖论的 "可证明性版本 "编码到数论中。也就是说,给定一个足够丰富的形式系统来模拟数论,哥德尔想出了一个系统的字符串G,其在解释下的含义是:

G是不可证明的。

如果G是假的,那么G将是可证明的,因此是真的,这是一个矛盾。所以G一定是真的,使它成为一个不可证明的真理。由此可见,相关的形式系统是不完整的。

....感兴趣者点击标题见原文

人类意识与人工智能
霍夫斯塔德在第二部分的主要目标是关于智能和意识的东西;所有其他的主题都是切身的。我的总体感觉是,霍夫斯塔特在这里最有趣的观点自1979年GEB出版以来并没有过时。以下是他的主张的一个样本。

虽然他避免提出所谓的 "祖母神经元 "的存在,也就是说,一个神经元的唯一工作就是在你需要使用 "祖母 "这个概念时启动。
但霍夫斯塔特似乎认为类似的事情是真的:大脑中存在一个 "祖母模块"--也许是一个神经元集合--只要你想到祖母就会启动(而不会为其他事情启动)。
霍夫斯塔特似乎认为,我们思考问题的方式是让我们所有的不同模块一起启动,其方式大致与一连串的单词一起说出来形成一个句子一样。例如,"我的祖母很快乐 "的想法归结为你大脑中代表 "祖母 "和 "快乐 "的模块一起激活,再加上一些额外的信息来说明它是 "我的祖母",而不只是 "一个祖母 "之类的东西。

他的(人工)智能范式似乎涉及到智能系统构建形式化的系统,这些系统对它们要解决的问题进行建模,然后通过对形式化系统的符号化工作来解决这些问题。
更具体地说,他似乎设想智能系统:构建一个概念及其相互关系的网络(类似于WordNet对语言的作用),其中概念在内部由上述祖母模块等模块表示;然后将这些模块视为形式系统中的符号,根据某些规则操纵它们,从而修改它们之间的关系。

按照霍夫斯塔特的说法,意识产生于支持自我参照并能以某种方式自我修改的系统中。例如:能够编辑其源代码的计算机,当前权重决定如何修改权重的神经网络,以及人类的大脑,其中高层次的抽象会影响我们对低层次抽象的思考方式,反之亦然。霍夫斯塔特称这些自我参照系统为 "纠结的层次结构",而它们自我调节的方式为 "奇怪的循环"。

当涉及到视觉处理时,想法1似乎是正确的。在低层次上,我们已经确定了特定的神经元,它们以特定的方式一起发射,以编码关于线条方向的信息,这有点像低层次版本的祖母模块,用于垂直度或其他的概念(尽管显然预测性处理对具体代表什么信息有另一种看法)。
在中等水平上,当你看到人脸、动物或场景的图片时,会有神经元选择性地启动。在高层次上......这还不清楚。有些人将Quiroga等人的工作解释为证明了 "哈莉-贝瑞 "神经元的存在,但根据维基百科,Quiroga本人对这种解释提出异议。
但我们确实知道,在一些人工神经网络中存在这样的高级模块:OpenAI在他们的CLIP神经网络中发现了个别神经元,它们似乎与 "蜘蛛人"、"冬天 "或 "西非 "等概念相对应。
像这样的模块存在于视觉处理中也许并不令人惊讶--当你看一张模糊的图片时,你可以亲身体验到它们的激活,它突然变成了一张脸。

在视觉处理之外,事情并不那么清楚。当你看到一张脸时,你的 "脸部模块 "会被激活,但当你思考脸部的概念时,它是否会被激活?我个人持怀疑态度。
我们目前对GPT-3的理解是:我认为它是一个无法解释的权重丛林,其中没有一个概念被定位到网络的一个特定部分,这似乎是反对的证据。
但是,如果人工智能的可解释性有重大进展,比如你可以通过追踪特定神经元群的激活来确定GPT-3是否在思考一个祖母,那么这将是一个不同的故事。

目前,我初步得出结论,霍夫施塔特正在玩“哥德尔定理和意识都是神秘的,因此是等价的”游戏。







 

1