lemma A4.4 Behaviour of a maximal consistent set
open in the book ·
appendices/04-completeness.tex:116
· p. 2896
Rests on
-
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
definition 7.82
Consistency, completeness, soundness
¶
-
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 ¶
-
depends_on
definition 7.17
Logical equivalence
¶
- proves proof app:completeness@proof-3 ¶
Supports
-
depends_on
lemma A4.8
Truth lemma
¶
-
depends_on
theorem A4.9
Model existence
¶
- depends_on corollary A4.11 Compactness ¶
- depends_on theorem A4.10 Completeness ¶
-
depends_on
theorem A4.9
Model existence
¶
-
depends_on
lemma A4.7
lem:app-comp-welldefined
¶
- depends_on lemma A4.8 Truth lemma ¶ ↺
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 |
→ | Maximal consistent | declared | appendices/04-completeness.tex:131 |
depends_on |
→ | Algebra of propositions | declared | appendices/04-completeness.tex:131 |
depends_on |
← | Truth lemma | declared | appendices/04-completeness.tex:295 |
depends_on |
← | lem:app-comp-welldefined | declared | appendices/04-completeness.tex:258 |
proves |
← | app:completeness@proof-3 | declared | appendices/04-completeness.tex:134 |