The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

Hi Emilio (and others),

On 3/6/21 8:18 PM, Emilio Jesús Gallego Arias wrote:
> Another way to look at it is that replacing the axiom scheme from PA by
> a single, second order induction principle usually rules out
> non-standard models.

that depends on one's stance on Henkin-style models.

Full second-order logic cannot be axiomatized. So even if one states the induction principle with second-order 
quantification, the kind of (non-standard, Henkin) models that one rules out depends on instantiation/substitution rules 
postulated for that second-order quantifiers. There is no end to it, as long as one insists that the set of rules/axioms 
remains decidable.

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?


Best,

t.