I am considering whether I should learn the ACL2 proof assistant. However, before diving into that, I wanted to know if there are significant limitations in terms of proving math. The first thing I noticed is that it is said to be first-order-logic (e.g. here).
I am not sure if being FOL is a significant limitation in terms of proving math. From my very limited understanding, a concrete example of using higher order logic is to assert in inductions that an arbitrary property $P$ holds for all values (e.g. the ability to quantify over properties or functions). But from initial reading, it seems that ACL2 can define various kinds of induction rules:
However, unlike Nqthm, ACL2 provides a means by which the user can elaborate the rules under which function applications suggest induction schemes. Such rules are called :induction rules. The definitional principle automatically creates an :induction rule, named (:induction fn), for each admitted recursive function, fn.
It is possible for the user to create additional :induction rules by using the :induction rule class in defthm.
My questions are:
Are there proofs using inductions that can be proved in HOL provers (such as Isabelle) but not in ACL2?
More generally, are there other types of mathematical proofs that can be done in HOL provers but not in ACL?