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ã 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.