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.


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?


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.

  • $\begingroup$ Thank you for your response Mikhail. As far as I know Coq is based on a type theory called the Calculus of Constructions, rather than ZF set theory. I'm not sure what that means in terms of how 'low-level' the addition will have to be. Probably still very low-level. In CoC, Prop, the type of propositions, is totally fundamental so if I have to split this type into separate types for internal and external propositions it may require major changes to the entire theory. I think I'll just work through the text by pen and paper for now, and leave learning Coq for another project :) $\endgroup$ – Kit Joyce Sep 1 '16 at 6:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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