Вычислительные последствия (недоказуемой) теоремы Фридмана о неподвижной точке верхнего сдвига?

Харви Фридман показал, что есть точный результат с фиксированной точкой, который нельзя доказать в ZFC (обычная теория множеств Цермело-Франкеля с Аксиомой Выбора). Многие современные логики построены на операторах с фиксированной запятой, поэтому мне было интересно: известны ли какие-либо последствия теоремы о фиксированной точке верхнего сдвига для теоретической информатики?

Недоказуемая теорема о неподвижной точке с верхним сдвигом
Для всех некоторые содержат .$R \in \text{SDOI}(Q^k,Q^k)$$A = \text{cube}(A,0) \setminus R[A]$$\text{us}(A)$

Теорема USFP, по-видимому, является утверждением , поэтому она может быть «достаточно близка» к вычислимости (такой как проверка неизоморфизма автоматных структур), чтобы повлиять на теоретическую информатику.$\Pi^1_1$

Для полноты приведем определения из выступления Фридмана в MIT за ноябрь 2009 года (см. Также черновик книги «Теория булевых отношений» ).

$Q$ - множество рациональных чисел. являются порядка эквивалентны , если всякий раз , когда , то . При , то верхний сдвиг по , обозначаемому , получаются путем добавления 1 к каждому неотрицательной координате . Отношение является порядок инвариантным , если для любого порядка инвариантной эквивалентной справедливо , что . Отношение$x, y \in Q^k$$1 \le i,j \le k$$x_i \lt x_j \Leftrightarrow y_i \lt y_j$$x \in Q^k$$x$$\text{us}(x)$$x$$A \subseteq Q^k$ x ∈ A ⇔ y ∈ A R ⊆ Q k × Q $x,y \in Q^k$$x \in A \Leftrightarrow y \in A$$R \subseteq Q^k \times Q^k$является инвариантным по порядку, если является инвариантным по порядку как подмножество , и строго доминирует, если для всех всякий раз, когда тогда . Далее, если A является подмножеством Q ^ k, то R [A] обозначает \ {y | \ существует x \ в AR (x, y) \} , верхний сдвиг A равен \ text {us} (A) = \ {\ text {us} (x) | x \ in A \} , а \ text {cube} (A, 0) обозначает наименьшее B ^ k такое, что 0 \ in B и A содержится в B ^ k . ПозволятьQ 2 $R$$Q^{2k}$$x,y \in Q^k$$R(x,y)$A Q k R [ A ] { y | ∃ x ∈ A R ( x , y ) } A us ( A ) = { us ( x ) | x ∈ A } куб $\max(x) \lt \max(y)$$A$$Q^k$$R[A]$$\{ y | \exists x \in A R(x,y)\}$$A$$\text{us}(A) = \{\text{us}(x) | x \in A\}$B k 0 ∈ B A B k SDOI ( Q k , Q k$\text{cube}(A,0)$$B^k$$0 \in B$$A$$B^k$$\text{SDOI}(Q^k,Q^k)$ обозначает множество всех инвариантных отношений строго доминирующего порядка $R \subseteq Q^k \times Q^k$ .

Редактировать: Как отмечает Dömötör Pálvölgyi в комментариях, взятие и в качестве обычного упорядочения для рациональных чисел, похоже, приводит к контрпримеру. Во-первых, множество не может быть пустым, так как тогда является пустым, и тогда должно содержать 0 по условию куба, противоречие. Если непустое множество имеет инфимум, то оно не может содержать каких-либо рациональных чисел, больших этого, поэтому оно должно быть одноэлементным, что противоречит условию верхнего сдвига. Если, с другой стороны, не имеет инфимума, то поэтому должно быть пустым, противоречие. R A R [ A ] A A A R [ A ] = Q $k=1$$R$$A$$R[A]$$A$$A$$A$$R[A] = Q$$A$Любые комментарии о том, есть ли какие-то скрытые неочевидные проблемы определения, такие как, возможно, неявная нестандартная модель рациональных чисел?

Дальнейшее редактирование: приведенный выше аргумент является примерно правильным, но неверным в применении верхнего сдвига. Этот оператор применяется только к неотрицательным координатам, поэтому установка в качестве любого отрицательного одноэлементного набора дает желаемую фиксированную точку. Другими словами, если то является решением, и других решений нет.m < 0 A = { м $A$$m < 0$$A = \{m\}$

Я не знаю каких-либо последствий этой конкретной теоремы, но доказательства нормализации лямбда-исчислений, таких как исчисление индуктивных конструкций, основаны на больших кардинальных аксиомах - даже если набор лямбда-терминов исчисляется настолько, насколько вы могли бы захотеть.

Я думаю, что лучший способ понять вычислительную значимость теоретико-множественных аксиом, утверждающих существование больших кардиналов, - это думать о теории множеств как о способе формулировки теории графов. То есть модель набора представляет собой набор элементов, снабженных бинарным отношением, используемым для интерпретации членства. Затем аксиомы теории множеств сообщают вам свойства отношения принадлежности, включая то, как вы можете формировать новые множества из старых. В частности, аксиома основания означает, что отношение членства является обоснованным (то есть оно не имеет бесконечных нисходящих цепочек). Эта обоснованность в свою очередь означает, что если вы можете выровнять состояния выполнения программы с транзитивным членством элементов набора, то у вас есть доказательство завершения.

Таким образом, утверждение о том, что «большой» набор существует, имеет вычислительную выгоду как утверждение, что определенный класс циклов в общем рекурсивном языке программирования завершается. Эта интерпретация работает равномерно, начиная с простой старой аксиомы бесконечности (которая оправдывает итерацию натуральных чисел) и заканчивая большими кардинальными аксиомами.

Являются ли эти аксиомы верно ? Хорошо, если аксиома ложна, вы можете найти программу в одном из этих классов, которая не заканчивается. Но если это правда, мы никогда не будем уверены, благодаря теореме Халтинга. Все, начиная с индукции натуральных чисел, является вопросом научной индукции, которая всегда может быть фальсифицирована экспериментом - Эдвард Нельсон, как известно, надеялся доказать, что возведение в степень является частичной функцией!