theorem A.12 Model existence

open in the book · appendices/A-long-proofs.tex:1829 · p. 2797

Rests on

depends_on definition A.9 The term structure ¶
- depends_on definition A.5 Maximal consistent ¶
  - depends_on definition 3.82 Consistency, completeness, soundness ¶
    - depends_on definition 3.80 Formal system ¶
    - depends_on definition 3.7 Negation ¶
- depends_on equation A.112 eq:app-comp-Tstar ¶
depends_on equation A.112 eq:app-comp-Tstar ¶ ↺
depends_on lemma A.11 Truth lemma ¶
- depends_on definition A.9 The term structure ¶ ↺
- depends_on lemma A.7 Behaviour of a maximal consistent set ¶
  - depends_on definition A.5 Maximal consistent ¶ ↺
  - depends_on proposition 3.22 Algebra of propositions ¶
    - depends_on definition 3.17 Logical equivalence ¶
      - depends_on definition 3.12 Biconditional ¶
      - depends_on definition 3.14 Tautology ¶
    - depends_on definition 3.6 Truth table ¶
    - proves proof ch:01-logic-sets@proof-4 ¶
  - proves proof app:A-long-proofs@proof-5 ¶
- depends_on lemma A.10 lem:app-comp-welldefined ¶
  - depends_on definition A.9 The term structure ¶ ↺
  - depends_on definition 3.58 Equivalence relation ¶
  - depends_on lemma A.7 Behaviour of a maximal consistent set ¶ ↺
  - depends_on theorem 3.60 Equivalence classes partition the set ¶
    - depends_on definition 3.59 Equivalence class ¶
      - depends_on definition 3.58 Equivalence relation ¶ ↺
    - depends_on definition 3.58 Equivalence relation ¶ ↺
    - depends_on definition 3.36 Disjoint sets ¶
    - depends_on equation 3.47 eq:set-double-inclusion ¶
    - proves proof ch:01-logic-sets@proof-11 ¶
  - proves proof app:A-long-proofs@proof-7 ¶
- depends_on lemma A.8 Adding witnesses preserves consistency ¶
  - depends_on definition 3.82 Consistency, completeness, soundness ¶ ↺
  - proves proof app:A-long-proofs@proof-6 ¶
- proves proof app:A-long-proofs@proof-8 ¶
proves proof app:A-long-proofs@proof-9 ¶

Supports

depends_on corollary A.14 Compactness ¶
depends_on theorem A.13 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/A-long-proofs.tex:1831
`depends_on`	→	eq:app-comp-Tstar	declared	appendices/A-long-proofs.tex:1831
`depends_on`	→	Truth lemma	declared	appendices/A-long-proofs.tex:1831
`depends_on`	←	Compactness	declared	appendices/A-long-proofs.tex:1862
`depends_on`	←	Completeness	declared	appendices/A-long-proofs.tex:1848
`proves`	←	app:A-long-proofs@proof-9	declared	appendices/A-long-proofs.tex:1834