Metamathematical investigations on the theory of Grossone

We propose an axiomatization of Sergeyev’s theory of Grossone, trying to comply with his methodological principles. We find that a simplified form of his Divisibility axiom is sufficient. We use for easier readability a second order language and a predicative second order logic. Our theory is not finitely axiomatizable and is a conservative extension of Peano’s arithmetic.