Following Dan Willard (from his paper "Self-Verifying Axiom Systems, the Incompleteness Theorem, and Related Reflection Systems", found on his [homepage](http://www.cs.albany.edu/FacultyStaff/profiles/willard.htm), pdf [here](http://www.cs.albany.edu/%7Edew/m/jsl1.pdf)):



> 
> "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?



A question regarding the consistency of Nelson's Predicative Arithmetic
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>


