Apakah bentuk rekursif dari pernyataan Godel itu mungkin?

Referensi-diri dari masalah P / NP kadang-kadang telah disorot sebagai penghalang untuk penyelesaiannya, lihat, misalnya, makalah Scott Aaronson, apakah P vs. NP independen secara formal ? Salah satu dari banyak resolusi yang dapat dipikirkan untuk P / NP akan menjadi sebuah demonstrasi bahwa masalahnya secara formal independen dari ZFC atau benar tetapi tidak dapat dibuktikan.

Dapat dibayangkan bahwa pengarahan diri sendiri dari masalah dapat menimbulkan tantangan yang lebih dalam dalam bukti-bukti kemandirian, misalnya, jika pernyataan tentang provabilitasnya sendiri tidak dapat dibuktikan atau tidak mungkin dipikirkan.

Misalkan kita menyebut teorema T Godel_0 jika itu benar tetapi tidak dapat dibuktikan dalam pengertian teorema Godel. Panggil T Godel_1 jika pernyataan "T is Godel_0" benar, tetapi tidak dapat dibuktikan. Panggil T Godel_i jika pernyataan "T is Godel _ {(i-1)} benar.

Kita tahu bahwa pernyataan Godel_0 ada, dan beberapa contoh telah ditemukan "di alam liar" yang tidak dibangun secara eksplisit untuk tujuan ini, seperti dalam artikel ini .

Pertanyaan saya adalah: apakah ada pernyataan Godel_1 atau lebih tinggi? Apakah pernyataan seperti itu merupakan konsekuensi alami dari teorema Godel?

Bagaimana dengan pernyataan yang tidak dapat kita buktikan sama sekali: yaitu, yang untuk setiap k > 0, T adalah Godel_k?

Saya dapat mengajukan pertanyaan analog untuk kemerdekaan formal, meskipun saya curiga jawabannya adalah "tidak" di sana.

Untuk kembali ke pertanyaan P vs NP, izinkan saya bertanya apakah ada petunjuk bahwa teorema Godel relevan dengan pertanyaan tentang keterpisahan kelas. Adakah pernyataan yang benar tetapi tidak dapat dibuktikan telah diidentifikasi sehubungan dengan kelas kompleksitas - di luar, tentu saja, hubungan yang jelas antara menghentikan masalah dan teorema Godel?

Seperti yang telah ditunjukkan orang lain, ada kesulitan teknis tertentu dengan pernyataan pertanyaan Anda. Untuk meluruskannya, mari kita mulai dengan menghindari penggunaan istilah "tidak dapat dibuktikan" tanpa kualifikasi, dan secara eksplisit tentang set aksioma yang mana dari pernyataan Anda T seharusnya tidak dapat dibuktikan. Sebagai contoh, anggaplah kita tertarik pada pernyataan T yang tidak dapat dibuktikan dari PA, aksioma aritmatika Peano orde pertama.

Gangguan pertama adalah bahwa "T benar" tidak dapat diungkapkan dalam bahasa aritmatika tingkat pertama, oleh teorema Tarski. Kita bisa menyiasatinya dengan bekerja di metateori yang cukup kuat untuk mendefinisikan kebenaran pernyataan aritmatika, tetapi saya pikir untuk tujuan Anda ini adalah rute rumit yang tidak perlu untuk diambil. Saya pikir Anda tidak begitu tertarik pada kebenaran, tetapi pada provabilitas. Yaitu, saya menduga Anda akan puas dengan mendefinisikan T sebagai Godel_0 jika T benar tetapi tidak dapat dibuktikan dalam PA, dan mendefinisikan T menjadi Godel_1 jika T tidak dapat dibuktikan dalam PA tetapi "T tidak dapat dibuktikan di PA" tidak dapat dibuktikan di PA, tidak dapat dibuktikan di PA, dan mendefinisikan T menjadi Godel_2 jika T tidak dapat dibuktikan dalam PA dan "T tidak dapat dibuktikan dalam PA" tidak dapat dibuktikan dalam PA tetapi "'T tidak dapat dibuktikan dalam PA' tidak dapat dibuktikan dalam PA" tidak dapat dibuktikan dalam PA "tidak dapat dibuktikan dalam PA, dll. Dengan cara itu kita tidak

