Incompleteness for stably consistent formal systems
We first partly develop a mathematical notion of stable consistency intended to reflect the actual consistency property of human beings. Then we give a generalization of the first and second G\"odel incompleteness theorem to stably $1,2$-consistent formal systems. Our argument in particular re-proves the original incompleteness theorems from first principles, using Turing machine language to (computably) construct our "G\"odel sentence" directly, in particular we do not use the diagonal lemma, nor any meta-logic, with the proof naturally formalizable in set theory. In practice such a stably consistent formal system could be meant to represent the mathematical output of humanity evolving in time, so that the above gives a formalization of a famous disjunction of G\"odel, obstructing computability of intelligence.
Code (0)
등록된 구현이 없습니다.
Tasks
LEMMASentenceSimilar Papers 제목 키워드 기반
Dual Computational Horizons: Incompleteness and Unpredictability in Intelligent Systems
We formalize two independent computational limitations that constrain algorithmic intelligence: formal incompleteness and dynamical unpredictability. The former limits the deductive power of consistent reasoning systems …
Incompleteness of AI Safety Verification via Kolmogorov Complexity
Ensuring that artificial intelligence (AI) systems satisfy formal safety and policy constraints is a central challenge in safety-critical domains. While limitations of verification are often attributed to combinatorial c…
Towards Concise, Machine-discovered Proofs of Gödel's Two Incompleteness Theorems
There is an increasing interest in applying recent advances in AI to automated reasoning, as it may provide useful heuristics in reasoning over formalisms in first-order, second-order, or even meta-logics. To facilitate …
Automated Theorem ProvingVocal Bursts Valence PredictionSynthesizing Robust Plans under Incomplete Domain Models
Most current planners assume complete domain models and focus on generating correct plans. Unfortunately, domain modeling is a laborious and error-prone task, thus real world agents have to plan with incomplete domain mo…
The Alignment Problem in Constrained Code Generation
Large Language Models (LLMs) have demonstrated strong capabilities in code generation, but their outputs frequently contain syntax or type errors that result in compilation failures. Constrained decoding has been propose…
Code Generation