1 files changed, 26 insertions, 0 deletions
diff --git a/content/zettel/3b3c.md b/content/zettel/3b3c.md
new file mode 100644
index 0000000..159fbad
--- /dev/null
+++ b/content/zettel/3b3c.md
@@ -0,0 +1,26 @@
++++
+title = "Inductive Predicates"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3b3b"]
+forwardlinks = ["3b3d"]
+zettelid = "3b3c"
++++
+
+`tauto` is a complete decision procedure to solve propositional proofs,
+however, if other theorems are needed, then intuition can be used to
+prove more about those theorems.
+
+Coq implements *constructive*, or *intuitionistic* logic. Therefore,
+simple theorems like $\neg \neg P \rightarrow P$ do not always hold, and
+can only be proven if *P* is decidable.
+
+Therefore, the difference between `Prop` and `bool` is that `Prop` is
+often not decidable and cannot be constructed, whereas `bool` terms can
+be constructed by default.
+
+We can also think of `forall` as the type constructor for dependent
+function type constructor. This is because implication and `forall` are
+actually the same, for example we can define `forall x : P, Q`, where x
+does not appear in `Q`, which is equivalent to `P -> Q`.