+++
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`.