lemma A.24 lem:app-inc-beta-delta0
open in the book ·
appendices/A-long-proofs.tex:2200
· p. 2801
Rests on
- depends_on definition A.22 Gödel's $\beta$ ¶
-
depends_on
definition A.18
$\Delta_{0}$ and $\Sigma_{1}$
¶
- depends_on equation A.119 eq:app-inc-order ¶
-
depends_on
lemma A.19
Numerals behave
¶
-
depends_on
definition 3.83
Peano arithmetic
¶
- depends_on axiom 3.33 Peano axioms ¶
- depends_on axiom 3.34 Principle of induction ¶
- depends_on definition 3.80 Formal system ¶
- depends_on equation A.118 eq:app-inc-Q-successor ¶
- depends_on equation A.119 eq:app-inc-order ¶ ↺
- proves proof app:A-long-proofs@proof-13 ¶
-
depends_on
definition 3.83
Peano arithmetic
¶
- proves proof app:A-long-proofs@proof-17 ¶
Supports
-
depends_on
theorem A.25
thm:app-inc-primrec
¶
-
depends_on
theorem A.17
Representability
¶
-
depends_on
proposition A.28
prop:app-inc-derivability
¶
- depends_on theorem A.29 Second incompleteness theorem ¶
- depends_on theorem A.30 Church, Turing ¶
- depends_on theorem A.26 Diagonal lemma ¶
- depends_on theorem A.27 Rosser ¶ ↺
-
depends_on
proposition A.28
prop:app-inc-derivability
¶
-
depends_on
theorem A.17
Representability
¶
Neighborhood
Every logical edge within two steps of this node.
- declared and complete
- partly declared
- a check failed
- not graded
- declared in the source
- inferred from structure
Edges
| type | direction | node | provenance | where |
|---|---|---|---|---|
depends_on |
→ | Gödel's $\beta$ | declared | appendices/A-long-proofs.tex:2210 |
depends_on |
→ | $\Delta_{0}$ and $\Sigma_{1}$ | declared | appendices/A-long-proofs.tex:2210 |
depends_on |
→ | Numerals behave | declared | appendices/A-long-proofs.tex:2210 |
depends_on |
← | thm:app-inc-primrec | declared | appendices/A-long-proofs.tex:2229 |
proves |
← | app:A-long-proofs@proof-17 | declared | appendices/A-long-proofs.tex:2213 |