cousin_it:
For example, we can add to PA some axiom that rules out its standard model, but leaves many nonstandard ones. The simplest example would be to add the inconsistency of PA - the resulting theory will (counterintuitively) be just as consistent as PA, but quite weird. [...] Can the AI recognize such situations and say "no way, this formal system doesn't seem to describe my regular integers"?
This seems to be a matter of some relatively straightforward human heuristics. A theory that is somehow directly "talking about itself" via its axioms looks weird and suspicious. And not to mention what this axiom would look like if you actually wrote it down alongside the standard PA axioms in the same format!
Note that when these heuristics don't apply, humans end up confused and in disagreement about what should be considered as "our regular" stuff when faced with various independent statements that look like potential axioms. (As with Euclid's fifth postulate, the continuum hypothesis, the axiom of choice, etc.)
It will have many interesting provable theorems that are nevertheless common-sensically "false", e.g. "PA proves 1+1=3".
More specifically, it will prove: "There exists a natural number that, when decoded according to your Goedelization scheme, yields a proof in PA that 1+1=3." However, it won't prove anything about that number that would actually allow you to write it down and see what that proof is. ("Writing down" a natural number essentially means expressing a theorem about a specific relation it has with another number that you use as the number system base.) This suggests another straightforward heuristic: if the theory asserts the existence of objects with interesting properties about which it refuses to say anything more that would enable us to study them, it's not "our regular" kind of thing.
If the theory asserts the existence of objects with interesting properties about which it refuses to say anything more that would enable us to study them, it's not "our regular" kind of thing.
Does this heuristic say that Chaitin's constant isn't a regular real number?
A big problem with natural numbers is that the axiomatic method breaks on them.
Mystery #1: if we're allowed to talk about sets of natural numbers, sets of these sets, etc., then some natural-sounding statements are neither provable nor disprovable ("independent") from all the "natural" axiomatic systems we've invented yet. For example, the continuum hypothesis can be reformulated as a statement about sets of sets of natural numbers. The root cause is that we can't completely axiomatize which sets of natural numbers exist, because there's too many of them. That's the substantial difference between second-order logic and first-order logic; logicians say that second-order logic is "defined semantically", not by any syntactic procedure of inference.
Mystery #2: if we're allowed to talk about arithmetic and use quantifiers (exists and forall) over numbers, but not over sets of them - in other words, use first-order logic only - then some natural-sounding statements appear to be true, but to prove them, we need to accept as axioms a lot of intuition about concepts other than natural numbers. For example, Goodstein's theorem is a simple arithmetical statement that cannot be proved in Peano arithmetic, but can be proved in "stronger theories". This means the theorem is a consequence of our intuition that some "stronger theory", e.g. ZFC, is consistent - but where did that intuition come from? It doesn't seem to be talking about natural numbers anymore.
Can we teach a computer to think about natural numbers the same way we do, that is, somehow non-axiomatically? Not just treat numbers as opaque "things" that obey the axioms of PA - that would make a lot of true theorems unreachable! This seems to be the simplest AI-hard problem that I've ever seen.