Jabarkan Konsistensi dari Aksioma Peano

Ketika aksioma Peano pertama kali diusulkan, Bertrand Russell dan yang lainnya setuju bahwa aksioma tersebut secara tersirat mendefinisikan apa yang dimaksud sebagai "bilangan asli". Henri Poincaré lebih hati-hati, mengatakan bahwa aksioma tersebut hanya mendefinisikan bilangan asli apabila mereka konsisten; jika terdapat bukti yang dimulai hanya dari aksioma itu dan menghasilkan kontradiksi seperti 0 = 1, maka aksioma itu tidak konsisten, dan tidak mendefinisikan apapun. Pada tahun 1900, David Hilbert mengajukan masalah membuktikan konsistensi aksioma Peano hanya menggunakan metode finitis sebagai masalah kedua dari kedua-puluh-tiga masalahnya. Pada tahun 1931, Kurt Gödel membuktikan teorema ketaklengkapan keduanya, yang menunjukkan bahwa bukti konsistensi seperti itu tidak bisa diformalisasikan dalam aritmetika Peano itu sendiri.

Meskipun kerap dikatakan bahwa teorema Gödel menunjukkan bahwa bukti konsistensi finistis untuk aritmetika Peano tidak mungkin dibuat, ini bergantung pada apa yang dimaksud dengan bukti finistis. Gödel sendiri mengatakan bahwa bisa saja dibuat bukti konsistensi finistis untuk aritmetika Peano atau sistem yang lebih kuat dengan menggunakan metode finistis yang tidak bisa diformalisasikan dalam aritmetika Peano, dan pada tahun 1958, Gödel menerbitkan sebuah metode untuk membuktikan konsistensi aritmetika menggunakan teori tipe. Pada tahun 1936, Gerhard Gentzen memberikan bukti konsistensi aksioma Peano, menggunakan induksi transfinit hingga bilangan ordinal yang disebut ε0. Gentzen menjelaskan: "Tujuan dari karangan ini adalah untuk membuktikan konsistensi dari teori bilangan dasar atau, lebih tepatnya, untuk mereduksi pertanyaan konsistensi ke prinsip-prinsip dasar tertentu". Bukti Gentzen bisa jadi finitis, karena ordinal transfinit ε0 bisa dituliskan dalam bentuk objek-objek terhingga (contohnya, sebagai mesin Turing yang menggambarkan urutan yang cocok pada bilangan bulat, atau lebih abstraknya sebagai terdiri dari pohon yang terhingga, yang diurutkan linear sehingga cocok). Apakah bukti Gentzen memenuhi syarat yang Hilbert berikan atau tidak bukanlah hal yang jelas: tidak ada definisi yang diterima secara umum mengenai apa yang dimaksud bukti finistis, dan Hilbert sendiri tidak pernah memberikan definisi yang saksama.

Mayoritas matematikawan percaya bahwa aksioma Peano bersifat konsisten, atas dasar intuisi mereka atau menerima bukti konsistensi seperti yang diberikan Gentzen. Sebagian kecil filsuf dan matematikawan, yang sebagian mendukung ultrafinitisme, menolak aksioma Peano karena menerimanya berarti menerima kumpulan bilangan asli yang tak berhingga. Khususnya, penambahan (termasuk fungsi penerus) dan perkalian diasumsikan bersifat total. Menariknya, terdapat teori self-verifying yang mirip dengan aksioma Peano tetapi terdiri dari pengurangan dan pembagian bukannya penambahan dan perkalian, yang diaksiomakan sedemikian rupa sehingga tidak membuktikan bahwa penambahan dan perkalian bersifat total, tetapi masih bisa membuktikan semua teorema  yang benar dari aksioma Peano, dan bisa diperluas menjadi teori konsisten yang membuktikan konsistensinya sendiri (dalam arti tidak bisa dibuat bukti "0=1").