Какие интересные теоремы в TCS опираются на Аксиому выбора? (Или, в качестве альтернативы, Аксиома Определенности?)

67

Иногда математики беспокоятся об аксиоме выбора (AC) и аксиоме детерминированности (AD).

Аксиома выбора : При любом наборе непустых множеств существует функция F , что, учитывая множество S в C , возвращает элемент из S .CfSCS

Аксиома детерминированности : Пусть - набор бесконечно длинных битовых строк. Алиса и Боб играют в игру, в которой Алиса выбирает 1-й бит b 1 , Боб выбирает 2-й бит b 2 и так далее, пока не будет построена бесконечная строка x = b 1 b 2 . Алиса выигрывает , если х S , Боб выигрывает , если х S . Предполагается, что для каждого S есть выигрышная стратегия для одного из игроков. (Например, если S состоит только из строки «все единицы», Боб может выиграть за конечное число ходов.)Sb1b2x=b1b2xSxS SS

Известно, что эти две аксиомы несовместимы друг с другом. (Подумай об этом или иди сюда .)

Другие математики почти не обращают внимания на использование этих аксиом в доказательстве. Казалось бы, они почти не имеют отношения к теоретической информатике, поскольку мы считаем, что мы работаем в основном с конечными объектами. Однако, поскольку TCS определяет задачи вычислительного решения как бесконечные битовые строки, и мы измеряем (например) временную сложность алгоритма как асимптотическую функцию над натуральными числами, всегда существует вероятность того, что использование одной из этих аксиом может привести к ползучести в некоторые доказательства.

Какой самый яркий пример в TCS, что вы знаете, где требуется одна из этих аксиом ? (Вы знаете какие-нибудь примеры?)

Отметим, что аргумент диагонализации (скажем, над множеством всех машин Тьюринга) не является применением Аксиомы выбора. Хотя язык, который определяет машина Тьюринга, представляет собой бесконечную битовую строку, каждая машина Тьюринга имеет конечное описание, поэтому нам действительно не требуется функция выбора для бесконечного множества бесконечных множеств.

(Я поместил много тегов, потому что понятия не имею, откуда будут взяты примеры.)

Райан Уильямс
источник
CW? или нет ? Точно сказать не могу.
Суреш Венкат
Я тоже не уверен ... это один вопрос, в котором я очень не уверен насчет "сложности" ответа ...
Райан Уильямс
5
Другие математики почти не обращают внимания на использование этих аксиом в доказательстве. Действительно ли математики небрежно используют обе аксиомы? Если вы случайно приняли обе аксиомы, вы можете доказать что угодно!
Уоррен Шуди
1
Гипотеза Харви Фридмана . Я не знаю, относится ли это также к теоретической информатике.
Каве
1
Я не знаю никакого результата в теоретической информатике, который не может быть доказан в ZF, но может быть доказан в некотором интересном расширении ZF. Тем не менее, мое дикое предположение состоит в том, что даже такие результаты, вероятно, не потребуют полной аксиомы выбора (AC), и что они требуют только более слабой версии AC, такой как аксиома зависимого выбора (DC) или даже более слабая аксиома счетного выбор (AC_ω). Кроме того, DC (и, следовательно, AC_ω) согласуется с аксиомой определенности .
Цуёси Ито

Ответы:

47

Любое арифметическое утверждение, доказуемое в ZFC, доказуемо в ZF и, следовательно, не «нуждается» в аксиоме выбора. Под «арифметическим» утверждением я подразумеваю утверждение на языке арифметики первого порядка, означающее, что оно может быть указано с использованием только квантификаторов над натуральными числами («для всех натуральных чисел x» или «существует натуральное число x»), без количественного определения по множествам натуральных чисел. На первый взгляд может показаться очень ограничительным запрещать количественное определение наборов целых чисел; однако, конечные наборы целых чисел могут быть «закодированы» с использованием единственного целого числа, поэтому можно количественно определять конечные наборы целых чисел.

Практически любое заявление о заинтересованности в TCS, возможно, с небольшим количеством сомнений, может быть сформулировано как арифметическое утверждение, и поэтому не нуждается в аксиоме выбора. Например, PNP на первый взгляд выглядит как утверждение о бесконечных наборах целых чисел, но его можно перефразировать следующим образом: «для каждой машины Тьюринга за полиномиальное время существует экземпляр SAT, который он получает неправильно», который является арифметическим заявление. Таким образом, мой ответ на вопрос Райана: «Я не знаю ни одного».

