definition 3.80 Formal system

open in the book · parts/02-mathematical-methods/01-logic-sets.tex:2284 · p. 45

ground object -- no derivation owed

Rests on

No declared or derived dependency edges point away from this node yet.

Supports

depends_on definition A.16 Representability ¶
- 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 theorem A.27 Rosser ¶ ↺
- depends_on theorem A.17 Representability ¶ ↺
depends_on definition 3.82 Consistency, completeness, soundness ¶
- depends_on definition A.5 Maximal consistent ¶
  - depends_on definition A.9 The term structure ¶
    - depends_on lemma A.11 Truth lemma ¶
      - depends_on theorem A.12 Model existence ¶
    - depends_on lemma A.10 lem:app-comp-welldefined ¶
      - depends_on lemma A.11 Truth lemma ¶ ↺
    - depends_on theorem A.12 Model existence ¶ ↺
  - depends_on lemma A.6 Lindenbaum ¶
  - depends_on lemma A.7 Behaviour of a maximal consistent set ¶
    - depends_on lemma A.11 Truth lemma ¶ ↺
    - depends_on lemma A.10 lem:app-comp-welldefined ¶ ↺
- depends_on lemma A.8 Adding witnesses preserves consistency ¶
  - depends_on lemma A.11 Truth lemma ¶ ↺
- depends_on theorem 3.84 Gödel's completeness theorem, 1930 ¶
  - depends_on theorem A.30 Church, Turing ¶ ↺
- depends_on theorem 3.87 Gödel, 1931 ¶
  - depends_on theorem A.29 Second incompleteness theorem ¶ ↺
  - depends_on theorem 3.88 Gödel's second incompleteness theorem ¶
- depends_on theorem 3.91 Tarski's undefinability of truth ¶
depends_on definition 3.81 Effective axiomatization ¶
- depends_on proposition A.15 Syntax is computable ¶
  - depends_on theorem A.26 Diagonal lemma ¶ ↺
- depends_on theorem 3.87 Gödel, 1931 ¶ ↺
depends_on definition 3.83 Peano arithmetic ¶
- depends_on lemma A.19 Numerals behave ¶
  - depends_on lemma A.24 lem:app-inc-beta-delta0 ¶
    - depends_on theorem A.25 thm:app-inc-primrec ¶ ↺
  - depends_on lemma A.20 $\Sigma_{1}$-completeness ¶
    - depends_on theorem A.25 thm:app-inc-primrec ¶ ↺
    - depends_on theorem A.17 Representability ¶ ↺
  - depends_on theorem A.25 thm:app-inc-primrec ¶ ↺
  - depends_on theorem A.27 Rosser ¶ ↺
- depends_on lemma 3.86 Diagonal lemma ¶
  - depends_on theorem 3.87 Gödel, 1931 ¶ ↺
  - depends_on theorem 3.91 Tarski's undefinability of truth ¶ ↺
- depends_on theorem 3.88 Gödel's second incompleteness theorem ¶ ↺
depends_on lemma 3.86 Diagonal lemma ¶ ↺
depends_on theorem 3.98 Church–Turing ¶
depends_on theorem 3.84 Gödel's completeness theorem, 1930 ¶ ↺

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`	←	Representability	declared	appendices/A-long-proofs.tex:2003
`depends_on`	←	Consistency, completeness, soundness	declared	parts/02-mathematical-methods/01-logic-sets.tex:2334
`depends_on`	←	Effective axiomatization	declared	parts/02-mathematical-methods/01-logic-sets.tex:2311
`depends_on`	←	Peano arithmetic	declared	parts/02-mathematical-methods/01-logic-sets.tex:2361
`depends_on`	←	Diagonal lemma	declared	parts/02-mathematical-methods/01-logic-sets.tex:2444
`depends_on`	←	Church–Turing	declared	parts/02-mathematical-methods/01-logic-sets.tex:2863
`depends_on`	←	Gödel's completeness theorem, 1930	declared	parts/02-mathematical-methods/01-logic-sets.tex:2386