На языке «проблемы остановки» утверждение должно звучать так: не существует алгоритма, который берет другой алгоритм (то есть преобразователь из строки в строку) и определяет остановится этот алгоритм на себе самом или нет.
Если бы такой алгоритм существовал, то можно было бы построить диагональную функцию: она на входе f смотрит на то, останавливается ли f(f), если не останавливается — возвращает 0, если останавливается — возвращает f(f) + 1.
Чуть подробнее вот тут: habr.com/en/post/512518/#comment_21901770
Там же формальная грамматика, она, в некотором смысле, даже проще чисел.
Эм, нет, любая теория, в которой можно выразить Х, как минимум не слабее Х.
Любая теория, в которой можно доказать Х, не слабее Х.
Но сформулировать, конечно, можно в более слабой.
Например, после того как мы вложили логику первого порядка в числа, можно сформулировать утверждение «2 + 2 = 5» (которое очень сильное).
Вся наша метатеория — она про то, «что такое доказательство» (с синтаксической точки зрения). Строки и числа можно сопоставить не изучая вопроса «какая аксиоматика поверх чисел».
Единственное тонкое место здесь — когда мы говорим, что «если теория непротиворечива, то нельзя получить доказательств ложных утверждений в этой теории». Но это утверждение — оно про корректность наших правил вывода, они опять не зависят от кодирования. Да, если мы в метатеорию добавим некорректное правило вывода — все сломается.
Так снаружи она тоже безопасная — все уже смыло и унесло ветром.
Они продували область между внешней обшивкой и капсулой (у них там же служебный отсек). И вот в этой области и было повышенное содержание одного и компонентов топлива.
Так основной результат заключается в том, что доказуемость утверждения можно сформулировать в терминах самой арифметики, не выходя за ее примеры.
Один из частный случаев теоремы Геделя: есть диафантово уравнение (т.е. просто многочлен с целыми коэффициентами, даже не очень большой, можно явно написать все, кроме одной константы.), у которого нету корней (если арифметика Пеано непротиворечива), но доказать это (в рамках арифметики Пеано) невозможно.
Мы же в интернете. Все утверждения — это просто числа (соответствующие utf8-строкам). В каком месте тут софистика?
Если мы запрещаем (без дополнительной проверки) синтаксический вывод — нужно границы явно провести, где синтаксически еще можно, а где уже нельзя.
И если мы добавляем семантическую проверку, то смысл синтаксического вывода во многом теряется — если есть семантическая проверка, то и истинность можно уж заодно проверить.
Тогда у нас неправильный синтаксис, и его нужно ослаблять. Например, пойти по пути конструктивизма или, даже, исключения правила исключенного третьего.
Если нет корректности (т.е. синтаксически из верного утверждения можно сделать бессмысленное или неверное, делая только синтаксически-эквивалентные замены), то непонятно как вообще про какие-то доказательства можно говорить вообще.
Не совсем согласен. Стандартная интерпретация натуральных чисел — это все-таки что-то достаточно понятное (и существующее, если ZFC непротиворечиво).
Хороший пример — это уравнения Матиясевича. Есть конкретное диафантово уравнение, у которого нету корней, но в стандартной арифметике Пеано этого доказать нельзя.
А почему собственно?
Если оно некорректно, то оно не является саморефлексевным (потому что утверждает что-то про множество корректных утверждений, в которое не входит).
А значит мы должны считать его корректным.
Вроде, у нас было два ограничения на корректность: «быть не саморефлексевным и касаться только корректных утверждений». Что я упускаю?
Я, вроде, нигде не пользовался явной формой анализатора.
Мне всего лишь было важно алгоритмически определить останавливается A(A) или нет.
Для Вашего анализатора алгоритм для f будет выглядеть вот так: f(A):
Если Анализатор(А,А) = 1 { вернуть 1 }
Иначе { вернуть А(А) + 1 }
На вход поданы два аргумента — код программы и строка, на которой нужно предсказать остановку.
Какой из входных параметров некорректен?
Если на вход подано что?
Если бы такой алгоритм существовал, то можно было бы построить диагональную функцию: она на входе f смотрит на то, останавливается ли f(f), если не останавливается — возвращает 0, если останавливается — возвращает f(f) + 1.
Чуть подробнее вот тут: habr.com/en/post/512518/#comment_21901770
Любая теория, в которой можно доказать Х, не слабее Х.
Но сформулировать, конечно, можно в более слабой.
Например, после того как мы вложили логику первого порядка в числа, можно сформулировать утверждение «2 + 2 = 5» (которое очень сильное).
Вся наша метатеория — она про то, «что такое доказательство» (с синтаксической точки зрения). Строки и числа можно сопоставить не изучая вопроса «какая аксиоматика поверх чисел».
Единственное тонкое место здесь — когда мы говорим, что «если теория непротиворечива, то нельзя получить доказательств ложных утверждений в этой теории». Но это утверждение — оно про корректность наших правил вывода, они опять не зависят от кодирования. Да, если мы в метатеорию добавим некорректное правило вывода — все сломается.
Они продували область между внешней обшивкой и капсулой (у них там же служебный отсек). И вот в этой области и было повышенное содержание одного и компонентов топлива.
Что вкладывается в «корректность» отношения?
Там же формальная грамматика, она, в некотором смысле, даже проще чисел.
Один из частный случаев теоремы Геделя: есть диафантово уравнение (т.е. просто многочлен с целыми коэффициентами, даже не очень большой, можно явно написать все, кроме одной константы.), у которого нету корней (если арифметика Пеано непротиворечива), но доказать это (в рамках арифметики Пеано) невозможно.
Если мы запрещаем (без дополнительной проверки) синтаксический вывод — нужно границы явно провести, где синтаксически еще можно, а где уже нельзя.
И если мы добавляем семантическую проверку, то смысл синтаксического вывода во многом теряется — если есть семантическая проверка, то и истинность можно уж заодно проверить.
То есть мы запрещаем (фактически) все утверждения об утверждениях, это, конечно возможный способ решить проблему с самореферентностью.
Но тогда нужно запретить и утверждения про числа, например, — мы можем заменить утверждение его utf8 записью, которая является числом.
Если нет корректности (т.е. синтаксически из верного утверждения можно сделать бессмысленное или неверное, делая только синтаксически-эквивалентные замены), то непонятно как вообще про какие-то доказательства можно говорить вообще.
Умножение на любое конкретное число в арифметики Пресбургера есть, нет умножения как операции двух аргументов.
Тогда у нас есть беда: эти два утверждения эквивалентны (просто потому что «Все А есть не Б» и «Все Б есть не А» — это синтаксически одно и то же).
Мы же пока просто пытаемся понять является ли оно корректным, а не вывести из этого что-то.
Еще раз: Как выглядит ограничение на корректные утверждения?
Еще одна точка — «саморефлексивные утверждение некорректны» само по себе является корректным?
Хороший пример — это уравнения Матиясевича. Есть конкретное диафантово уравнение, у которого нету корней, но в стандартной арифметике Пеано этого доказать нельзя.
Если оно некорректно, то оно не является саморефлексевным (потому что утверждает что-то про множество корректных утверждений, в которое не входит).
А значит мы должны считать его корректным.
Вроде, у нас было два ограничения на корректность: «быть не саморефлексевным и касаться только корректных утверждений». Что я упускаю?
Например, является ли корректным утверждение «среди корректных утверждений есть истинное»?
Мне всего лишь было важно алгоритмически определить останавливается A(A) или нет.
Для Вашего анализатора алгоритм для f будет выглядеть вот так:
f(A):Если Анализатор(А,А) = 1 { вернуть 1 }
Иначе { вернуть А(А) + 1 }