Но подождите, вы можете сказать, как насчет арифметических утверждений, для доказательства которых требуется нечто вроде леммы Кенига или теоремы Крускала о дереве? Разве это не требует слабой формы аксиомы выбора? Ответ заключается в том, что все зависит от того, как именно вы сформулируете нужный результат. Например, если вы сформулируете теорему о второстепенном графе в виде: «для любого бесконечного набора немаркированных графов должно существовать два из них, так что один является второстепенным для другого», то для перехода через некоторое количество необходимо некоторое количество выбора. ваш бесконечный набор данных, выбирая вершины, подграфы и т. д. [ПРАВИТЬ: я сделал ошибку здесь. Как объясняет Эмиль Йержабектеорема о второстепенном графе - или, по крайней мере, самое естественное ее утверждение в отсутствие AC - доказуема в ZF. Но по модулю этой ошибки то, что я скажу ниже, все еще по существу верно. ] Однако если вместо этого вы записываете определенную кодировку с помощью натуральных чисел минорного отношения на помеченных конечных графах и формулируете теорему второстепенного графа как утверждение об этом конкретном частичном порядке, то это утверждение становится арифметическим и не требует AC в доказательство.

Большинству людей кажется, что «комбинаторная сущность» теоремы о второстепенном графе уже уловлена ​​версией, которая исправляет определенную кодировку, и что необходимо вызывать AC для маркировки всего, в случае, если вам предоставляется общий набор Теоретическая версия проблемы является своего рода не относящимся к делу артефактом решения использовать теорию множеств, а не арифметику в качестве логического основания. Если вы чувствуете то же самое, то теорема о второстепенном графе не требует AC. (См. Также этот пост Али Энайата в список рассылки «Основы математики», написанный в ответ на похожий вопрос, который у меня когда-то был.)

Пример хроматического числа плоскости также является вопросом интерпретации. Существуют различные вопросы, которые вы можете задать, которые оказываются эквивалентными, если вы принимаете AC, но это разные вопросы, если вы не принимаете AC. С точки зрения TCS, комбинаторное сердце вопроса - это цветность конечных подграфов плоскости, а также тот факт, что вы можете (если хотите) использовать аргумент компактности (вот где появляется AC), чтобы заключить что-то Насчет хроматического числа всей плоскости забавно, но в некоторой степени тангенциально. Поэтому я не думаю, что это действительно хороший пример.

Я думаю, что в конечном итоге вам, возможно, повезет больше, если вы спросите, существуют ли какие-либо вопросы TCS, требующие больших кардинальных аксиом для их разрешения (а не AC). Работа Харви Фридмана показала, что некоторые конечные утверждения в теории графов могут требовать больших кардинальных аксиом (или, по крайней мере, 1-согласованности таких аксиом). Пока что примеры Фридмана немного искусственны, но я не удивлюсь, если подобные примеры будут «естественно» появляться в TCS в течение наших жизней.

Тимоти Чоу
источник
8
Для доказательства нормализации для типизированного лямбда-исчисления с полиморфизмом требуется как минимум арифметика 2-го порядка, а для того, чтобы показать то же самое для более щедрых теорий типов, могут потребоваться большие кардинальные аксиомы, хотя и довольно скромные. IIRC, для доказательства нормализации Coq требуется много недоступных, так как вы можете использовать его для кодирования аргументов юниверса в стиле Гротендика.
Нил Кришнасвами
3
@Neel: Хорошая мысль, хотя IMO эти примеры «обманывают», потому что очевидно, что вам могут понадобиться сильные логические аксиомы, чтобы доказать непротиворечивость логической системы.
Тимоти Чоу
4
Мне нравится этот ответ, потому что он объясняет, почему использование аксиомы выбора в TCS кажется крайне редким.
Цуёси Ито
1
Этот ответ размещен в блоге сообщества.
Аарон Стерлинг
39

