definition 3.14 Tautology
open in the book ·
parts/02-mathematical-methods/01-logic-sets.tex:402
· p. 21
- ground object -- no derivation owed
Rests on
No declared or derived dependency edges point away from this node yet.
Supports
-
depends_on
definition 3.17
Logical equivalence
¶
-
depends_on
proposition 3.19
Conditional as disjunction
¶
- depends_on proposition 3.21 Contraposition ¶
- depends_on proposition 3.20 De Morgan's laws ¶
-
depends_on
proposition 3.22
Algebra of propositions
¶
-
depends_on
lemma A.7
Behaviour of a maximal consistent set
¶
-
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
lemma A.11
Truth lemma
¶
-
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.17 Representability ¶ ↺
-
depends_on
theorem A.25
thm:app-inc-primrec
¶
-
depends_on
lemma A.7
Behaviour of a maximal consistent set
¶
-
depends_on
proposition 3.19
Conditional as disjunction
¶
-
depends_on
theorem A.4
Soundness
¶
- 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 |
← | Logical equivalence | declared | parts/02-mathematical-methods/01-logic-sets.tex:427 |
depends_on |
← | Soundness | declared | appendices/A-long-proofs.tex:1512 |