Nonstandard Natural Numbers via Internal Set Theory in Coq

Question

I'm trying to translate http://www.stat.umn.edu/geyer/nsa/o.pdf to Coq, but I'm stuck right at the start on the simple axioms for the predicate "standard" over natural numbers. The pdf linked here gives these as the first three axioms:

1. $0$ is standard
2. If $n \in \mathbb{N}$ is standard, then so is $n + 1$.
3. There exists an $n \in \mathbb{N}$ that is not standard.

For which I have two potential translations into Coq:

Axiom std : nat -> Prop.
Axiom std_0 : std 0.
Axiom std_Sn : forall n : nat, std n -> std (S n).
Axiom exists_non_std_n : exists n : nat, ~ std n.

or:

Inductive std : nat -> Prop :=
  | std_0 : std 0
  | std_Sn : forall n : nat, std n -> std (S n).

Axiom exists_non_std_n : exists n : nat, ~ std n.

Both have the same problem, which is that I can freely use internal induction with the property "standard" to prove that all natural numbers are standard (and so with the third axiom I've introduced a contradiction.) Of course the text specifically points out that internal induction can only be used with internal properties so as to avoid this problem.

So my question is, what can I do differently to avoid this problem. Do I need to specify whether predicates are internal or external? (and if so, how?) Or a more radical change, like not using the inbuilt definition of natural numbers?

And for bonus points, can anyone highlight the difference between the two definitions as I provided them? Is it just that I wouldn't be able to use the induction tactic on str as written the first way or are there other important differences?

Answer 1

Very intriguing idea. It seems to me that if you are going to implement Nelson's framework you are going to have to address the central feature of his framework that makes it different from traditional ZF frameworks. In traditional set theory, one is limited to a single relation, namely the binary relation "belonging to" $\in$. In Nelson's framework you have in addition a one-place predicate "standard". It is unfortunate that Nelson used the term "standard", by the way. It would have been preferable to use Leibnizian "assignable". At any rate it seems to me that the new predicate has to be incorporated into the system at a very low/basic level if one is to get anywhere with implementing Nelson.