What I did in my paper on Sergeyev’s Grossone 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 Internal Set Theory 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:
F. Montagna, G. Simi and A. Sorbi, Taking the Pirahã seriously, Communication in Nonlinear Science and Numerical Simulation, 21(1–3), April 2015, 52–69.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, Kaufmann 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 Sergeyev’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
