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

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

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.