There is just one model of Dedekind's axioms up to a unique isomorphism, which is indeed the standard model. However, Gödel's incompleteness proofs do not wor

There is just one model of Dedekind's axioms up to a unique isomorphism, which is indeed the standard model. However, Gödel's incompleteness proofs do not work for Dedekind's theory because there are uncountable axiom instances. (Dedekind's theory is nevertheless effective because proof checking is algorithmically decidable.) Consequently, the first incompleteness result (inferentially undecidable) has been proved by other means. See the following for a proof: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 The above article explains that Gödel's second incompleteness result is false because the theory can prove its own consistency.