16
$\begingroup$

Is there a proof assistant for Peano Arithmetic (PA)?

Or, for some well known and better developed proof assistant is there a way to employ it to write down PA proofs ? Are there even tools to check whether the proof is within a fragment of PA?

If that is not the case for any proof assistant, why so?

(I am asking for first order PA, but the question could be formulated for second order PA, reverse math big fives, PRA, bounded arithmetic, and so on).

$\endgroup$
14
  • $\begingroup$ I think it is more concerned with FOL which is the infrastructure of PA. We have plenty of theories that has the strength of around PA (which can be measured by the ordinal $\epsilon_0$). So you should probably clarify whether you just want the strength of PA, or the whole FOL framework behind it. $\endgroup$
    – Trebor
    Feb 9, 2022 at 18:07
  • $\begingroup$ Peano level is Principia Mathematica so could/should be studied with Metamath-like systems. But you also can study this in MLTT. Actually there are a lot of systems able to handle PA. $\endgroup$ Feb 9, 2022 at 18:07
  • 2
    $\begingroup$ You could probably implement PA in Isabelle, which is a framework designed for different object-logics. $\endgroup$ Feb 9, 2022 at 19:11
  • $\begingroup$ Peano Arithmetic was originally second order, though first order PA and its fragments are the common usage today. For a the latter, FOL is all that is needed so Isabelle could do it just fine. PRA is more interesting since there are other possibilities for formalization. $\endgroup$ Feb 9, 2022 at 22:43
  • $\begingroup$ This is a very broad question. $\endgroup$ Feb 9, 2022 at 22:44

4 Answers 4

10
$\begingroup$

(I'm not a Metamath user, so I'll make this answer community wiki and others can improve it if needed.)

Metamath peano.mm

The Metamath theorem prover is (as the name suggests) a theorem prover for working with a number of different logics. While set theory is the most common, it also has some support for Peano arithmetic. The peano.mm file for Metamath was created by the late Bob Solovay in fact.

Number theory game for Metamath

