6
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • $\begingroup$ Generally until you start getting into the limits of logical strength, like proving that ZFC is consistent, I don’t think the choice of logic matters for what you can prove. They can prove all the same basic theorems. The difference is in how easy they are to use. As for FOL vs HOL it depends on the additional axioms used in both systems. IIRC, FOL with the axioms of ZFC is stronger than HOL with the axioms used in HOL-light. (I don’t know exactly what axioms ACL2 or Isabelle use.) $\endgroup$
    – Jason Rute
    Commented Dec 1, 2022 at 16:38

1 Answer 1

Reset to default
10
$\begingroup$

ACL2 supports well-founded induction up to, but not including $\epsilon_0$. So you cannot prove consistency of (first order) arithmetic, whereas in higher order logic you can (type :doc ordinals in the REPL for documentation).

More practically, however, you cannot express infinite sets in ACL2. More precisely, you can define a predicate (ie. even x holds iff x is an even number) which holds on infinitely many objects, and think of this as an infinite set, however you cannot quantify over infinite sets. This restriction to quantification over finite sets is the real limitation here, more so than being a first-order logic (recall ZFC is a first order logic).

There are advantages to this approach, however, as ACL2 supports highly automated inductive proofs.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Is there a reference for the first sentence? Or perhaps there is a well-known interpretation of ACL2 in PA, for example? $\endgroup$
    – François G. Dorais
    Commented Dec 22, 2022 at 16:51
  • $\begingroup$ I'm puzzled about the second paragraph: if you could quantify over infinite sets then it wouldn't be first-order logic. Maybe you mean something else? $\endgroup$
    – François G. Dorais
    Commented Dec 22, 2022 at 16:53
  • $\begingroup$ @FrançoisG.Dorais You can input the command :doc ordinals in the REPL to get documentation on ordinals in ACL2. All ordinals up to epsilon-0 may be represented in this way, and it is assumed in termination checking that these ordinals are well-founded. Edited my answer, should make more sense. $\endgroup$
    – Couchy
    Commented Dec 22, 2022 at 19:39
  • $\begingroup$ @FrançoisG.Dorais See also Ordinal Arithmetic in ACL2 $\endgroup$
    – Couchy
    Commented Dec 22, 2022 at 19:43

Not the answer you're looking for? Browse other questions tagged or ask your own question.