On Formally Undecidable Propositions of Principia Mathematica and Related Systems

Author: Kurt Gödel
Links: PDF (English translation)

Summary

Proves that any sufficiently powerful formal system contains true statements that cannot be proven within the system, and that no such system can prove its own consistency.

Relevance to Hyperon

Fundamental to understanding the limits of formal reasoning in AGI. Informs the design of PLN and MeTTa's type system, which must handle incompleteness gracefully rather than assuming decidability.