Aksioma diperlukan untuk ilmu komputer teoretis

Pertanyaan ini diilhami oleh pertanyaan serupa tentang matematika terapan pada aliran matematika, dan pemikiran itu mengomentari bahwa pertanyaan penting TCS seperti P vs. NP mungkin independen dari ZFC (atau sistem lain). Sebagai sedikit latar belakang, matematika terbalik adalah proyek untuk menemukan aksioma yang diperlukan untuk membuktikan teorema penting tertentu. Dengan kata lain, kita mulai pada satu set teorema yang kita harapkan benar dan mencoba untuk memperoleh set minimal aksioma 'alami' yang membuatnya begitu.

Saya bertanya-tanya apakah pendekatan matematika terbalik telah diterapkan pada teorema penting TCS. Khususnya pada teori kompleksitas. Dengan kebuntuan pada banyak pertanyaan terbuka di TCS tampaknya wajar untuk bertanya "aksioma apa yang belum kita coba gunakan?". Atau, apakah ada pertanyaan penting dalam TCS yang terbukti independen dari subsistem sederhana tertentu dari aritmatika tingkat dua?

cc.complexity-theory lo.logic proof-complexity Artem Kaznatcheev
sumber

Dua aksioma yang mungkin tidak independen: 1) 3-SAT membutuhkan

waktu. 2) Mengingat satisfiable rumus 3SAT, setiap efisien algoritma memenuhi paling

-fraction dari klausa. Selain itu, perkalian dua bilangan prima dengan ukuran yang sama sulit untuk dibalik (efisien).

2^{Ω (n)}

$2^{\Omega(n)}$

7 / 8

$7/8$

Mohammad Al-Turkistany

