Peano arithmetic has also been proved consistent (by Gödel himself, Gentzen, and others) but all of the proofs necessarily use methods slightly beyond Peano ari

Peano arithmetic has also been proved consistent (by Gödel himself, Gentzen, and others) but all of the proofs necessarily use methods slightly beyond Peano arithmetic. Gentzen proved the consistency of PA from primitive recursive arithmetic (a much weaker theory than PA, lacking quantifiers) combined with transfinite induction up to a particular ordinal. Gentzen also proved that this is more-or-less the best possible. Similarly, since Presburger arithmetic can't even express its own consistency, never mind attempt to prove it, any proof of the consistency of Presburger arithmetic must use methods beyond Presburger arithmetic, which will probably subsume Presburger Arithmetic itself. While formal consistency results have some meaningful technical consequences, from afar they often give off an aire of preaching to the converted. Anyone who accepts transfinite induction up to the ordinal in Gentzen's proof will probably have no problem accepting PA itself.