definition A5.2 Representability

open in the book · appendices/05-incompleteness.tex:88 · p. 2902

ground object -- no derivation owed

Rests on

depends_on definition 7.80 Formal system ¶

Supports

depends_on theorem A5.11 thm:app-inc-primrec ¶
- depends_on theorem A5.3 Representability ¶
  - depends_on proposition A5.14 prop:app-inc-derivability ¶
    - depends_on theorem A5.15 Second incompleteness theorem ¶
  - depends_on theorem A5.16 Church, Turing ¶
  - depends_on theorem A5.12 Diagonal lemma ¶
    - depends_on theorem A5.13 Rosser ¶
  - depends_on theorem A5.13 Rosser ¶ ↺
depends_on theorem A5.3 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`	→	Formal system	declared	appendices/05-incompleteness.tex:102
`depends_on`	←	thm:app-inc-primrec	declared	appendices/05-incompleteness.tex:328
`depends_on`	←	Representability	declared	appendices/05-incompleteness.tex:111