The first order Peano axioms are not categorical but are recursively enumerable. The second order axioms are categorical but not recursively enumerable. Ther

The first order Peano axioms are not categorical but are recursively enumerable. The second order axioms are categorical but not recursively enumerable. There are statements that are true in Z but not true in a non-standard model of the first order axioms. Such a true statement is not something that can't be proven true. It just can't be proven true using the first order system.