Isn't the underlying question proved impossible by Godel's incompletness theorem?

No, Gödel's incompleteness theorem applies to theories that can interpret first-order arithmetic, which includes quantified statements like "for all x, there exists a prime p > x".

In this case, we have the much simpler equational theory of positive integers under addition, multiplication, and exponentiation, which does not include any quantifiers. In fact, Gurevič showed that this theory is decidable [0]. On the other hand, Gurevič later showed that this theory is not finitely axiomatizable [1], so an infinite (but still computable) set of axioms is needed to fully characterize the theory.

[0] R. Gurevič, Equational theory of positive numbers with exponentiation, 1985, https://doi.org/10.2307/2044966

[1] R. Gurevič, Equational theory of positive numbers with exponentiation is not finitely axiomatizable, 1990, https://doi.org/10.1016/0168-0072(90)90049-8

[deleted]
[deleted]