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 ).
Tak więc ustawieniem jest wyraźnie Informatyka (modalny calculus jest logiką czasową i rozszerzam go na pracę z systemami probabilistycznymi).
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
źródło
Odpowiedzi:
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).
źródło
To zależy od twojej definicji „informatyki”. Weź przykład poniżej - czy to się liczy?
Oto dwie właściwości, które są niezależne od ZFC:
źródło
Stwierdzenie determinacji stopnia Turinga :
jest konsekwencją aksjomatu determinacji (AD), który jest niezależny od ZF i niezgodny z ZFC. Słabsze stwierdzenie
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.
źródło
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 .
źródło
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.
źródło