---
title: "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I"
authors:
  - "Kurt Gödel"
year: 1931
venue: "Monatshefte für Mathematik und Physik"
arxiv: null
doi: "10.1007/BF01700692"
source: "https://doi.org/10.1007/BF01700692"
topics:
  - incompleteness
  - godel
  - undecidability
  - arithmetization
seed_rank: 500
seed_batch: "foundations-greats-2026-08-13"
reviewed: "2026-08-13"
pool: "maths-foundations"
relevance_score: 10
lineage: foundations-of-computing
cites:
  - title: "Die Vollständigkeit der Axiome des logischen Funktionenkalküls"
    url: "https://doi.org/10.1007/BF01692469"
    year: 1930
    doi: "10.1007/BF01692469"
  - title: "Principia Mathematica, Volume I"
    url: "https://archive.org/details/cu31924001575244"
    year: 1910
see:
  - "499-die-vollstandigkeit-der-axiome-des-logischen-funktionenkalku"
  - "488-principia-mathematica-volume-i"
---

# Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I

## One-sentence takeaway

Any consistent formal system strong enough for arithmetic harbors a true but unprovable sentence, and (second theorem) cannot prove its own consistency.

## Why it matters here

The hard stop on Hilbert's program; every Anoptic discussion of total verification or self-certifying systems sits downstream of arithmetized syntax.

## Key ideas

- Gödel numbering: proofs, formulas, and substitution become primitive-recursive predicates on integers.
- First incompleteness: the sentence that says of itself "I am not provable" is true if the system is consistent, hence unprovable in it.
- Second incompleteness: a consistency statement \(\mathrm{Con}(T)\) is likewise unprovable in \(T\), so finitary self-consistency proofs of Principia-like systems fail.
- Explicitly targets *Principia Mathematica* and related systems; published *Monatshefte* 38:173–198, DOI 10.1007/BF01700692.

## Caveats

## Links

- DOI: [10.1007/BF01700692](https://doi.org/10.1007/BF01700692)