Die Widerspruchsfreiheit der reinen Zahlentheorie.¶
Gentzen, G. (1936). Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112(1), 493-565.
Cited by¶
2 citations across 2 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Mathematical Induction
- preservation-and-progress proof of type soundness for ML-like languages, and is the workhorse of programming-language metatheory. Well-founded induction on program executions proves termination — pick a well-founded measure (a function from program states to a well-founded set), show every execution step strictly decreases the measure, and conclude that no infinite execution is possible. Transfinite induction in set theory extends induction beyond \(\omega\) into the ordinals; Gentzen 1936
This sourceConsistency proof of Peano Arithmetic via transfinite induction up to ε₀.
Supported in partVerified against the publisher's abstract
The title and the fetched abstract confirm a consistency proof of number theory, but nothing states transfinite induction or ε₀.
“Auch der «Kalkül LK » eignet sich für den Widerspruchsfreiheitsbeweis.”
- preservation-and-progress proof of type soundness for ML-like languages, and is the workhorse of programming-language metatheory. Well-founded induction on program executions proves termination — pick a well-founded measure (a function from program states to a well-founded set), show every execution step strictly decreases the measure, and conclude that no infinite execution is possible. Transfinite induction in set theory extends induction beyond \(\omega\) into the ordinals; Gentzen 1936
- Well-Foundedness (Well-Ordering)
- Descending-chain-free semantics in domain theory (Scott's pointed CPOs and Plotkin's powerdomains) provide fixed-point theorems for denotational semantics — the recursive equation f(x) = g(f, x) has a unique least fixed point in a CPO, and the construction iterates from ⊥ up the well-founded approximation order.
This sourceConsistency proof of Peano Arithmetic via transfinite induction up to ε₀.
- Descending-chain-free semantics in domain theory (Scott's pointed CPOs and Plotkin's powerdomains) provide fixed-point theorems for denotational semantics — the recursive equation f(x) = g(f, x) has a unique least fixed point in a CPO, and the construction iterates from ⊥ up the well-founded approximation order.
Verification¶
Does it exist? Not checked yet. This entry carries no identifier to resolve. It was extracted from the citation as written in the article, normalized, and deduplicated against the rest of the registry.
Does it back the claim? Read against the text for 1 of 2 citations: 1 supported in part. Each verdict is shown under its citation below, with what in the work backs the sentence.
Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.
See how references were verified.
Registry ID ref:7cdfbc6e0c79 · see in the full table