В каком смысле ссылающийся?
Компилятор, который себя может скомпилировать ссылается на себя или нет?
Или программа на C, печатающая свой собственный текст?
Так это набор букв, а не алгоритм.
Не всякий набор букв является алгоритмом.
Но когда мы говорим «существует алгоритм делающий что-то» — мы имеем в виду «есть такой набор букв, являющийся алгоритмом, что если его исполнить что-то будет сделано».
Не понимаю.
Почему носитель модели — это множества?
Если мы ссылаемся просто на Сколема — то он всего лишь утверждает, что на числах можно ввести (бинарный) предикат принадлежности так, чтобы аксиомы zfc были выполнены.
И тогда «множество в модели» — это всего лишь число. Биекции между числами — это что-то странное, не так ли?
Откуда он может появиться?
У нас же простой вычислитель, у которого не может быть проблем ни с памятью (она вся инициализирована нулями и позволяет любую адресацию), ни с вычислениями (из любого состояния написано куда переходить в зависимости от того, что находится в той ячейки памяти, которую он сейчас читает).
Максимум он может никогда не остановиться, но это не fatal error.
В ZFC доказывается, что 2^N != N.
То есть в интерпретации (любой, в частности счетной) есть элементы (=множества в ZFC), которые континуальны (=равномощны 2^N).
Ну вроде не совсем.
Есть проблема с тем, что не все и не всегда проверяют, но обычно (особенно если утверждение сильное) есть статья (или серия статей), в которой это утверждение доказывается.
И «мамой клянусь, правда» — это не доказательство.
О каких я могу говорить — зависит от сигнатуры.
Да, в логике первого порядка (как и второго) поверх не более чем счетной сигнатуры выразимо не более чем счетное число предикатов.
Если рассматривать все возможные предикаты на числах — их уже не счетно. Странно не считать какой-то из предикатов «утверждением о числе».
Соображение о расширении сигнатуры (например, разрешить логику второго порядка, а не первого) — просто один из способов объяснить, откуда такие предикаты могут взяться (и почему они по-прежнему могут иметь смысл).
Да, когда мы говорим про логику второго порядка мы неявно предполагаем, что теория не более чем счетных множеств не противоречива сама по себе (как мы предполагаем непротиворечивость правил вывода для логики первого порядка или даже логики высказываний).
Можно, например, делать утверждения в более богатой сигнатуре.
В логике второго порядка можно сформулировать строго больше, чем в логике первого, например.
Все-таки не любое утверждение о натуральном числе является арифметическим (как минимум из соображений мощности — утверждений о натуральных числах континуум, а формул — лишь счетное количество)
Он не противоречивый сам по себе.
Он просто делает не то, что должен был бы делать (потому что если бы делал — то не мог бы).
Из этого и получается, что диагностика «никогда не останавливается на своем входе» не реализуема никаким алгоритмом.
В каком именно месте алгоритм оказывается некорректным?
Мы же не объявляем gcc некоректным, только потому, что он может скомпилировать сам себя?
Рассмотрим чуть более сложную диагностику — пусть эта диагностика берет на вход код программы (которая уже читает максимум одну строку на вход) и тестовый вход. А на выходе должна сказать останавливается эта программа на этом входе или нет.
Эта диагностика еще корректна, или уже нет?
Если улучшенная диагностика корректная (и есть алгоритм, который ее выполняет), то можно написать следующую программу:
прочитай вход
вызови улучшенную диагностику, интерпретируя свой вход и как алгоритм, и как его вход.
Если улучшенная диагностика сказала, что алгоритм остановится, то вызови этот алгоритм, дождись результата, припеши к результату 1.
Если улучшенная диагностика сказала, что алгоритм не остановится — напиши «алгоритм не останавливается» и закончи работать.
Этот алгоритм уже не корректен? В каком месте?
Так этот алгоритм тоже самоотрицанием не занимается.
Представьте, что это еще одна диагностика компилятора «программа, которую вы пытаетесь скомпилировать, никогда не остановится (для простоты давайте считать, что она не должна читать ничего с входа, только что-то напечатать на выход и сразу после печати остановиться)».
Между прочим, очень полезная диагностика.
Теорема о неразрешимости проблемы остановки говорит, что как бы мы эту диагностику не реализовали, есть такой код, на котором эта диагностика ошибается (либо ругается на программу, которая останавливается, либо пропускает программу, которая на самом деле зацикливается).
Компилятор, который себя может скомпилировать ссылается на себя или нет?
Или программа на C, печатающая свой собственный текст?
Не всякий набор букв является алгоритмом.
Но когда мы говорим «существует алгоритм делающий что-то» — мы имеем в виду «есть такой набор букв, являющийся алгоритмом, что если его исполнить что-то будет сделано».
Почему носитель модели — это множества?
Если мы ссылаемся просто на Сколема — то он всего лишь утверждает, что на числах можно ввести (бинарный) предикат принадлежности так, чтобы аксиомы zfc были выполнены.
И тогда «множество в модели» — это всего лишь число. Биекции между числами — это что-то странное, не так ли?
У нас же простой вычислитель, у которого не может быть проблем ни с памятью (она вся инициализирована нулями и позволяет любую адресацию), ни с вычислениями (из любого состояния написано куда переходить в зависимости от того, что находится в той ячейки памяти, которую он сейчас читает).
Максимум он может никогда не остановиться, но это не fatal error.
Компьютер, который выполняет этот код, растворится в воздухе в процессе?
То есть в интерпретации (любой, в частности счетной) есть элементы (=множества в ZFC), которые континуальны (=равномощны 2^N).
Есть проблема с тем, что не все и не всегда проверяют, но обычно (особенно если утверждение сильное) есть статья (или серия статей), в которой это утверждение доказывается.
И «мамой клянусь, правда» — это не доказательство.
Теорема Сколема об уменьшении мощности модели — она до размера сигнатуры, а не до счетного множества.
Да, конечно, у ZFC есть счетная модель, но какие-то ее элементы нужно считать континуальными и выше множествами.
Да, в логике первого порядка (как и второго) поверх не более чем счетной сигнатуры выразимо не более чем счетное число предикатов.
Если рассматривать все возможные предикаты на числах — их уже не счетно. Странно не считать какой-то из предикатов «утверждением о числе».
Соображение о расширении сигнатуры (например, разрешить логику второго порядка, а не первого) — просто один из способов объяснить, откуда такие предикаты могут взяться (и почему они по-прежнему могут иметь смысл).
Да, когда мы говорим про логику второго порядка мы неявно предполагаем, что теория не более чем счетных множеств не противоречива сама по себе (как мы предполагаем непротиворечивость правил вывода для логики первого порядка или даже логики высказываний).
В логике второго порядка можно сформулировать строго больше, чем в логике первого, например.
Но утверждение о доказуемости — является.
В чем принципиальное отличие?
Он просто делает не то, что должен был бы делать (потому что если бы делал — то не мог бы).
Из этого и получается, что диагностика «никогда не останавливается на своем входе» не реализуема никаким алгоритмом.
Мы же не объявляем gcc некоректным, только потому, что он может скомпилировать сам себя?
Рассмотрим чуть более сложную диагностику — пусть эта диагностика берет на вход код программы (которая уже читает максимум одну строку на вход) и тестовый вход. А на выходе должна сказать останавливается эта программа на этом входе или нет.
Эта диагностика еще корректна, или уже нет?
Если улучшенная диагностика корректная (и есть алгоритм, который ее выполняет), то можно написать следующую программу:
прочитай вход
вызови улучшенную диагностику, интерпретируя свой вход и как алгоритм, и как его вход.
Если улучшенная диагностика сказала, что алгоритм остановится, то вызови этот алгоритм, дождись результата, припеши к результату 1.
Если улучшенная диагностика сказала, что алгоритм не остановится — напиши «алгоритм не останавливается» и закончи работать.
Этот алгоритм уже не корректен? В каком месте?
Представьте, что это еще одна диагностика компилятора «программа, которую вы пытаетесь скомпилировать, никогда не остановится (для простоты давайте считать, что она не должна читать ничего с входа, только что-то напечатать на выход и сразу после печати остановиться)».
Между прочим, очень полезная диагностика.
Теорема о неразрешимости проблемы остановки говорит, что как бы мы эту диагностику не реализовали, есть такой код, на котором эта диагностика ошибается (либо ругается на программу, которая останавливается, либо пропускает программу, которая на самом деле зацикливается).
Или, даже, скомпилировать gcc с помощью gcc.
Что именно не так?