Насколько я понимаю, в известном доказательстве теоремы Робертсона-Сеймура используется Аксиома выбора (с помощью теоремы Крускала о дереве). Это очень интересно с точки зрения TCS, поскольку теорема Робертсона-Сеймура подразумевает, что тестирование принадлежности в любом заданном минор-замкнутом семействе графов может быть выполнено за полиномиальное время. Другими словами, Аксиома выбора может использоваться косвенно, чтобы доказать, что алгоритмы полиномиального времени существуют для определенных задач, без фактического построения этих алгоритмов.

Однако это может быть не совсем то, что вы ищете, так как неясно, действительно ли здесь требуется AC.

Янне Х. Корхонен
источник
Это хорошее начало, так как неизвестно, как доказать теорему иначе.
Райан Уильямс
7
Как упомянуто на странице Википедии, статья Фридмана, Робертсона и Сеймура о метаматематике теоремы о младшем графе показывает, что теорема о второстепенном графе подразумевает (форму) теоремы Крускала о дереве над базовой теорией RCA_0, поэтому это устанавливает, что Крускал Теорема о дереве требуется для теоремы о графе в сильном смысле. Однако означает ли это, что аксиома выбора требуется для теоремы о второстепенном графе, - вопрос немного хитрый. Это тонким образом зависит от того, как вы решите сформулировать второстепенную теорему о графе. Смотрите мой ответ для более подробной информации.
Тимоти Чоу
7
Эмиль Йержабек показал на MathOverflow, как доказать теорему Робертсона-Сеймура без аксиомы выбора. Это было удивительно для меня, потому что у меня также было впечатление, что Робертсон-Сеймур для немаркированных графов требует AC, но это, очевидно, было неверным впечатлением.
Тимоти Чоу
Таким образом, принятый ответ на самом деле ложный?
Андрей Бауэр
@AndrejBauer: Если вы ссылаетесь на мой ответ, вы правы в том, что то, что я сказал о Робертсоне-Сеймуре, неверно. Я пытался редактировать свой ответ только сейчас, но не смог. Может быть, у меня недостаточно репутации, чтобы редактировать такой старый пост.
Тимоти Чоу
21

Это относится к ответу, который дал Янне Корхонен.

В 80-х и 90-х годах был поток результатов, которые пытались охарактеризовать системы аксиом (иными словами, арифметическую теорию), необходимые для доказательства расширений теоремы Крускала (KTT; оригинальный KTT относится к 1960 году). В частности, Харви Фридман доказал несколько результатов, следуя этой линии (см. С.Г. Симпсон. Недоказуемость некоторых комбинаторных свойств конечных деревьев . В работе Л.А. Харрингтона и др., Редактора исследования Харви Фридмана по основам математики. Elsevier, Северная Голландия, 1985) , Эти результаты показали, что (некоторые расширения) KTT должны использовать «сильные» аксиомы понимания (т. Е. Аксиомы, говорящие о существовании определенных наборов высокой логической сложности). Я не знаю точно о доказуемости расширений KTT в ZF (без аксиомы выбора).

Параллельно с этим потоком результатов была предпринята попытка подключить его к («Теория B») TCS через системы перезаписи . Идея состоит в том, чтобы построить системы перезаписи (представьте, что это своего рода функциональное программирование или программы лямбда-исчисления), для которых их завершение зависит от определенных (расширений) KTT (первоначальная связь между KTT и прекращением переписывающих систем была доказана N Дершовиц (1982)). Это означает, что для того, чтобы показать, что определенные программы завершаются, нужны сильные аксиомы (поскольку расширениям KTT нужны такие аксиомы). Результаты такого типа см., Например, А. Вейерманн, Оценки сложности для некоторых конечных форм теоремы Крускала , Журнал символических вычислений 18 (1994), 463-488.

Иддо Цамерет
источник
16

R2

В Shelah и Soifer, «Аксиома выбора и хроматическое число плоскости», показано, что если все конечные подграфы плоскости являются четырехцветными, то

  • Если принять аксиому выбора, то плоскость четырехцветная.
  • Если вы предполагаете принцип зависимого выбора и что все множества измеримы по Лебегу, то плоскость будет пяти-, шести- или семикроматической.
Деррик Стоули
источник
Разве это не более ориентировано на математику, чем на TCS?
MS Dousti
Вот почему я сказал «тангенциально» связано. Проблемы окраски ориентированы на TCS, но не на эту конкретную проблему.
Деррик Стоули
4
α
Отлично. Проверка.
Деррик Стоули
5

