Я собираюсь задать довольно расплывчатый вопрос, поскольку грань между теоретической информатикой и математикой не всегда легко различить.
ВОПРОС: Известно ли вам о каком-либо интересном результате в CS, который либо не зависит от ZFC (т. Е. Стандартная теория множеств), либо который был первоначально доказан в ZFC (+ некоторая другая аксиома) и только позже доказан в ZFC alorne?
Я спрашиваю, потому что я близок к завершению своей кандидатской диссертации, и мой основной результат (определенность класса игр, которые используются для придания "семантики игры" вероятностному модальному вычислению) в настоящий момент доказан в ZFC распространяется на другие аксиомы (а именно отрицание гипотезы Континуума ¬ C H и аксиомы Мартина ).
Таким образом, настройка явно является информатикой (модальный калькуляция - это временная логика, и я расширяю ее для работы с вероятностными системами).
Я хотел бы привести в своей диссертации другие примеры (если вы их знаете) такого рода.
Заранее спасибо,
до свидания
Matteo
источник
Ответы:
Хотя я не знаю ни о каких таких результатах, кроме ваших собственных, я думаю, что вы могли бы немного расширить сферу и спросить: какие результаты в TCS были доказаны с использованием (любого рода) нестандартных аксиом. Под нестандартным здесь я подразумеваю нечто иное, чем классическая логика с ZF (или ZFC).
Прекрасным примером работы, которую я имею в виду, являются результаты Алекса Симпсона о свойствах языков программирования, использующих синтетическую теорию предметной области. Он использует интуиционистскую теорию множеств с аксиомами, которые противоречат классической логике.
Кроме того, Алекс и я использовали интуиционистские аксиомы с антиклассическими принципами непрерывности, чтобы показать результаты о вычислимости Банаха-Мазура.
Однако ни один из упомянутых примеров не имеет «открытого» статуса, как ваши доказательства, потому что мы знаем, что нестандартные аксиомы, которые мы использовали, могут быть поняты просто как работа внутри модели интуиционистской математики, где модель может быть показана как существующая в ZFC. Таким образом, нестандартная настройка - это действительно способ сделать вещи более элегантно, и в принципе они могут быть выполнены в прямом ZFC (хотя я боюсь думать о том, как именно это будет происходить).
источник
Это зависит от вашего определения "компьютерных наук". Возьмите пример ниже - это считается?
Кодирования целых чисел однозначно декодируемый бинарный код . Если длина кодовых слов не уменьшается, мы называем код монотонным . КодN являетсялучшечем кода C 2 , если | C 1 ( n ) | - | C 2 ( n ) | → - ∞ . Другими словами, для каждого L из некоторой точки на кодовых словах C 1 по меньшей мере LС1 С2 | С1( n ) | - | С2( n ) | → - ∞ L С1 L бит короче.
Набор кодов называется конфинально , если для каждого кода C есть код D ∈ S , который лучше , чем C . Это хорошо упорядочено, если оно упорядочено по отношению к «лучше». шкалаS С D ∈ S С является вполне упорядоченным конфинально набор кодов.
Вот два свойства, которые не зависят от ZFC:
источник
Утверждение определенности степени Тьюринга :
является следствием аксиомы определенности (AD), которая не зависит от ZF и несовместима с ZFC. Более слабое утверждение
является следствием теоремы Мартина о борелевской определимости, доказуемой в ZFC. Оба эти утверждения были изучены до того, как был доказан результат Мартина об определенности Бореля, когда было известно только, что они оба доказуемы в ZF + AD.
Второй приведенный результат имеет следующий интересный вывод: предположим, что - борелевское множество вещественных чисел, замкнутое по эквивалентности Тьюринга, такое, что для любого действительного bS б c ∈ S б ≤Tс S S
источник
Недавно я участвовал в беседе с одним из таких результатов, посвященным определению игр Büchi с одним счетчиком: Оливье Финкель, «Определенность бесконтекстных игр» , STACS 2012, http://drops.dagstuhl.de/opus/volltexte/2012/ 3389 / pdf / 5.pdf .
источник
Много конструктивной математики. См. Работу Пера Мартина-Лёфа о конструктивной теории множеств, используемой в качестве основы для языков программирования с зависимой типизацией.
источник