It’s just like the set of all arithmetical truths: you cannot axiomatize it, but it’s for sure not inconsistent.
Mega-nitpicks: 1) it is possible to axiomatize the set of all arithmetical truths by taking as your axioms the set of all arithmetical truths. The problem with this axiomatization is that you can’t tell what is and isn’t an axiom, which is why Gödel’s theorem is about recursively enumerable axiomatizations instead of arbitrary ones, and 2) it is very likely that Peano arithmetic is consistent, but this isn’t a proposition I would assign probability 1.
it is possible to axiomatize the set of all arithmetical truths by taking as your axioms the set of all arithmetical truths.
Yes, I’ve thought to add “recursively” to the original statement, but I felt that the word “axiomatize” in the OP carried the meaning of somehow reducing the number of statement, so I decided not to write it. But of course the trivial axiomatization is always possible, you’re totally correct.
it is very likely that Peano arithmetic is consistent, but this isn’t a proposition I would assign probability 1.
Heh, things get murky really quickly in this field. It’s true that you can prove arithmetic consistent inside a stronger model, and it’s true that there are non-standard submodel that think they are inconsistent while being consistent in the outer model. There are also models (paraconsistent in the meta-logic) that can prove their own consistency, avoiding Goedel theorem(s). This means that semantically, from a formal point of view, we cannot hope to really prove anything about some true consistency. I admittedly took a platonist view in my reply.
Mega-nitpicks: 1) it is possible to axiomatize the set of all arithmetical truths by taking as your axioms the set of all arithmetical truths. The problem with this axiomatization is that you can’t tell what is and isn’t an axiom, which is why Gödel’s theorem is about recursively enumerable axiomatizations instead of arbitrary ones, and 2) it is very likely that Peano arithmetic is consistent, but this isn’t a proposition I would assign probability 1.
Yes, I’ve thought to add “recursively” to the original statement, but I felt that the word “axiomatize” in the OP carried the meaning of somehow reducing the number of statement, so I decided not to write it. But of course the trivial axiomatization is always possible, you’re totally correct.
Heh, things get murky really quickly in this field. It’s true that you can prove arithmetic consistent inside a stronger model, and it’s true that there are non-standard submodel that think they are inconsistent while being consistent in the outer model. There are also models (paraconsistent in the meta-logic) that can prove their own consistency, avoiding Goedel theorem(s). This means that semantically, from a formal point of view, we cannot hope to really prove anything about some true consistency. I admittedly took a platonist view in my reply.
Sure we can. If we found a contradiction in Peano arithmetic, we’d prove that Peano arithmetic is inconsistent.