Apakah ada konsep ganda untuk "Turing Lengkap" dalam logika?

Dua model komputasi dapat ditunjukkan saling melengkapi jika masing-masing dapat menyandikan simulator universal untuk yang lain. Dua logika dapat ditunjukkan untuk melengkapi jika suatu pengkodean aturan inferensi (dan mungkin aksioma jika ada) dari masing-masing ditunjukkan sebagai teorema dari yang lain. Dalam komputabilitas ini telah mengarah pada gagasan alami kelengkapan Turing dan Tesis Gereja Turing. Namun, saya belum melihat di mana kelengkapan co logis telah menyebabkan ide yang diinduksi secara alami kelengkapan total kualitas yang sama.

Karena Provabilitas dan Komputasi sangat erat kaitannya, jadi saya pikir tidak terlalu banyak untuk mempertimbangkan bahwa mungkin ada konsep dalam logika yang merupakan ganda alami untuk Turing Completeness. Secara spekulatif, sesuatu seperti: ada teorema "benar" yang tidak dapat dibuktikan dalam logika jika dan hanya jika ada fungsi yang dapat dihitung yang tidak dapat dijelaskan oleh model komputasi. Pertanyaan saya adalah, adakah yang mempelajari ini? Referensi atau kata kunci akan sangat membantu.

Dengan "true" dan "computable" pada paragraf sebelumnya saya merujuk pada ide-ide intuitif tetapi akhirnya tidak dapat didefinisikan. Sebagai contoh, seseorang dapat menunjukkan bahwa urutan rangkaian Goodstein "benar" tetapi tidak dapat dibuktikan dalam aritmatika Peano tanpa sepenuhnya mendefinisikan konsep "benar". Demikian pula, dengan diagonalisasi dapat ditunjukkan bahwa ada fungsi yang dapat dihitung yang tidak primitif rekursif tanpa benar-benar sepenuhnya mendefinisikan konsep yang dapat dihitung. Saya bertanya-tanya, meskipun pada akhirnya cenderung konsep empiris, mungkin konsep-konsep tersebut dapat saling terkait dengan cukup baik untuk menghubungkan konsep kelengkapan.

Saya tidak yakin mengapa Anda mengatakan "benar" pada akhirnya tidak dapat didefinisikan, karena ada definisi yang tepat untuk apa artinya formula urutan pertama menjadi benar .

Apa yang unik dalam hal komputasi, adalah bahwa untuk definisi apa pun (sesering impian Anda) untuk "model komputasi", Anda akhirnya dapat mengaitkannya dengan serangkaian fungsi (fungsi yang dapat dikomputasi). Dengan demikian, Anda secara alami dapat membandingkan model yang berbeda, dan setelah memperbaikinya (berdasarkan beberapa pembenaran empiris seperti "itu adalah representasi yang baik dari perhitungan di dunia nyata") Anda dapat memanggil model lain yang lengkap jika menghitung seperangkat yang sama persis fungsi.

Namun, bagaimana Anda membandingkan berbagai logika? Tampaknya tidak ada properti alami yang dapat Anda lampirkan pada logika sewenang-wenang, dan menggunakannya untuk membandingkannya dengan sistem lain. Anda mungkin dapat, memperbaiki logika, misalnya logika predikat urutan pertama, dan bertanya tentang kelengkapan sistem aksiomatik. Misalkan Anda bekerja di ZFC, dan percaya itu terdiri dari aksioma alami yang mewakili dunia. Sekarang, ketika diberi sistem aksiomatik yang berbeda, Anda dapat bertanya apakah mereka memiliki teori yang sama, dan menyebut sistem ini lengkap jika jawabannya adalah ya. Saya pikir perbedaan dari kasus komputabilitas, adalah bahwa untuk komputabilitas, ada konsensus yang lebih kuat tentang apa "model dasar" seharusnya. Alasan untuk konsensus ini adalah bahwa banyak model komputasi independen kemudian terbukti setara,