逻辑是许多事情的基础。但逻辑本身的基础是什么？
在符号逻辑中，一个引入p和q这样的符号，以代表语句（或“命题”），如“这是一个有趣的文章”。然后，一个具有某些“逻辑规则”，类似于任何P和任何Q，而不是（P和Q）与（不是P）或（不是Q）相同。
但这些“逻辑规则”来自哪里？好吧，逻辑是一个正式的系统。而且，与Euclid的几何形状一样，它可以建立在公理上。但是是什么原理？我们可能会从像p和q = q和p这样的东西开始，或者不是p = p。但需要多少公理？他们有多简单？
很长一段时间是一个唠叨的问题。但是在2000年1月29日星期六下午8:31，在我的电脑屏幕上突然出现了一个公理。我已经展示了没有任何更简单的东西，但我很快就确定了这个小公理足以产生所有逻辑：
但是我怎么知道它是正确的？好吧，因为我有一台计算机证明它。这是证据，因为我以新的四种科学（它现在在Wolfram数据存储库中提供）：
使用最新版本的Wolfram语言，任何人现在都可以在一分钟内生成此证明。鉴于验证每个步骤，鉴于此证明。但为什么结果是真的？什么是解释？
这与越来越多地被问及各种计算系统的问题，以及机器学习和AI的各种应用。是的，我们可以看到会发生什么。但我们能理解吗？
我认为这最终是一个深刻的问题 - 这实际上对科学技术的未来至关重要，实际上是我们整个智力发展的未来。
但在我们谈论这个问题之前，让我们谈谈逻辑，以及我找到的公理。
逻辑作为正式纪律基本上起源于公元前4世纪的亚里士多德。作为他终身努力的一部分，目录的东西（动物，原因等），aristotle编目的有效形式的参数，并为它们创建了符号模板，基本上提供了两千年的逻辑的主要内容。
然而，到了1400年代，代数已经发明了，并且它来了解的符号表示。但直到1847年，George Boole最后用与代数相同的方式制定了逻辑，逻辑运营如和或被认为根据代数的规则。
在几年之内，人们明确地编写了逻辑的Axiom系统。典型的例子是：
但逻辑真的需要和还是不是？在20世纪的第一个十年之后，几个人发现，实际上我们现在呼叫NAND的单一操作足够了，例如计算为（P NAND P）NAND（Q NAND Q）。 （NAND的“功能完整性”可能是一个好奇心，但是对于半导体技术的发展 - 这在现代微处理器中实现了所有晶体管中的所有数十亿逻辑操作，这些晶体管的组合除了NAND或相关功能，也没有。 ）
但是，好的，所以逻辑的公理（或“布尔代数”）在NAND方面看起来像什么？这是他们的第一个已知版本，来自1913年的Henry Sheffer（这里是DOT·代表NAND）：
回到1910年的怀特麦满和拉塞尔的普林尼亚Mathematica已经推广了这一想法，也许所有数学都可以来自逻辑。特别是考虑到这一点，对看到逻辑的原理是多么简单的兴趣，有很大的兴趣。这是关于这一点的一些最着名的工作是在利沃夫和华沙（波兰两部），特别是由JanŁukasiewicz（作为他的工作的副作用，在1920年括号内发明了1920年括号ŁukAsiewicz或“波兰”符号） 。 1944年，在66岁时，Łukasiewz从接近的苏维埃逃离 - 1947年在爱尔兰最终。
同时，在温彻斯特和剑桥教育的爱尔兰人出生的梅雷迪思，并成为剑桥的数学教练，他的健康主义被迫于1939年回到爱尔兰。并于1947年，梅雷迪思讲课Łukasiewicz在都柏林，激励他开始寻找简单的公理，这将占据他余生的大部分时间。
经过近20年的工作，他在1967年取得了成功，简化了这一点：
但它可以变得更简单吗？梅雷迪斯多年来一直在挑选，试图看看NAND如何在这里或那里被删除。但在1967年之后，他显然没有进一步（他在1976年去世），但1969年他确实找到了三Axiom系统：
当我开始探索逻辑的Axiom系统时，我实际上并不了解Meredith的工作。我会成为试图了解简单规则可以产生的行为的一部分的一部分。回到20世纪80年代初，我会令人惊讶的发现，即使是蜂窝自动机甚至是一个最简单的可能的规则，就像我最喜欢的规则30一样 - 可能会产生大复杂性的行为。
并在20世纪90年代基本上试图弄清楚这一现象的概括，我最终想了解它如何适用于数学。它是一个直接观察，即在数学中，一个基本上从公理开始（例如算术，或几何形状或逻辑），然后试图从他们那里证明一系列复杂的定理。
但是，公理可以是多么简单？嗯，这就是我想在1999年发现的。作为我的第一个例子，我决定看看逻辑（或等价，布尔代数）。与我预期的预期相反，我对蜂窝自动机，图灵机和许多其他类型的系统的经验 - 包括甚至部分微分方程 - 是可以刚刚开始枚举最简单的情况，之后不太长会开始看到有趣的东西。
但可以这样一个“发现逻辑”？好吧，只有一种方法可以讲述。在1999年底，我设置了事情，开始探索所有可能的公理系统的空间 - 以最简单的方式开始。
在某种意义上，任何Axiom系统都提供了一组约束，例如P·Q.它没有说什么p·q“是”;它只是提供P·Q必须满足的属性（例如，它可以说P·Q = P·Q）。然后，问题是，来自这些属性是否可以从P Q Q为NAND [P，Q]：不再且不少。
有一种直接测试其中的一些方法。只要采取Axiom系统，如果P和Q可以是真或假的，请看看P Q Q·Q的显式形式满足公理。如果Axiom系统只是P·Q = Q·P，则是，P·Q可以是NAND [P，Q] - 但它不一定。它也可以是[p，q]或相等的[p，q] - 批量其他事情，这些内容不会满足与逻辑中的NAND函数相同的定理。但是，当一个到达公理系统{（（p·p）·q）·（q·p）= q}一个人到达nand [p，q]（以及基本上等同的或[p，q ]）是P·Q的唯一“模型”，其工作 - 至少假设P和Q只有两个可能的值。
那么这是逻辑的Axiom系统吗？好吧，没有。例如，它意味着，P Q Q有一个可能的形式，具有P和Q的3个值，而逻辑也没有这样的事情。但是，好的，这一事实是，这种公理系统只有一个公理甚至接近它表明它可能值得寻找再现逻辑的单一公理。这就是我2000年1月所做的（这几天都变得有点易于衡量，尤其非常感谢您的友好，相当新的Wolfram语言功能分组）。
很容易看出没有3个或更少的“NANDS”（或，真的，3或更少的“DOT运算符”）可以工作。在1月29日星期六凌晨5点（是的，我是一个夜猫子，我发现没有4个Nands可以工作。当我在凌晨6点后停止工作时，我会有14个可能的候选人5个。但是，当我在周六晚上再次开始工作并做更多的测试时，这些候选人中的每一个都失败了。
所以，毋庸置疑，下一步是尝试6个号码的情况。所有这些都有288,684人。但我的代码是高效的，并且在我的屏幕上出来之前没有长时间突出（是的，来自Mathematica版本4）：
起初我不知道我有什么。我所知道的只是这些是25个不平等的6- NAND公理，它比任何5名的任何一个都进一步得出。但是他们中的任何一个真的是逻辑的公理系统吗？我有一个（相当的计算密集型）的经验方法，可以统治公理。但是，肯定是任何公理实际正确的唯一方法是证明它可以成功繁殖，例如，逻辑的谢菲尔公理。
它采用了一点软件争吵，但在很多日子之前，我发现我发现的大部分时间都无法正常工作。到底，只有两个幸存下来：
并兴奋地兴奋地，我成功地拥有我的电脑证明两者都是逻辑的公理。我用的过程确保逻辑可能没有更简单的公理。所以我知道我会走到路的尽头：经过一个世纪（或甚至可能是几千年），我们最终可以说逻辑最简单的公理。
不久之后，我发现了两个2-Axiom系统，也有6个Nands总共，我证明可以重现逻辑：
如果选择采取换向P·Q = Q·P进行授予，那么这些就可以获得逻辑所需的只是一个微小的4- Nand Axiom。
好的，所以能够说一个人的“完成了亚里士多德开始了”（或者至少开始了）并找到了最简单的逻辑的公理系统。但它只是一个好奇心，还是对它有真正的意义？
在我以一种新的科学开发的整个框架之前，我认为人们会难以置信，以远远超过好奇心。但是现在人们可以看到它实际上与各种各样的创始问题相连，就像一个人是否应该考虑要发明或发现的数学。
数学作为人类实践它基于少数特定的公理系统 - 各自在定义某个数学领域（例如逻辑，或组理论或几何形状或设定理论）。但是在摘要中，在那里存在无限数量的可能的公理系统，每个系统都定义了原则上可以研究的数学领域，即使我们人类没有完成它。
在新的科学之前，我认为我隐含地认为，在计算宇宙中，几乎没有“在那里”，必须以某种方式“不太有趣”，而不是我们人类明确建立和研究的东西。但我对简单计划的发现使其清楚地说，在系统中的最小值通常是“在那里”的系统中，这比我们仔细选择的系统。
那么数学的Axiom Systems呢？好吧，比较与我们的人类研究的东西中的“出来”，我们必须知道我们已经研究过的数学领域的公理系统，我们已经学习了类似的逻辑 - 实际上是谎言。基于传统的人为构造的公理系统，我们得出结论，他们必须远远，如果一个人已经知道他们在哪里，那么就会有效。
但我的Axiom-System Discovery基本上回答了这个问题，“逻辑有多远？”对于像蜂窝自动机这样的东西，它特别容易分配一个数字（在20世纪80年代初）到每个可能的蜂窝自动机。用公理系统做到这一点稍微努力，但并不多。在一种方法中，我的公理可以标记为411; 3; 7;在Wolfram语言中构建为：
至少在可能的功能形式的空间（不计算可变标签），这是Axiom所在的视觉指示：
鉴于对我们人类学习的许多正规系统的基本逻辑是多么基本的逻辑，我们可能认为在任何合理的代表中，逻辑对应于最简单的可想象的公理系统之一。但至少我们使用的（NAND的）表示，这不是真的。仍然可以通过大多数衡量一个非常简单的Axiom系统，但如果刚刚开始枚举了从最简单的系统开始枚举Axiom系统，那么它可能会遇到千万可能的公理系统。
所以鉴于这一点，明显的下一个问题是，所有其他公理系统如何？那些故事是什么？嗯，这正是一种新的科学所在的调查。事实上，在书中，我认为我们在大自然中看到的系统等事情通常是最好的，我们可以通过枚举可能性来询问。
在AXIOM系统的情况下，我制作了一张图片，表示对应于不同可能的公理系统的“数学领域”中发生的事情。每行都显示了特定公理系统的后果，其中包含跨页面的框，指示在该公理系统中是否为真实定义。 （是的，在某些时候，Gödel的定理咬了一个，并且它变得不可挽回的是在给定的公理系统中证明或反驳给定定理;在实践中，通过我的方法发生在右边的右边，而不是图片显示......）
关于“人类调查”的数学领域有根本特别有些特殊？从这张照片，以及我研究过的其他事情，似乎没有任何明显的事情。我认为，唯一对这些数学领域来说真正特别的唯一特别是他们已经研究过的历史事实。 （一个人可能会使他们出现的索赔是因为他们“描述了真实世界”，或者因为他们是“与我们的大脑如何工作有关”，但结果是一种新的科学的结果反对这些。）
好吧，那么我的Axiom系统对于逻辑的重要性是什么？它的大小给出了逻辑的最终信息内容作为公理系统。它使它看起来像 - 至少现在 - 我们应该将逻辑视为“被发明为人类建设”的逻辑，而不是“被发现的”，因为它是以某种方式“自然暴露”。
如果历史有所不同，我们经常看出（以新的科学方式）在许多可能的简单公理系统中，我们将“发现”作为具有特定属性的逻辑的Axiom系统碰巧找到有趣。但是，我们探讨了这么少一些可能的简单公理系统，我认为我们只能合理地将逻辑视为“发明” - 由基本上是“自由裁量的”的方式构建。
从某种意义上说，这就是逻辑看，说，在中世纪 - 当可能的三段论（或有效的论点形式）被芭芭拉和圆圈等可能的助记符代表时要镜像这一点，找到我们现在所知的逻辑是逻辑的最简单的AxioM系统很有趣。
从（（P·Q）·R）开始）作为DPQ的HP计算器 - 所以可以写入整个公理= DDDPQRDPDPRPR。然后（正如Ed Pegg为我找到）那里有一个英文助记线：搞定队列，其中p，q，r是u，r，e。或者，看第一字母（使用运算符B和p，q，q，r为a，p，c）：“比特，一个程序计算了布尔代数的最佳二进制公理覆盖了所有情况”。
好的，那么人们如何证明我的Axiom系统是正确的？嗯，最直接的事情就是表明，从它可以推导出一个已知的Axiom系统，用于逻辑样谢菲尔的Axiom系统：
这里有三个公理，我们必须推导出他们每个人。好吧，通过最新版本的Wolfram语言，这是我们为派生的东西衍生，例如，第二个公理：
这是非常出色的，现在可以做到这一点。证明中使用了125个步骤的“证明对象”记录。从此证明对象来看，我们可以生成一个描述每个步骤的笔记本：
在概述中，恰及是一整个中间lemmas的序列，最终允许衍生的最终结果。在这种可视化显示的情况下，lemmas之间存在整个网络相互依存性：
以下是涉及在谢菲尔公理系统中导出所有三个公理的网络 - 最后一个涉及有些往往的504步骤：
而且，是的，很明显这些都很复杂。但在我们讨论复杂性意味着什么之前，让我们谈谈这些证明的各个步骤中实际进行的。
基本的想法很简单。让我们想象一下，我们的公理只是说P·Q = Q·p。 （在数学上，这对应于·换的陈述。）更准确地说，Axiom所说的是，对于任何表达式P和Q，P Q Q相当于Q·P.
好的，让我们说我们想要从这个公理得出（a·b）·（c·d）=（d·c）·（b·a）。我们可以通过使用公理将D·C转变为C·d，b·a至a·b，然后最后（C·d）·（a·b）至（a·b）·（c· d）。
FeedequicalProof实质上是相同的，尽管它选择以略微不同的顺序进行执行，并修改左侧以及右侧：
一旦一个人这样的证据，只需通过每个步骤才能贯彻即将贯彻，并检查他们产生的结果。但是如何找到证据？有许多不同的替换序列和可以做的转变。那么如何找到成功进入最终结果的序列？
有人可能会想：为什么不只是尝试所有可能的序列，如果有任何序列有效，那么人们最终会找到它？嗯，问题是，一个人快速最终得到了天文数的可能序列来检查。事实上，自动定理的主要艺术证明包括找到修剪序列数量的方法。
这很快得到了漂亮的技术，但如果一个人知道基本代数，最重要的想法很容易谈谈。假设您试图证明代数结果如：
✕（-1 + x ^ 2）（1 - x + x ^ 2）（1 + x + x ^ 2）==（-1 + x）（1 + x + x ^ 2）（1 + x ^ 3 ）
好吧，有一种保证的方法来实现这一点：只需应用代数的规则来扩展每个侧面 - 并且立即可以看到它们是相同的：
✕{展开[（ - 1 + x ^ 2）（1 - x + x ^ 2）（1 + x + x ^ 2）]， 展开[（ - 1 + x）（1 + x + x ^ 2）（1 + x ^ 3）]}
为什么这项工作？嗯，这是因为有一种方法是这样的代数表达式，并始终系统地减少它们，以便他们最终获得标准形式。好的，但是一个人可以对任意公理系统的证据做同样的事情吗？
答案是：没有立即。 它在代数中起作用，因为代数有一个特殊的财产，保证一个人总是可以在减少表达式中“取得进步”。 但是，在20世纪70年代，在20世纪70年代独立发现了什么（像Knuth-BENDIX和GRÖBNER基础算法等名称）是，即使AXIOM系统没有本质上有适当的财产，也可以潜在地找到它的“完成” 做。 这就是Findequical专业（基于Waldmeister的典型证据）正在发生的情况下发生了什么样的典型证据（“树木”）系统）。 有所谓的“关键双lemmas”，不直接“取得进步”自己，但是使它成为可能 ......