lemma A4.8 Truth lemma

open in the book · appendices/04-completeness.tex:290 · p. 2898

Rests on

depends_on definition A4.6 The term structure ¶
- depends_on definition A4.2 Maximal consistent ¶
  - depends_on definition 7.82 Consistency, completeness, soundness ¶
    - depends_on definition 7.80 Formal system ¶
    - depends_on definition 7.7 Negation ¶
- depends_on equation A4.4 eq:app-comp-Tstar ¶
depends_on lemma A4.4 Behaviour of a maximal consistent set ¶
- depends_on definition A4.2 Maximal consistent ¶ ↺
- depends_on proposition 7.22 Algebra of propositions ¶
  - depends_on definition 7.17 Logical equivalence ¶
    - depends_on definition 7.12 Biconditional ¶
    - depends_on definition 7.14 Tautology ¶
  - depends_on definition 7.6 Truth table ¶
  - proves proof ch:01-logic-sets@proof-4 ¶
- proves proof app:completeness@proof-3 ¶
depends_on lemma A4.7 lem:app-comp-welldefined ¶
- depends_on definition A4.6 The term structure ¶ ↺
- depends_on definition 7.58 Equivalence relation ¶
- depends_on lemma A4.4 Behaviour of a maximal consistent set ¶ ↺
- depends_on theorem 7.60 Equivalence classes partition the set ¶
  - depends_on definition 7.59 Equivalence class ¶
    - depends_on definition 7.58 Equivalence relation ¶ ↺
  - depends_on definition 7.58 Equivalence relation ¶ ↺
  - depends_on definition 7.36 Disjoint sets ¶
  - depends_on equation 7.47 eq:set-double-inclusion ¶
  - proves proof ch:01-logic-sets@proof-11 ¶
- proves proof app:completeness@proof-5 ¶
depends_on lemma A4.5 Adding witnesses preserves consistency ¶
- depends_on definition 7.82 Consistency, completeness, soundness ¶ ↺
- proves proof app:completeness@proof-4 ¶
proves proof app:completeness@proof-6 ¶

Supports

depends_on theorem A4.9 Model existence ¶
- depends_on corollary A4.11 Compactness ¶
- depends_on theorem A4.10 Completeness ¶

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`	→	The term structure	declared	appendices/04-completeness.tex:295
`depends_on`	→	Behaviour of a maximal consistent set	declared	appendices/04-completeness.tex:295
`depends_on`	→	lem:app-comp-welldefined	declared	appendices/04-completeness.tex:295
`depends_on`	→	Adding witnesses preserves consistency	declared	appendices/04-completeness.tex:295
`depends_on`	←	Model existence	declared	appendices/04-completeness.tex:350
`proves`	←	app:completeness@proof-6	declared	appendices/04-completeness.tex:298