Book Review
                            Program = Proof: Part II

                                     LdBeth

               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.