Makalah ini relevan: Harry Buhrman, Lance Fortnow, Leen Torenvliet, "Enam Hipotesis Mencari Teorema," CCC, hal.2, Konferensi IEEE Tahunan ke-12 tentang Kompleksitas Komputasi (CCC'97), 1997

Mohammad Al-Turkistany

Pertanyaan berikut terkait: cstheory.stackexchange.com/questions/1923/... Sebagian besar TCS dapat diformalkan dalam RCA_0. Teorema minor grafik adalah pengecualian langka. Seperti yang ditekankan Neel, jika Anda menginginkan ide-ide baru, maka cari ide-ide baru; jangan mencari aksioma baru. Keduanya sama sekali tidak sama.

Timothy Chow

Saya bingung mengapa hasil seperti pernyataan pada

atau

dinyatakan. Dalam kuliah TCS pertama saya, kami mulai dengan bilangan asli dan beberapa fungsi dasar. Sisanya mengikuti. Ternyata saya tidak mengerti pertanyaannya.

P

$P$

N P

$NP$

Raphael

Saya hanya memperhatikan ini, tetapi ternyata Lipton mengajukan pertanyaan serupa di posting ini: rjlipton.wordpress.com/2011/02/03/… , mengutip: "Saya ingin tahu apakah ada teknik bukti yang melibatkan ide-ide yang jauh melampaui PA yang kami miliki tidak digunakan, dan mana yang akan membantu memecahkan beberapa masalah penting. Haruskah kita mengajarkan metode kepada mahasiswa pascasarjana kita dari bidang matematika yang berada di luar PA? " (PA = Aritmetika Peano)

Artem Kaznatcheev

Jawaban:

Ya, topik tersebut telah dipelajari dalam kompleksitas bukti. Ini disebut Bounded Reverse Mathematics . Anda dapat menemukan tabel yang berisi beberapa hasil matematika terbalik pada halaman 8 dari buku Cook dan Nguyen, " Yayasan Logical of Proof Complexity ", 2010. Beberapa siswa Steve Cook sebelumnya telah mengerjakan topik yang sama, misalnya tesis Nguyen, " Bounded Reverse Mathematics " , Universitas Toronto, 2008.

Alexander Razborov (juga teori kompleksitas bukti lainnya) memiliki beberapa hasil pada teori-teori lemah yang diperlukan untuk memformalkan teknik kompleksitas sirkuit dan membuktikan kompleksitas sirkuit rendah. Ia memperoleh beberapa hasil yang tidak dapat dibuktikan untuk teori-teori yang lemah, tetapi teorinya dianggap terlalu lemah.

Semua hasil ini dapat dibuktikan di (teori dasar Simpson UNTUK REVERSE Matematika), sehingga AFAIK kami tidak memiliki hasil kemerdekaan dari teori yang kuat (dan pada kenyataannya hasil kemerdekaan tersebut akan memiliki konsekuensi yang kuat sebagai Neel telah disebutkan, lihat Ben kerja -David (dan hasil terkait) pada kemandirian dari di mana adalah perluasan dari ). $RCA_0$ $\mathbf{P} vs. \mathbf{NP}$ $PA_1$ $PA_1$ $PA$

Kaveh
sumber

Hasil kemandirian seperti itu akan menjadi terobosan besar, tetapi saya tidak berpikir mereka memiliki konsekuensi langsung yang kuat; lihat komentar saya tentang jawaban Neel.

Timothy Chow

@Tim, terima kasih, Anda benar, saya memperbaiki jawaban saya. Ini bukan

, itu adalah

diperluas dengan semua kalimat universal aritmatika, dan Ben-David mengklaim bahwa jika pertanyaannya independen dari teori yang lebih kuat ini, maka SAT memiliki algoritma waktu yang hampir polinomial. Jadi asumsinya (jauh) lebih kuat tetapi klaim akhir adalah sama. (dan saat ini dikenal metode untuk membuktikan kemerdekaan dari

juga akan berarti kemerdekaan dari

P A

$PA$

P A_{1}

$PA_1$

P A

$PA$

P A

$PA$

P A_{1}

$PA_1$

Kaveh

Sebagai jawaban positif untuk pertanyaan akhir Anda, bukti normalisasi kalkulus lambda polimorfik seperti kalkulus konstruksi memerlukan setidaknya aritmatika tingkat tinggi, dan sistem yang lebih kuat (seperti kalkulus konstruksi induktif) sama dengan ZFC plus banyak sekali aksesibilitas.

Sebagai jawaban negatif atas pertanyaan akhir Anda, Ben-David dan Halevi telah menunjukkan bahwa jika independen dari , Peano aritmatika diperpanjang dengan aksioma untuk semua kebenaran aritmatika universal, maka ada algoritma hampir polinomial untuk SAT. Selain itu, saat ini tidak ada cara yang diketahui untuk menghasilkan kalimat yang independen dari tetapi tidak . $P \not= NP$ $PA_1$ $DTIME(n^{\log^{*}(n)})$ $PA$ $PA_1$

Secara lebih filosofis, jangan membuat kesalahan dengan menyamakan kekuatan konsistensi dengan kekuatan abstraksi.

Cara yang benar untuk mengatur subjek mungkin melibatkan prinsip-prinsip teori set liar, walaupun mereka mungkin tidak benar-benar diperlukan dalam hal kekuatan konsistensi. Sebagai contoh, prinsip pengumpulan yang kuat sangat berguna untuk menyatakan sifat keseragaman - misalnya, ahli teori kategori akhirnya menginginkan aksioma kardinal besar yang lemah untuk memanipulasi hal-hal seperti kategori semua kelompok seolah-olah mereka objek. Contoh yang paling terkenal adalah geometri aljabar, yang perkembangannya memanfaatkan alam semesta Grothendieck secara ekstensif, tetapi semua aplikasinya (seperti Teorema Terakhir Fermat) tampaknya berada dalam aritmatika orde ketiga. Sebagai contoh yang jauh lebih sepele, perhatikan bahwa operasi identitas dan komposisi generik tidak berfungsi, karena mereka diindeks di seluruh alam semesta set.

$\sigma$ $X$ $X$

EDIT: Sistem logis A memiliki kekuatan konsistensi yang lebih besar daripada sistem B, jika konsistensi A menyiratkan konsistensi B. Misalnya, ZFC memiliki kekuatan konsistensi yang lebih besar daripada aritmatika Peano, karena Anda dapat membuktikan konsistensi PA dalam ZFC. A dan B memiliki kekuatan konsistensi yang sama jika keduanya sama. Sebagai contoh, aritmatika Peano konsisten jika dan hanya jika aritmetika Heyting (konstruktif) adalah.

IMO, salah satu fakta paling menakjubkan tentang logika adalah bahwa kekuatan konsistensi bermuara pada pertanyaan "apa fungsi yang paling cepat berkembang yang dapat Anda buktikan total dalam logika ini?" Akibatnya, konsistensi banyak kelas logika dapat dipesan secara linear! Jika Anda memiliki notasi ordinal yang mampu menggambarkan fungsi yang paling cepat berkembang, kedua logika Anda dapat menunjukkan total, maka Anda tahu dengan trikotomi bahwa salah satu dapat membuktikan konsistensi yang lain, atau keduanya sama-sama konsisten.

Tetapi fakta yang mencengangkan ini juga mengapa kekuatan konsistensi bukan alat yang tepat untuk berbicara tentang abstraksi matematis. Ini adalah invarian dari suatu sistem termasuk trik pengkodean, dan abstraksi yang baik memungkinkan Anda mengekspresikan ide tanpa trik. Namun, kami tidak cukup tahu tentang logika untuk mengekspresikan ide ini secara formal.

Neel Krishnaswami
sumber

apa 'kekuatan konsistensi'?

Suresh Venkat

Bukan itu yang dibuktikan Ben-David dan Halevi. Anda mengabaikan pengendara penting mereka, "menggunakan teknik yang tersedia saat ini." Saya menafsirkan makalah mereka sebagai menekankan betapa lemahnya teknik bukti kita saat ini daripada mengatakan banyak tentang pertanyaan P = NP.

Timothy Chow