Here is an interesting example of how to encode first order logic. You see you encode all the connectives in a strict algebraic way over two sets, one for individuals and one for propositions, but the set of propositions has an inductive constructor, therefore all here takes a high order object as argument. There is only one truth…

---