The Coq mailing list

[Dominik Kirst <dominik.kirst AT cs.uni-saarland.de>]

Hi everyone!

Incidentally, there are weak fragments of PA, such as Robinson's Q, which is finitely axiomatizable and yet allows suitable variants of Gödel's incompleteness theorems. I'm not up-to-date: did Robinson arithmetic appear in any relevant Coq formalization?

O’Connor’s Coq mechanisation of the incompleteness theorem (that has already been mentioned) works with a finite axiomatisation that is pretty close (but uncomparable) to Q. For an upcoming ITP paper, Marc Hermes and I mechanised the undecidability and incompleteness of an even weaker fragment than Q just containing the equations for addition and multiplication and showed that these results transport to all extensions still sound for the standard model [1].

Related to the initial question about non-standard numbers, Marc is currently working on a Coq mechanisation of Tennenbaum’s theorem in his ongoing master’s project [2]. Classically, this theorem states that there are no recursive non-standard models of PA [3] and interpreted in a constructive meta-theory, it even says that no non-standard models of HA exist at all [4]. So in Coq without additional assumptions, one cannot construct a model containing non-standard numbers for the natural definition of Tarski semantics (function symbol interpreted as functions). In fact, not even the standard model of PA can be shown to behave classically (i.e. to satisfy the first-order instances of LEM).

[1] https://www.ps.uni-saarland.de/extras/axiomatisations/

[2] https://www.ps.uni-saarland.de/~hermes/master.php

[3] https://www.logicmatters.net/resources/pdfs/TennenbaumTheorem.pdf

[4] https://www.jstor.org/stable/2274603?seq=1

Best wishes,

Dominik

-----------------------------------------

Programming Systems Lab
Saarland University
http://www.ps.uni-saarland.de/~kirst/