Wyniki w teoretycznej CS niezależnej od ZFC

Zadam dość niejasne pytanie, ponieważ granica między informatyką teoretyczną a matematyką nie zawsze jest łatwa do rozróżnienia.

PYTANIE: Czy znasz jakieś interesujące wyniki w CS, które są albo niezależne od ZFC (tj. Standardowa teoria zbiorów), albo które zostały pierwotnie udowodnione w ZFC (+ niektóre inne aksjomaty), a dopiero później udowodnione w ZFC alorne?

Pytam, ponieważ jestem bliski ukończenia pracy doktorskiej, a mój główny wynik (determinacja klasy gier, które są używane do nadania „semantyki gry” probabilistycznemu modalnemu obliczeniom) jest w tej chwili udowodniony w ZFC rozszerzony o inne aksjomaty (mianowicie zaprzeczenie hipotezy Continuum ¬ C H i Martin's Axiom M A ).$\mu$$\neg CH$$MA$

Tak więc ustawieniem jest wyraźnie Informatyka (modalny calculus jest logiką czasową i rozszerzam go na pracę z systemami probabilistycznymi).$\mu$

Chciałbym zacytować w mojej pracy inne przykłady tego rodzaju (jeśli są Państwo tego świadomi).

Z góry dziękuję,

PA

Matteo

Chociaż nie jestem świadomy żadnych takich wyników innych niż twoje, myślę, że możesz nieco rozszerzyć zakres i zapytać: jakie wyniki w TCS zostały udowodnione przy użyciu (dowolnego rodzaju) niestandardowych aksjomatów. Przez niestandardowy rozumiem tutaj coś innego niż klasyczna logika z ZF (lub ZFC).

Pięknym przykładem tego rodzaju pracy, którą mam na myśli, są wyniki Alexa Simpsona dotyczące właściwości języków programowania z wykorzystaniem syntetycznej teorii domen. Używa intuicyjnej teorii mnogości z aksjomatami sprzecznymi z logiką klasyczną.

Również Alex i ja zastosowaliśmy intuicyjne aksjomaty z antyklasycznymi zasadami ciągłości, aby pokazać wyniki dotyczące obliczalności Banacha-Mazura.

Jednak żaden z wymienionych przykładów nie ma statusu „otwartego”, podobnie jak twoje dowody, ponieważ wiemy, że stosowane przez nas niestandardowe aksjomaty można rozumieć po prostu jako działające w modelu matematyki intuicyjnej, w którym można wykazać, że model istnieje w ZFC. Tak więc niestandardowa konfiguracja jest naprawdę sposobem na bardziej eleganckie wykonanie i w zasadzie można to zrobić w prostej ZFC (chociaż boję się myśleć o tym, jak to dokładnie pójdzie).

To zależy od twojej definicji „informatyki”. Weź przykład poniżej - czy to się liczy?

$\mathbb{N}$$C_1$$C_2$$|C_1(n)| - |C_2(n)| \rightarrow -\infty$$L$$C_1$$L$

$S$$C$$D \in S$$C$

Oto dwie właściwości, które są niezależne od ZFC:

1. Istnieje skala kodów.
2. Istnieje skala kodów monotonicznych (tj. Dobrze uporządkowany zestaw kodów monotonicznych, który jest spójny w zestawie wszystkich kodów monotonicznych).

$D$$b \in D$$c$$b \leq_T c$$c \in D$

Stwierdzenie determinacji stopnia Turinga :

Każdy zestaw stopni Turinga zawiera stożek lub jest odłączony od jakiegoś stożka

jest konsekwencją aksjomatu determinacji (AD), który jest niezależny od ZF i niezgodny z ZFC. Słabsze stwierdzenie

Każdy zestaw reali Borela, który jest zamknięty w ramach równoważności Turinga, albo zawiera stożek, albo jest odłączony od stożka

jest konsekwencją twierdzenia Martina o determinacji Borela, którą można udowodnić w ZFC. Oba te stwierdzenia zostały zbadane, zanim udowodniono wynik Martina na determinacji Borela, w którym to czasie wiadomo było tylko, że oba można udowodnić w ZF + AD.

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

Niedawno uczestniczyłem w rozmowie z jednym z takich wyników, dotyczącej determinacji gier Büchi z jednym kontem: Olivier Finkel, Determinacja gier bezkontekstowych, STACS 2012, http://drops.dagstuhl.de/opus/volltexte/2012/ 3389 / pdf / 5.pdf .

Wiele konstruktywnej matematyki. Zobacz pracę Per Martina-Löfa nad konstruktywną teorią zbiorów, stosowaną jako podstawa dla języków programowania o typie zależnym.