Некоторые работы Оливье Финкеля, похоже, связаны с вопросом - хотя и не обязательно явно о самой Аксиоме выбора - и соответствуют ответу Тимоти Чоу. Например, цитируя реферат теорем о неполноте, больших кардиналов и автоматов над конечными словами , TAMC 2017 ,

Tn:=ZFC+``There exist (at least) n inaccessible cardinals''n0
Сильвен
источник
3

[Это не прямой ответ на ваш вопрос, но он может быть наводящим и / или информативным для некоторых людей.]

Опрос Уильяма Гасарха « Р против NP» дает статистику о том, «как будет решен вопрос« Р против NP »»:

  1. 61 мысль P ≠ NP.
  2. 9 думал, P = NP.
  3. Я думал, что это независимо . Хотя ни одна конкретная система аксиом не была упомянута, я предполагаю, что они думают, что она не зависит от ZFC .
  4. 3 только что заявил, что он НЕ является независимым от примитивно-рекурсивной арифметики.
  5. Я сказал, что это будет зависеть от модели.
  6. 22 не высказал никакого мнения.

В Википедии есть интересный взгляд на независимость:

... Эти барьеры также заставили некоторых компьютерных ученых предположить, что проблема P против NP может быть независимой от стандартных систем аксиом, таких как ZFC (не может быть доказана или опровергнута внутри них). Интерпретация результата независимости может состоять в том, что либо алгоритм полиномиального времени не существует для любой NP-полной задачи, и такое доказательство не может быть построено в (например, ZFC), либо могут существовать алгоритмы полиномиального времени для NP-полных задач, но в ZFC невозможно доказать, что такие алгоритмы верны [ 1]. Однако, если можно показать, используя методы такого рода, которые, как известно, в настоящее время применимы, то, что проблема не может быть решена даже при гораздо более слабых допущениях, расширяющих аксиомы Пеано (PA) для целочисленной арифметики, тогда обязательно будет существовать почти алгоритмы полиномиального времени для каждой задачи в NP [ 2 ]. Следовательно, если считать (как это делают большинство теоретиков сложности), что не все проблемы в NP имеют эффективные алгоритмы, из этого следует, что доказательства независимости с использованием этих методов не могут быть возможными. Кроме того, этот результат подразумевает, что доказательство независимости от PA или ZFC с использованием известных в настоящее время методов не проще, чем доказательство существования эффективных алгоритмов для всех проблем в NP.

М.С. Дусти
источник
5
Другой интересный факт (также из Википедии) заключается в том, что основной (единственный?) Общий метод доказательства независимости в ZFC, принуждение, не может доказать, что P =? NP не зависит от ZFC. Это является следствием теоремы об абсолютности Шоенфилда.
Трэвис Сервис
Спасибо Тревис. Вот указатель: en.wikipedia.org/wiki/Absoluteness . См. Также cs.uwaterloo.ca/~shai/P%20vs%20NP-2.ppt и blog.computationalcomplexity.org/2009/09/… .
MS Dousti
Обратите внимание, что Билл проводит еще один опрос, который будет открыт в течение еще одного месяца: blog.computationalcomplexity.org/2011/06/…
Чарльз
@Charles: Спасибо за обновление. Я действительно хочу узнать последний консенсус сообщества.
MS Dousti
2

ZF

Gχ(H)HGG

ZF

Стелла Бидерман
источник
Хороший пример. Я думаю, что Тимоти Чоу действительно упомянул этот пример в параграфе о хроматическом числе плоскости.
Сашо Николов
@SashoNikolov Окрашиваемость графов, на мой взгляд, является проблемой TCS, даже если графы бесконечны. Проблема Хадвигера-Нельсона гораздо менее очевидна в области TCS, как отметили комментаторы, и ОП этого ответа согласилась. Напротив, я не думаю, что есть кто-то, кто посмотрит на эту теорему и
Стелла Бидерман,
Я вообще не вижу различий: Хадвигер-Нельсон тоже хочет раскрасить бесконечный геометрический граф. В любом случае, мне действительно нравятся оба примера, и я думаю, что бессмысленно пытаться провести слишком тонкое различие между TCS и другими областями математики.
Сашо Николов