2
$\begingroup$

Following Dan Willard (from his paper "Self-Verifying Axiom Systems, the Incompleteness Theorem, and Related Reflection Systems", found on his homepage, pdf here):

"Define an axiom system $\alpha$ to be self-verifying iff

i) $\alpha$ can formally verify its own consistency (by some reasonable definition of self-consistency), and

ii) the axiom system $\alpha$ is in fact consistent."

Question: Is Nelson's system of Predicative Arithmetic self-verifying?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

No, Nelson's system extends Robinson arithmetic, so it's subject to Gödel's incompleteness theorems. Willard's systems can't prove the totality of addition or multiplication (see the wiki article) and that lets them avoid being able to carry out the diagonalization needed to create unprovable sentences.

https://en.wikipedia.org/wiki/Self-verifying_theories

Improve this answer
$\endgroup$
10
  • $\begingroup$ Can it be shown that Nelson's Predicative Arithmetic can prove the totality of addition and multiplication? Can it be shown that it can prove the totality of the successor operation? $\endgroup$
    – Thomas Benjamin
    Jan 7, 2016 at 9:53
  • $\begingroup$ (cont.) See Nelson's book Predicative Arithmetic, chapters 29-31. These chapters (possibly) suggest otherwise. Contrariwise, can anyone (now, themselves, or from the literature) derive the First and Second Incompleteness Theorems in Nelsons system? $\endgroup$
    – Thomas Benjamin
    Jan 7, 2016 at 10:14
  • $\begingroup$ Furthermore, let me quote from page 5 of "Self-Verifying Axiom Systems, the Incompleteness Theorem, and Related Reflection Principles" : "Nelson [in Predicative Arithmetic---my comment] proved that Robinson's System $\mathrm Q$ (with linear ordering) could prove a version of [$\forall$y {Tang(y) $\supset$ $\lnot$$Prf_{\alpha}$('0=1' ,y)}, where $Prf_{\alpha}$('0=1',y) denotes a formula indicating that y is a Goedel number of a proof from axiom system $\alpha$ ($\alpha$=$\mathrm Q$ in Nelson's case) of the sentence (0=1 in this case) with the Goedel number '0=1' --my comment] about $\endgroup$
    – Thomas Benjamin
    Jan 7, 2016 at 11:13
  • $\begingroup$ (cont.) itself when Tang(y) was taken to be a delicately specified "Definable Cut" of the Natural Numbers and "$Prf$" denoted Herbrand Deduction." The question is, is this sufficient to say that Predicative Arithmetic is self-justifying? $\endgroup$
    – Thomas Benjamin
    Jan 7, 2016 at 11:18
  • $\begingroup$ Whether Herbrand consistency on a definable cut is a reasonable notion of self-justification is totally a matter of opinion, however, note that under this definition, plenty of common theories are self-justifing: e.g., $I\Sigma_1$, $\mathrm{ACA}_0$, or $\mathrm{NBG}$; in fact, every consistent finitely axiomatizable sequential theory is. $\endgroup$
    – Emil Jeřábek
    Jan 7, 2016 at 16:10

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.