Let's resume from about finite types we can do
first-order logic. This book enumeration, but for any‐
has a very good presentation thing that we can merely
of set theory for people prove that it exists this
with absolute no background seems impossible in the
in logic and set theory. intuitionistic setting.
Most other writers just
assumes the reader is a
mathematician that already The rest of the chapter
received the training at is about unification which
school, which is a very bad is the implementation detail
assumption. of a prover. We will skip
the tutorial on Agda and
1. INT set theory Emacs since one can always
reference their respective
Maybe I have mentioned documentation.
or maybe not, Intuitionism
is about having a witness of 3. Programming
corresponding proof terms.
While a general decider for Now we have a prover in
every proposition doesn't hand. Section 7.1 briefly
exist in intuitionistic gives an example of program
logic, for any finite types semantic, which I would say
we can easily construct some it might be much easier to
deciders by straightforward do it in Isabelle/HOL since
enumeration. Actually, Lemma Agda lacks automation. Actu‐
5.3.3.3 pointed out for ally, most of the examples
every subset of finite set here can also be done in
is finite IFF excluded mid‐ HOL.
dle is satisfied.
2. How do I make choice While I didn't expect
the review on FOL would be
While it seems confus‐ this long, that means we
ing on what the heck the will have a Part III for
axiom of choice is, it is this book review.
simply admitting that as
long as we know the type is So far we haven't
not empty we can always get touched anything specific to
a function that picks up an dependent type theory, thus
element of the type. Again what we learned also applies
for any combination of to HOL.
