What I did in <a href="http://www.sciencedirect.com/science/article/pii/S0096300314005116">my paper on Sergeyev’s Grossone</a> that has been mentioned in your discussion  was to present an axiomatised theory of arithmetic in the  language of Peano arithmetic augmented with a new constant for Grossone. I did it  because many colleagues seemed  to  think that  Sergeyev’s approach didn’t respect the standards of acceptable mathematical exposition.  In my theory I showed that  Sergeyev’s axioms are provable while I argued that  it  respected Sergeyev’s outlook expressed in his so called (by him) postulates. The main result is that the theory  is a conservative extension of Peano arithmetic, that is  that it proves the same  sentences in  the language without Grossone; hence Sergeyev theory, if my theory is faithful to his spirit, in consistent if Peano’s arithmetic is consistent.

Moreover this should show that Sergeyev’s methods, at least as to their arithmetical part,  are something different form non standard analysis.  To discuss non standard analysis is not easy, since one should be precise on what one means;  there are various approaches, among  whom Nelson’s <a href="https://en.wikipedia.org/wiki/Internal_set_theory">Internal Set Theory</a> IST is probably the smoothest.  But any theory for non standard methods should be stronger  than Sergeyev’s, since these methods do not  seem to be a conservative extension of the classical  ones;  one needs either third order logic or strong assumptions on the existence of  special ultrafilters. In Sergeyev’s theory there is no transfer principle, and so on.
	
There is another paper  you might be interested in:
<blockquote> 
F. Montagna, G. Simi and A. Sorbi, <a href="http://www.theinfinitycomputer.com/Sorbi_web.pdf">Taking the Pirah&atilde; seriously</a>, Communication in Nonlinear Science and Numerical Simulation, <b>21</b>(1–3), April 2015, 52–69.
</blockquote> 
Here, the authors  go deeper into the logical use of Grossone in relation to predicative arithmetic.

Andrej Bauer asked in the comments:

"Could you comment on how your result is related to results by Kreisel
on non-standard arithmetic being conservative over PA? See for example
Proposition 2.3 in jstor.org/stable/2274260 and the reference to
Kreisel therein? (I cannot find a direct link to Kreisel, sorry.)"


Our results are rather similar, also in the proof, by compactness and adjustment of models. But while I think that my theory can be considered a fair rendition of Sergeyev’s  outlook, it is  doubtful that Kreisel’s *PA can be considered a faithful framework for non standard arithmetic. The authors  of the paper  mentioned in the comment, Henson, Stockman and Keisler  after  briefly recalling Kreisel’s result (indeed the first in this line)  go on saying that most of non standard  arithmetical  results depend on the use of omega1-saturated models, and discuss possible strengthening  of the theory to approximate the properties of such models. Non standard mathematics is more ambitious than Sergeyv’s computational interest, and requires in consequence stronger logical principles. It seems to me that at present there is no consensus on a formalisztion of these principles, but perhaps for Nelson’s set theory. 

Gabriele Lolli