The NTG is a number theory game for Metamath (similar in spirit to Lean's Natural Number Game) based on Solovay's peano.mm. While making the game, the creator discovered that there was a logical mistake in the axioms of peano.mm (because no one used it and the mistake is quite subtle). I think it is fixed now. There is more discussion on the Lean Zulip chat about this.

Metamath Zero

Metamath Zero is a research project by Mario Carneiro to write a minimal prover in both the style of Metamath and Lean which will formally verify its own correctness (in the sense that it will verify that its x86 byte code will behave as expected---that is it will check proofs according to the logic given to it). Since it is logic agnostic, it will be usable as an external checker for a number of theorem proving libraries (when compiled to term proofs or similar). It is also super fast.

If I'm not mistaken, Mario plans to do the verification in Peano Arithmetic. You can find his Peano files here. I believe that since he is embarking on a big formalization project in Peano Arithmetic, his treatment of PA is quite professional, including tactics and other tooling.

$\endgroup$
2
  • $\begingroup$ Thanks, I am looking at peano.mm, does it include any theorem, beside axioms? $\endgroup$
    – mario
    Feb 11, 2022 at 21:42
  • 1
    $\begingroup$ The NTG seems to have a larger peano.mm file with more stuff, but I honestly haven’t looked into this much. $\endgroup$
    – Jason Rute
    Feb 11, 2022 at 22:11
7
$\begingroup$

I am not aware of a proof assistant geared specifically for proving things in PA. But having worked with this myself I can confirm that there are indeed developments which formalize PA inside of proof assistants.

To do this, you need to define all of first-order logic inside of the proof assistant. This surmounts to defining terms and formulas over a signature, substitution, the deduction system and maybe some semantics depending on your goals. All of this has been done in some Coq formalizations and should therefore be possible in any proof assistant which is equally expressive (more examples: Lean, HOL). You can then define PA by choosing the right signature plus axioms, and build deductions i.e. proofs for PA inside or your proof assistant.

A drawback is that, from the onset, building deductions in this setup can become tedious quite fast. You will probably not prove something like the infinitude of primes without developing some dedicated tacticals (i.e. "poof assistant inside of a proof assistant") for the handling of deductive proofs.

The great thing about this setup is however that you can do meta-mathematics about PA or first-order logic in general. So you can talk about and show things like the completeness of the logic, the incompleteness theorems, Gentzen's consistency proof, undecidability, Tennenbaum's theorem etc.

$\endgroup$
3
  • $\begingroup$ "All of this is possible in e.g. Coq or Lean" - I imagine this is possible in one way or another in any proof assistant! It would be great if you could mention in which those things have been done. The last few links all seem to be about Coq. $\endgroup$
    – Wojowu
    Feb 11, 2022 at 10:44
  • 1
    $\begingroup$ @Wojowu I am mainly aware of the projects in Coq, but I added some more pointers based on a quick and rough search. You are interpreting the quoted sentence in just the right way; I wanted to express that based on the fact that it has been done at least in Coq, there should be no hurdle to do it in any other equally expressive proof assistant. $\endgroup$
    – Léreau
    Feb 11, 2022 at 12:27
  • $\begingroup$ "You will probably not prove something like the infinitude of primes without developing some dedicated tacticals (i.e. "poof assistant inside of a proof assistant")" − That is very sad; then it can't be used in the 'right' manner for pedagogy, since we want to prove statements rather than prove that they are provable. Anyway, do you know of a proof that there are infinitely many primes that does not involve finite sequences at all? (The usual one needs something like factorial.) $\endgroup$
    – user21820
    Mar 20, 2022 at 12:07
6
$\begingroup$

First-order Peano arithmetic is not finitely axiomatizable. This means that it is not sufficient to use (resolution-based) theorem provers, and so one must turn to systems that allow for greater expressiveness, particularly for mathematical induction (the only axiom scheme in Peano arithmetic). Usually proof assistants have a very powerful foundational system, so mathematical induction turns out to be almost a corollary within them. However, there is one system whose deductive framework is based on induction, which makes it not particularly powerful (in a foundational sense): ACL2 (and its predecessor Boyer-Moore theorem prover). Kaufmann and Moore write in A Precise Description of ACL2 logic:

The ACL2 logic is a first-order, essentially quantifier-free logic of total recursive functions providing mathematical induction and several extension principles, including symbol package definition and recursive function definition.

$\endgroup$
4
  • $\begingroup$ You give an argument for automated theorems provers ($\neq$ proof assistants) not supporting PA, but the question is about proof assistants. I think we'll need to sort out the terminology, as there have already been questions where people spoke of "theorem provers" but they really meant "proof assistants". $\endgroup$ Feb 11, 2022 at 13:55
  • $\begingroup$ @AndrejBauer One problem is that proof assistants are also called interactive theorem provers. :/ $\endgroup$
    – Jason Rute
    Feb 11, 2022 at 14:48
  • $\begingroup$ @JasonRute: Sure, but my point is that finite axiomatizabilty is not relevant as far as proof assistants are concerned. In fact, most have infinite axiomatizations (in the sense that there are infinitely many inference rules). $\endgroup$ Feb 11, 2022 at 16:32
  • $\begingroup$ Totally agree there. I’m just referring to your comment about terminology is all. Unfortunately “theorem prover” is a bit ambiguous because of the phrase “interactive theorem prover”. It might be hard to standardize terminology on this site which is what I thought you meant. $\endgroup$
    – Jason Rute
    Feb 11, 2022 at 17:07
2
$\begingroup$

In the source code for HOL Light (GitHub) is pa.ml with this comment.

(* ========================================================================= *)
(* Two interesting axiom systems: full Peano Arithmetic and Robinson's Q.    *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* We define PA as an "inductive" predicate because the pattern-matching     *)
(* is a bit nicer, but of course we could just define the term explicitly.   *)
(* In effect, the returned PA_CASES would be our explicit definition.        *)
(*                                                                           *)
(* The induction axiom is done a little strangely in order to avoid using    *)
(* substitution as a primitive concept.                                      *)
(* ------------------------------------------------------------------------- *)

In checking the HOL light tutorial (pdf) there is no direct examples of Peano arithmetic.

However pa.ml does have (link)

let PA_SOUND = prove
 (`!A p. (!a. a IN A ==> true a) /\ (PA UNION A) |-- p ==> true p`,
  REPEAT STRIP_TAC THEN MATCH_MP_TAC THEOREMS_TRUE THEN
  EXISTS_TAC `PA UNION A` THEN
  ASM_SIMP_TAC[IN_UNION; TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
  REWRITE_TAC[IN] THEN MATCH_MP_TAC PA_INDUCT THEN
  REWRITE_TAC[true_def; holds; termval] THEN
  REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
   [SIMP_TAC[ADD_CLAUSES; MULT_CLAUSES; EXP; SUC_INJ; NOT_SUC] THEN ARITH_TAC;
    ALL_TAC] THEN
  MAP_EVERY X_GEN_TAC [`q:form`; `i:num`; `j:num`] THEN
  ASM_CASES_TAC `j:num = i` THEN
  ASM_REWRITE_TAC[VALMOD; VALMOD_VALMOD_BASIC] THEN
  SIMP_TAC[HOLDS_VALMOD_OTHER] THENL [MESON_TAC[]; ALL_TAC] THEN
  REWRITE_TAC[UNWIND_THM2] THEN DISCH_TAC THEN
  SUBGOAL_THEN
   `!a b v. holds ((i |-> a) ((j |-> b) v)) q <=> holds ((i |-> a) v) q`
   (fun th -> REWRITE_TAC[th])
  THENL
   [REPEAT STRIP_TAC THEN MATCH_MP_TAC HOLDS_VALUATION THEN
    ASM_REWRITE_TAC[valmod] THEN ASM_MESON_TAC[];
    GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[]]);;

If you want to learn the internals of HOL Light see this other answer.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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