Artifact · open
Godel's first incompleteness theorem
This page records one proposition and the evidence attached to it. Text from the source ledger is shown as record data.
- Identifier
- F:godel-first-incompleteness
- Proof route
- Not assigned
- External status
- proved
- Axiom footprint
- Empty
Recorded description
Every consistent, effectively axiomatised formal system that interprets enough elementary arithmetic contains an arithmetical sentence that the system neither proves nor refutes.
; NOT EXPRESSIBLE. The proposition quantifies over formal systems and over derivations within them. Nothing in the axeyum term language denotes a formula, a proof, or a provability predicate, so there is no assertion whose negation being unsat would establish it. Recorded verbatim rather than approximated, because an approximation would be checkable and would not be this statement.Dependencies
The graph shows direct ledger edges. Follow a node to open its artifact page.
0 direct dependencies 0 direct dependents
Evidence
Provenance
{
"date": "2026-08-14",
"established_by": "not established in this ledger",
"source": "authored from the S:logic-and-proof strand of the math-education concept graph; statement written here, not copied",
"prior_art": [
{
"citation": "Godel 1931",
"establishes": "the theorem, long settled; also formalised and machine-checked in several proof assistants (Shankar in Nqthm 1986, Paulson in Isabelle/HOL 2014)"
}
]
}