There is a lot of weirdness here, once you try to reduce the question.
Imagine an AI programmed to believe in the axioms of PA and nothing else. What credence should it assign to the arithmetical statement Con(PA)? The answer is that there’s no answer. Assuming PA is “in fact” consistent, Con(PA) is formally independent from PA—which means I may add the negation of Con(PA) to PA as an extra axiom and get a consistent system. (Equivalently, that “self-hating” system has a model in ordinary set theory. Building it is a neat little exercise.) So believing or disbelieving in the “actual” consistency of PA, as we humans can, requires some notion of Platonism or semantics that we cannot yet teach to a computer.
And the question why you instinctively believe Gentzen’s proof, which uses transfinite induction up to epsilon zero, is even more mysterious. You’re comfortable relying on the consistency of a stronger system than PA because it sounds intuitive to you, right? Where do those intuitions come from? The very same place where naive set theory came from, I think.
There is a lot of weirdness here, once you try to reduce the question.
Imagine an AI programmed to believe in the axioms of PA and nothing else. What credence should it assign to the arithmetical statement Con(PA)? The answer is that there’s no answer. Assuming PA is “in fact” consistent, Con(PA) is formally independent from PA—which means I may add the negation of Con(PA) to PA as an extra axiom and get a consistent system. (Equivalently, that “self-hating” system has a model in ordinary set theory. Building it is a neat little exercise.) So believing or disbelieving in the “actual” consistency of PA, as we humans can, requires some notion of Platonism or semantics that we cannot yet teach to a computer.
And the question why you instinctively believe Gentzen’s proof, which uses transfinite induction up to epsilon zero, is even more mysterious. You’re comfortable relying on the consistency of a stronger system than PA because it sounds intuitive to you, right? Where do those intuitions come from? The very same place where naive set theory came from, I think.