EAGER: An Investigation of the Partial Degrees in Which Logics Can Recognize Their Own Consistency and the Potentially Broad Inter-Disciplinary Implications of These Effects

哥德尔的不完全性定理本质上是一个两部分的结果，它的第二个方面确定了所有传统的公理系统都不能证明一个定理来证实它们自己的一致性。后一种效应被称为第二不完备性定理，它与直觉完全相反，因为人类似乎隐含地认为他们的思考过程是一致的(以便他们获得思考所需的动机能量)。然而，令人惊讶的是，第二不完备性定理证明了传统逻辑不能证实这样非常自然的一致性假设。威拉德的研究项目的主要目标将是探索逻辑形式主义在多大程度上可以绕过第二不完备性定理，并形式化一种至少部分本能信念的自身一致性。威拉德已经发表了几篇文章，探索第二不完备性定理的边界情况例外及其推广，从而为这一相当非正统的研究方法建立了基本概念。威拉德计划的调查将有一个跨学科的重点，与计算机科学、数学、认知和信息科学、哲学和语言学密切相关。它将表明，尽管自我证明的公理系统有一个非常非常规的外壳，但它们确实保留了模拟任何逻辑上有效的公理系统所需的数据的大部分实用的面向计算机的知识的能力。它还将展示计算机化的浮点实数算术如何表现出与整数算术非常不同的行为，以及自我证明形式主义如何通过从一个形式的自我证明公理系统跳到另一个系统来保持扩展其知识库的能力(通过使用思想变化理论和各种反复试验的方法)。第二个不完备性定理足够健壮，只有在有限的上下文中它的扩散才是可行的，其中指定逻辑以非平凡的方式具有非常规的组件。这种非传统逻辑之所以令人感兴趣，是因为人类显然对自身的自我一致性有着某种与生俱来的本能理解(至少在某种形式上的一致性定义下是如此)。因此，从符号逻辑中了解什么样的算法过程和基本规则可以模拟思维存在对自身一致性的概念(完全意义上或部分意义上)是可取的。本研究项目的目的将是调查那些对自身一致性具有某种明确定义的部分知识的逻辑的性质、潜在用途和含义。

Goedel's Incompleteness Theorem is essentially a 2-part result, whosesecond facet establishes that all conventional axiom systems are unable toprove a theorem corroborating their own consistency. This latter effect,called the Second Incompleteness Theorem, is quite counter-intuitivebecause human beings seem to implicitly believe that their cogitationprocesses are consistent (in order for them to gain the needed motivationalenergy for cogitation). Yet quite surprisingly, the Second IncompletenessTheorem has demonstrated that conventional logics cannot corroborate such aseemingly very natural consistency assumption.The main goal of Willard's research project will be to explore to whatextent a logic formalism can wiggle around the Second IncompletenessTheorem and formalize a type of at least partial instinctive faith inits own consistency. Willard has already published several articlesexploring boundary-case exceptions to the Second IncompletenessTheorem and generalizations of it, thus establishing the basicfoundational concepts for this quite unorthodox research approachWillard's planned investigation will have an inter-disciplinaryemphasis, being germane to computer science, mathematics, thecognitive and information sciences, philosophy and linguistics. Itwill show that while self-justifying axiom systems have a veryunconventional outer shell, they do retain an ability to simulate mostof the practical computer-oriented knowledge of the data needed by anyarbitrary logically valid axiom system. It will also show howcomputerized floating-point real number arithmetics behave verydifferently from integer arithmetics and how self-justifyingformalisms retain an ability to expand their knowledge base by hoppingand skipping form one formal self-justifying axiom system to another(via the use of Mind Change Theory and sundry trial-and-errorexperimental methodologies).The Second Incompleteness Theorem is sufficiently robust that itsevasion is feasible only in a limited context, where the specifiedlogic possesses a component that is unconventional in a nontrivialway. The reason that such unconventional logics are of interest isthat human beings evidently possess some type of innate instinctiveunderstanding of their own self-consistencies (at least under someformal definitions of consistency). It is therefore desirable tounderstand what type of algorithmic processes and foundationalprecepts from symbolic logic can simulate a Thinking Being'sconception of its own consistency (in either a full or partial sense).The goal of this research project will be to investigate the nature ofand the potential uses and implications of logics that possess sometype of well-defined partial knowledge of their own consistency.