Ini sudah cukup untuk membuat pertanyaan Anda tepat, tetapi sayangnya ada solusi yang agak sepele. Ambil T = "PA konsisten." Maka T benar karena PA konsisten, dan T tidak dapat dibuktikan dalam PA oleh teorema ketidaklengkapan 2 Goedel. Lebih lanjut, "T tidak dapat dibuktikan dalam PA" juga tidak dapat dibuktikan dalam PA untuk alasan yang agak konyol: pernyataan apa pun dari bentuk "X tidak dapat dibuktikan dalam PA" tidak dapat dibuktikan dalam PA karena "X tidak dapat dibuktikan dalam PA" secara sepele menyiratkan "PA konsisten" "(karena sistem yang tidak konsisten membuktikan segalanya ). Jadi T adalah Godel_n untuk semua n, tapi saya tidak benar-benar mengerti pertanyaan yang Anda maksudkan.

Kami dapat mencoba "menambal" pertanyaan Anda untuk menghindari hal-hal sepele seperti itu, tetapi saya akan mencoba menjawab apa yang menurut saya adalah pertanyaan yang Anda maksudkan. Secara diam-diam, saya percaya Anda sedang menyatukan kekuatan logis yang dibutuhkan untuk membuktikan teorema dengan kesulitan psikologisuntuk membuktikannya. Artinya, Anda menafsirkan hasil dari bentuk "T tidak dapat dibuktikan dalam X" sebagai mengatakan bahwa T entah bagaimana di luar kemampuan kita untuk memahami. Ada dugaan mengerikan di luar sana, dan kami orang-orang lemah memecahkan cambuk PA atau cambuk ZFC atau apa yang telah Anda lakukan pada binatang buas itu, mencoba menjinakkannya. Tetapi saya tidak berpikir bahwa "T tidak dapat dibuktikan dalam X" harus ditafsirkan sebagai makna "T tidak mungkin untuk dipikirkan." Sebaliknya, ini hanya mengukur sifat teknis tertentu tentang T, yaitu kekuatan logisnya. Jadi, jika Anda mencoba untuk membuat monster über, saya tidak berpikir bahwa menemukan sesuatu yang tidak hanya tidak dapat dibuktikan, tetapi yang tidak dapat dibuktikan tidak dapat dibuktikan, dll, adalah arah yang tepat untuk pergi.

Akhirnya, sehubungan dengan pertanyaan Anda tentang apakah unprovability tampaknya terkait dengan pemisahan kelas kompleksitas, ada beberapa koneksi antara intraktabilitas komputasi dan unprovability dalam sistem aritmatika terbatas tertentu. Beberapa di antaranya disebutkan di koran oleh Aaronson yang Anda kutip; lihat juga buku Cook dan Nguyen, Logical Foundations of Proof Complexity .

Saya tidak begitu yakin tentang definisi Godel_1. Bisakah Anda mencoba memformalkannya sedikit lagi?

Bagaimana Anda bisa menyandikan rumus "T is Godel_0"? Untuk itu Anda perlu menyandikan bahwa "T benar secara semantik" tanpa merujuk pada gagasan pembuktian. Bagaimana kamu bisa melakukan itu?

Pernyataan Godel_n ada untuk setiap n. Anda mungkin tertarik pada The Unprovability of Consistency, sebuah buku karya George Boolos. Dia mendefinisikan logika modal di mana Box berarti "dapat dibuktikan," Diamond berarti "konsisten," dan kemudian mulai menyelidiki perilaku kalimat tipe Godel. (Dia menulis buku lanjutan, The Logic of Provability, juga.)