Hasil dalam CS Teoritis independen dari ZFC

Saya akan mengajukan pertanyaan yang cukup samar, karena batas antara ilmu komputer teoretis dan matematika tidak selalu mudah dibedakan.

PERTANYAAN: Apakah Anda mengetahui adanya hasil menarik dalam CS yang tidak tergantung pada ZFC (yaitu teori himpunan standar), atau yang awalnya terbukti dalam ZFC (+ beberapa aksioma lainnya) dan baru kemudian terbukti di ZFC alorne?

Saya bertanya karena saya hampir menyelesaikan tesis PhD saya, dan hasil utama saya (penentuan kelas permainan yang digunakan untuk memberikan "permainan semantik" ke modal probabilistik calculus) saat ini terbukti dalam ZFC diperluas dengan Aksioma lain (yaitu negasi dari hipotesis Continuum dan, Aksioma Martin ).$\mu$$\neg CH$$MA$

Jadi pengaturannya jelas Ilmu Komputer (modal -calculus adalah logika temporal, dan saya memperluasnya untuk bekerja dengan sistem probabilistik).$\mu$

Saya ingin mengutip dalam tesis saya contoh-contoh lain (jika Anda mengetahui adanya) dari jenis ini.

Terima kasih sebelumnya,

selamat tinggal

Matteo

Meskipun saya tidak mengetahui adanya hasil seperti itu, selain hasil Anda sendiri, saya pikir Anda dapat memperluas cakupan dan bertanya: hasil apa dalam TCS yang telah terbukti menggunakan (jenis) aksioma non-standar. Dengan non-standar di sini saya maksudkan sesuatu selain logika klasik dengan ZF (atau ZFC).

Sebuah contoh indah dari jenis pekerjaan yang saya pikirkan adalah hasil Alex Simpson pada properti bahasa pemrograman menggunakan teori domain sintetik. Dia menggunakan teori himpunan intuitionistic dengan aksioma yang bertentangan dengan logika klasik.

Juga, Alex dan saya menggunakan aksioma intuitionistic dengan prinsip kontinuitas anti-klasik untuk menunjukkan hasil tentang komputabilitas Banach-Mazur.

Namun, tidak satu pun dari contoh yang disebutkan memiliki status "terbuka", seperti bukti Anda, karena kami tahu bahwa aksioma non-standar yang kami gunakan dapat dipahami hanya sebagai bekerja di dalam model matematika intuitionistic, di mana model dapat ditunjukkan ada di ZFC. Jadi pengaturan non-standar benar-benar cara menyelesaikan sesuatu dengan lebih elegan, dan pada prinsipnya mereka dapat dilakukan dalam ZFC langsung (walaupun saya takut memikirkan bagaimana tepatnya itu akan berjalan).

Itu tergantung pada definisi Anda tentang "Ilmu Komputer". Ambil contoh di bawah ini - apakah itu masuk hitungan?

Sebuah coding dari bilangan bulat adalah kode biner unik decodable dari . Jika panjang codeword tidak berkurang, kami menyebutnya kode monoton . Kode C 1 adalah lebih baik daripada kode C 2 jika | C 1 ( n ) | - | C 2 ( n ) | → - ∞ . Dengan kata lain, untuk setiap L , dari beberapa titik pada codeword dari C 1 setidaknya L bit lebih pendek.$\mathbb{N}$$C_1$$C_2$$|C_1(n)| - |C_2(n)| \rightarrow -\infty$$L$$C_1$$L$

Satu set kode disebut cofinal jika untuk setiap kode C ada kode D ∈ S yang lebih baik daripada C . Ini tertata dengan baik jika tertata dengan baik sehubungan dengan "lebih baik". Sebuah skala adalah satu set cofinal tertata dengan baik kode.$S$$C$$D \in S$$C$

Berikut adalah dua properti yang tidak tergantung pada ZFC:

1. Ada skala kode.
2. Ada skala kode monoton (yaitu seperangkat kode monoton yang tertata dengan baik yang merupakan cofinal dalam rangkaian semua kode monoton).

Sebuah kerucut derajat Turing adalah seperangkat derajat dengan beberapa dasar b ∈ D sehingga untuk semua derajat c , b ≤ T c jika dan hanya jika c ∈ D .$D$$b \in D$$c$$b \leq_T c$$c \in D$

Pernyataan penentuan derajat Turing :

Setiap set derajat Turing mengandung kerucut atau terpisah dari beberapa kerucut

adalah konsekuensi dari aksioma determinasi (AD), yang independen terhadap ZF dan tidak sesuai dengan ZFC. Pernyataan yang lebih lemah

Setiap rangkaian Borel real yang ditutup di bawah Turing equivalence baik mengandung kerucut atau terlepas dari kerucut

adalah konsekuensi dari teorema Martin tentang determinasi Borel, yang dapat dibuktikan dalam ZFC. Kedua pernyataan ini dipelajari sebelum hasil Martin pada determinasi Borel terbukti, pada saat itu hanya diketahui bahwa keduanya dapat dibuktikan dalam ZF + AD.

$S$$b$$c \in S$$b \leq_T c$$S$$S$

Baru-baru ini saya menghadiri ceramah dengan satu hasil seperti itu, untuk menentukan permainan Büchi satu-counter: Olivier Finkel, The Determinacy of Context-Free Games , STACS 2012, http://drops.dagstuhl.de/opus/volltexte/2012/ 3389 / pdf / 5.pdf .

Banyak matematika konstruktif. Lihat karya Per Martin-Löf tentang teori himpunan konstruktif, yang digunakan sebagai dasar untuk bahasa pemrograman yang diketik secara dependen.