Теорема Лёба

[маткиб]

epros в сообщении #173087 писал(а):

В теории есть аксиомы, но не их номера. Формула, определяющая соответствие между аксиомами теории (высказываниями в её синтаксисе) и их номерами, определена в метатеории. И я не понимаю как эту формулу можно записать в синтаксисе теории. А если она не записана в синтаксисе теории, то мне непонятно что значит "определить номер этой формулы".

Я совершенно не понимаю, зачем всё это делать. Зачем вообще расширять синтаксис? Языка 0+*S= вполне достаточно, чтобы формулировать утверждения о любых алгоритмах (т.е. такие формулы, которые по нашему личному мнению будут утверждениями об алгоритмах).

Мы хотим показать, что существует алгоритм, который по номеру n алгоритма, перечисляющего аксиомы (точнее, их номера) теории в языке 0+*S=, вычисляет номер алгоритма, перечисляющего аксиомы (номера аксиом) мета-доказуемости. В чём здесь проблема?

Если есть число n, то не составит труда на основе Гёделевской нумерации по любой формуле $\Phi$ построить формулу $(T\vdash\Phi)\rightarrow\Phi$, т.е. есть алгоритм, который по n и номеру формулы $\Phi$ строит номер формулы $(T\vdash\Phi)\rightarrow\Phi$. На основе этого алгоритма строится и алгоритм, вычисляющий $F(n)$.

Добавлено спустя 2 минуты 58 секунд:

P.S. Конечно же, сначала нужно зафиксировать некоторую нумерацию строк языка 0+*S=

[epros]

маткиб писал(а):

Я совершенно не понимаю, зачем всё это делать. Зачем вообще расширять синтаксис? Языка 0+*S= вполне достаточно, чтобы формулировать утверждения о любых алгоритмах (т.е. такие формулы, которые по нашему личному мнению будут утверждениями об алгоритмах).

Мы хотим показать, что существует алгоритм, который по номеру n алгоритма, перечисляющего аксиомы (точнее, их номера) теории в языке 0+*S=, вычисляет номер алгоритма, перечисляющего аксиомы (номера аксиом) мета-доказуемости. В чём здесь проблема?

Если есть число n, то не составит труда на основе Гёделевской нумерации по любой формуле $\Phi$ построить формулу $(T\vdash\Phi)\rightarrow\Phi$, т.е. есть алгоритм, который по n и номеру формулы $\Phi$ строит номер формулы $(T\vdash\Phi)\rightarrow\Phi$. На основе этого алгоритма строится и алгоритм, вычисляющий $F(n)$.

Добавлено спустя 2 минуты 58 секунд:

P.S. Конечно же, сначала нужно зафиксировать некоторую нумерацию строк языка 0+*S=

Вот именно, что сначала нужно зафиксировать нумерацию строк языка теории. Попробую объяснить свои сомнения ещё раз: Как я уже сказал, нетривиально уже само утверждение, что существует некий "номер n алгоритма, перечисляющего аксиомы теории в языке 0+*S=".

Безусловно, алгоритм (формулу), нумерующий все акиомы теории, можно построить. Но этот алгоритм не может быть записан формулой в языке теории! А это значит, что способ нумерации, определённый для строк языка теории, для определения номера этого алгоритма не подходит.

Если Вы не согласны с утверждением, что формула, нумерующая все аксиомы теории, не может быть формулой в языке теории, то я хочу заметить, что это довольно легко доказывается. Итак, будем исходить из того, что у нас пронумерованы по крайней мере все аксиомы индукции (они-то уж всегда есть в теории, содержащей арифметику). Это означает то же самое, что у нас пронумерованы все формулы теории с одной свободной переменной. "Нумерующей формулой" будем называть алгоритм $\xi(k)$, который по предъявлению ему в качестве аргумента номера $k$ генерирует строку $\varphi_k(n)$, которая согласно синтаксису теории является формулой с одной свобоной переменной $n$. Предположим, что алгоритм $\xi(k)$ может быть записан формулой в языке теории. Добавим к нему две операции: 1) Поставить пред формулой знак отрицания и 2) подставить в качестве свободной переменной $n$ аргумент алгоритма $k$. В итоге получим некую формулу $\psi(k)$ с одной свободной переменной. Поскольку все формулы с одной свободной переменной у нас пронумерованы, то существует некий номер $m$ такой, что $\psi(k) \equiv \varphi_m(k)$, т.е. $\neg \varphi_k(k) \equiv \varphi_m(k)$, что при подставновке $k = m$ приводит к противоречию. Итак, алгоритм $\xi(k)$ не может быть записан формулой в языке теории.

[маткиб]

epros писал(а):

Если Вы не согласны с утверждением, что формула, нумерующая все аксиомы теории, не может быть формулой в языке теории, то я хочу заметить, что это довольно легко доказывается. Итак, будем исходить из того, что у нас пронумерованы по крайней мере все аксиомы индукции (они-то уж всегда есть в теории, содержащей арифметику). Это означает то же самое, что у нас пронумерованы все формулы теории с одной свободной переменной. "Нумерующей формулой" будем называть алгоритм $\xi(k)$, который по предъявлению ему в качестве аргумента номера $k$ генерирует строку $\varphi_k(n)$, которая согласно синтаксису теории является формулой с одной свобоной переменной $n$. Предположим, что алгоритм $\xi(k)$ может быть записан формулой в языке теории. Добавим к нему две операции: 1) Поставить пред формулой знак отрицания и 2) подставить в качестве свободной переменной $n$ аргумент алгоритма $k$. В итоге получим некую формулу $\psi(k)$ с одной свободной переменной. Поскольку все формулы с одной свободной переменной у нас пронумерованы, то существует некий номер $m$ такой, что $\psi(k) \equiv \varphi_m(k)$, т.е. $\neg \varphi_k(k) \equiv \varphi_m(k)$, что при подставновке $k = m$ приводит к противоречию. Итак, алгоритм $\xi(k)$ не может быть записан формулой в языке теории.

Что у Вас означает $\Phi(k)$ для формулы $\Phi$?

Если это истинность $\Phi(k)$, то Вы только что доказали теорему Тарского о невыразимости истинности: не существует формулы $\Phi(x,y)$, которая была бы эквивалентна истинности формулы с номером $x$ (с одной свободной переменной) на значении $y$.

Если это доказуемость, то Вы доказали некоторый ослабленный вариант второй теоремы Гёделя: ни для какой формулы нельзя доказать, что она не доказуема (т.е. для недоказуемых формул не получится построить отрицание).

А записать формулой $\Phi(x,y)\equiv(y\text{ есть номер }x-\text{й формулы теории})$ - это не проблема.

[epros]

маткиб писал(а):

Что у Вас означает $\Phi(k)$ для формулы $\Phi$?

Я не понимаю Вашего вопроса. У меня не было такого обозначения.

маткиб писал(а):

Если это истинность $\Phi(k)$, то Вы только что доказали теорему Тарского о невыразимости истинности: не существует формулы $\Phi(x,y)$, которая была бы эквивалентна истинности формулы с номером $x$ (с одной свободной переменной) на значении $y$.

Собственно, я и ориентировался на теорему Тарского. Только меня здесь интересует не "выразимость истинности", ибо я не очень понимаю, что это значит, а формула, нумерующая формулы теории.

маткиб писал(а):

А записать формулой $\Phi(x,y)\equiv(y\text{ есть номер }x-\text{й формулы теории})$ - это не проблема.

Я не понял, что означает фраза: "$y\text{ есть номер }x-\text{й формулы теории}$".

[маткиб]

epros писал(а):

маткиб писал(а):

Что у Вас означает $\Phi(k)$ для формулы $\Phi$?

Я не понимаю Вашего вопроса. У меня не было такого обозначения.

У Вас используется много подобных обозначений: $\xi(k)$, $\varphi_k(n)$, $\psi(k)$ и т.д. Я не понимаю, что они значат. Хочется думать, что $\Phi(k)$ - это результат подстановки числа $k$ в формулу $\Phi$ (т.е. новая формула), но меня приводит в ступор вот это:
$\neg \varphi_k(k) \equiv \varphi_m(k)$.
Что это значит? $T\vdash\neg \varphi_k(k) \equiv \varphi_m(k)$? Или "$\neg \varphi_k(k) \equiv \varphi_m(k)$ истинно"? Или что-то ещё? Сказать, что это тоже просто формула, мы не имеем права, потому что Вы делаете некоторые рассуждения на основе того, что этой формуле соответствует некоторое конкретное булево значение.

Добавка: и надо не забывать, что Вы в своём доказательстве оперируете с номерами формул, а не формулами, поэтому тем более приобретает смысл вопрос о том, каким образом булево значение сопоставляется номеру.

epros писал(а):

Собственно, я и ориентировался на теорему Тарского. Только меня здесь интересует не "выразимость истинности", ибо я не очень понимаю, что это значит, а формула, нумерующая формулы теории.

Вот для невыразимости истинности Ваше доказательство работает, а для "формул, нумерующих формулы теории" - нет.

epros писал(а):

маткиб писал(а):

А записать формулой $\Phi(x,y)\equiv(y\text{ есть номер }x-\text{й формулы теории})$ - это не проблема.

Я не понял, что означает фраза: "$y\text{ есть номер }x-\text{й формулы теории}$".

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

Кстати, а что такое "формула, нумерующая формулы теории"? Раньше этот вопрос не задавал, потому что все мои попытки домыслить это определение приводят к тому, что такая формула существует.

[epros]

маткиб писал(а):

У Вас используется много подобных обозначений: $\xi(k)$, $\varphi_k(n)$, $\psi(k)$ и т.д. Я не понимаю, что они значат.

Все разные. $\xi$ - это обозначение алгоритма, который берёт в качестве аргумента число и генерирует строку. $\varphi_k(n)$ - это обозначение результата выполнения этого алгоритма - строки, которая в синтаксисе теории соответствует некой формуле с одной свободной переменной $n$. $\psi(k)$ - это обозначение формулы, которая получается подстановкой в формулу $\varphi_k(n)$ вместо свободной переменной $n$ аргумента алгоритма $k$ и добавлением символа отрицания перед ней.

Обо всём этом выше было сказано.

маткиб писал(а):

но меня приводит в ступор вот это:
$\neg \varphi_k(k) \equiv \varphi_m(k)$.
Что это значит? $T\vdash\neg \varphi_k(k) \equiv \varphi_m(k)$? Или "$\neg \varphi_k(k) \equiv \varphi_m(k)$ истинно"? Или что-то ещё?

Это означает буквальное (посимвольное) совпадение двух формул, каждая с одной свободной переменной - $k$. Если я применил неадекватное обозначение, то извиняюсь.

маткиб писал(а):

Сказать, что это тоже просто формула, мы не имеем права, потому что Вы делаете некоторые рассуждения на основе того, что этой формуле соответствует некоторое конкретное булево значение.

Вы о чём здесь? Дальнейший вывод заключается только в том, что некоторое высказывание $\varphi_m(m)$ посимвольно совпадает тем же высказыванием, перед которым поставлен символ отрицания (что противоречиво).

маткиб писал(а):

Добавка: и надо не забывать, что Вы в своём доказательстве оперируете с номерами формул, а не формулами, поэтому тем более приобретает смысл вопрос о том, каким образом булево значение сопоставляется номеру.

Булево значение меня не интересует. А номер формулы - это аргумент нумерующего алгоритма $\xi$, он соответствует собственно формуле - результату выполенения этого алгоритма.

маткиб писал(а):

Вот для невыразимости истинности Ваше доказательство работает, а для "формул, нумерующих формулы теории" - нет.

Вашу формулировку: про формулу $\Phi(x,y)$, которая "эквивалентна истинности формулы с номером $x$ (с одной свободной переменной) на значении $y$". тоже можно интерпретировать как "нумерующую формулу". Например, подстановкой $x = 17$ мы получаем формулу с одной свободной переменной $y$, которая имеет номер 17. Для Вас с Тарским, возможно, важна логическая "эквивалентность" получившейся формулы 17-той формуле теории, а я требую большего - не только "эквивалентности", а буквального (посимвольного) совпадения.

Так что теоремой Тарского доказано в том числе и то, что такой "нумерующей формулы" в языке теории не существует.

маткиб писал(а):

Кстати, а что такое "формула, нумерующая формулы теории"? Раньше этот вопрос не задавал, потому что все мои попытки домыслить это определение приводят к тому, что такая формула существует.

Надеюсь, что приведённых выше объяснений достаточно?

[маткиб]

epros писал(а):

маткиб писал(а):

но меня приводит в ступор вот это:
$\neg \varphi_k(k) \equiv \varphi_m(k)$.
Что это значит? $T\vdash\neg \varphi_k(k) \equiv \varphi_m(k)$? Или "$\neg \varphi_k(k) \equiv \varphi_m(k)$ истинно"? Или что-то ещё?

Это означает буквальное (посимвольное) совпадение двух формул, каждая с одной свободной переменной - $k$. Если я применил неадекватное обозначение, то извиняюсь.

Такой подход ничего интересного не даёт, одни банальности.

epros писал(а):

Если Вы не согласны с утверждением, что формула, нумерующая все аксиомы теории, не может быть формулой в языке теории, то я хочу заметить, что это довольно легко доказывается. Итак, будем исходить из того, что у нас пронумерованы по крайней мере все аксиомы индукции (они-то уж всегда есть в теории, содержащей арифметику). Это означает то же самое, что у нас пронумерованы все формулы теории с одной свободной переменной. "Нумерующей формулой" будем называть алгоритм $\xi(k)$, который по предъявлению ему в качестве аргумента номера $k$ генерирует строку $\varphi_k(n)$, которая согласно синтаксису теории является формулой с одной свобоной переменной $n$. Предположим, что алгоритм $\xi(k)$ может быть записан формулой в языке теории. Добавим к нему две операции: 1) Поставить пред формулой знак отрицания и 2) подставить в качестве свободной переменной $n$ аргумент алгоритма $k$. В итоге получим некую формулу $\psi(k)$ с одной свободной переменной. Поскольку все формулы с одной свободной переменной у нас пронумерованы, то существует некий номер $m$ такой, что $\psi(k) \equiv \varphi_m(k)$, т.е. $\neg \varphi_k(k) \equiv \varphi_m(k)$, что при подставновке $k = m$ приводит к противоречию. Итак, алгоритм $\xi(k)$ не может быть записан формулой в языке теории.

Если я всё правильно понял (хотя я сомневаюсь в этом), то ошибка в выделенном красным цветом. $\psi(k)$ - это функция, отображающая множество натуральных чисел в множество формул, а никак не формула с одной свободной переменной. Было бы очень наивно полагать, что эта функция сводится к подстановке константы $k$ в фиксированную формулу-шаблон.

epros писал(а):

Вашу формулировку: про формулу $\Phi(x,y)$, которая "эквивалентна истинности формулы с номером $x$ (с одной свободной переменной) на значении $y$". тоже можно интерпретировать как "нумерующую формулу". Например, подстановкой $x = 17$ мы получаем формулу с одной свободной переменной $y$, которая имеет номер 17. Для Вас с Тарским, возможно, важна логическая "эквивалентность" получившейся формулы 17-той формуле теории, а я требую большего - не только "эквивалентности", а буквального (посимвольного) совпадения.

Утверждение в такой формулировке, конечно, верно, но это обыкновеннейшая банальность. Ясно, что, например, если формула $\Phi(x,y)$ имеет 19 символов логических операций, то никакой подстановкой константы вместо $x$ из неё не получить формулу, в которой 24 символа логических операций (или, например, формулу, которая попросту короче $\Phi$).

epros писал(а):

маткиб писал(а):

Кстати, а что такое "формула, нумерующая формулы теории"? Раньше этот вопрос не задавал, потому что все мои попытки домыслить это определение приводят к тому, что такая формула существует.

Надеюсь, что приведённых выше объяснений достаточно?

Если я всё понял правильно и правильно указал на место с ошибкой, то достаточно. Если нет, то этот вопрос снова подвисает.

[epros]

маткиб писал(а):

epros писал(а):

Если Вы не согласны с утверждением, что формула, нумерующая все аксиомы теории, не может быть формулой в языке теории, то я хочу заметить, что это довольно легко доказывается. Итак, будем исходить из того, что у нас пронумерованы по крайней мере все аксиомы индукции (они-то уж всегда есть в теории, содержащей арифметику). Это означает то же самое, что у нас пронумерованы все формулы теории с одной свободной переменной. "Нумерующей формулой" будем называть алгоритм $\xi(k)$, который по предъявлению ему в качестве аргумента номера $k$ генерирует строку $\varphi_k(n)$, которая согласно синтаксису теории является формулой с одной свобоной переменной $n$. Предположим, что алгоритм $\xi(k)$ может быть записан формулой в языке теории. Добавим к нему две операции: 1) Поставить пред формулой знак отрицания и 2) подставить в качестве свободной переменной $n$ аргумент алгоритма $k$. В итоге получим некую формулу $\psi(k)$ с одной свободной переменной. Поскольку все формулы с одной свободной переменной у нас пронумерованы, то существует некий номер $m$ такой, что $\psi(k) \equiv \varphi_m(k)$, т.е. $\neg \varphi_k(k) \equiv \varphi_m(k)$, что при подставновке $k = m$ приводит к противоречию. Итак, алгоритм $\xi(k)$ не может быть записан формулой в языке теории.

Если я всё правильно понял (хотя я сомневаюсь в этом), то ошибка в выделенном красным цветом. $\psi(k)$ - это функция, отображающая множество натуральных чисел в множество формул, а никак не формула с одной свободной переменной. Было бы очень наивно полагать, что эта функция сводится к подстановке константы $k$ в фиксированную формулу-шаблон.

Наивно или не наивно, а именно таково опровергаемое предположение (выше я слово "предположим" даже выделил жирным шрифтом). То, что $\psi(k)$ - формула теории, является непосредственным следствием этого предположения: Если "нумерующий алгоритм" $\xi(k)$ записывается формулой теории, то в результате добавления к этой формуле символа отрицания и подстановки в неё переменной мы тоже получим формулу теории.

маткиб писал(а):

Утверждение в такой формулировке, конечно, верно, но это обыкновеннейшая банальность. Ясно, что, например, если формула $\Phi(x,y)$ имеет 19 символов логических операций, то никакой подстановкой константы вместо $x$ из неё не получить формулу, в которой 24 символа логических операций (или, например, формулу, которая попросту короче $\Phi$).

Ну и что? Мне тоже и без привлечения теоремы Тарского очевидно, что алгоритм, нумерующий аксиомы теории, невозможно записать формулой теории. Но ведь это Вы взялись определять номера алгоритмов, нумерующих аксиомы. А я не знаю как можно определить номер алгоритма, если он не записывается формулой теории.

[маткиб]

Тогда повторяю вопрос: что значит "формула нумерует формулы теории"?

А то, как мне кажется, Вы приписываете такой формуле какие-то магические свойства, из которых сразу вытекает, что такой формулы не существует.

[maxal]

Немножно не в тему, но я знаю другого Лёба, которого зовут Питер. В честь него названы меры Лёба и пространства Лёба. Мои бакалаврская и магистерская диссертации оперировали этими понятиями, и основные результаты из них потом вошли в эту статью.
Поэтому когда я увидел тему "теорема Лёба", я подумал было, что речь идет о нестандартном анализе, а оказалось, что о теореме Мартина Лёба в логике.

[epros]

маткиб писал(а):

Тогда повторяю вопрос: что значит "формула нумерует формулы теории"?

А то, как мне кажется, Вы приписываете такой формуле какие-то магические свойства, из которых сразу вытекает, что такой формулы не существует.

Хм. Вообще-то я ожидал, что это Вы поясните, откуда берутся "номера $n$ алгоритмов, перечисляющих все аксиомы". Я вроде бы понимаю что такое "алгоритм" и кажется могу понять как алгоритм может "перечислять аксиомы". Я также понимаю, что алгоритм определяется некой конечной формулой (если хотите - кодом алгоритма). Но я не понимаю, каким образом нумеруются алгоритмы! Гедель, насколько я помню, определил способ нумерации для всех объектов теории, но этот способ не подходит, поскольку такой алгоритм не является объектом теории - не записывается её формулой.

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

[маткиб]

epros писал(а):

Хм. Вообще-то я ожидал, что это Вы поясните, откуда берутся "номера $n$ алгоритмов, перечисляющих все аксиомы".

У меня как раз всё просто. Алгоритм - это машина Тьюринга ( ru.wikipedia.org/wiki/Машина_Тьюринга ). МТ задаётся своей таблицей. Таблицу можно записать как строку символов некоторого фиксированного алфавита. Для строк символов можно взять обычную нумерацию. Тогда алгоритм имеет номер.

epros писал(а):

Я вроде бы понимаю что такое "алгоритм" и кажется могу понять как алгоритм может "перечислять аксиомы".

Если алгоритм существует, то у него есть номер.

epros писал(а):

Я также понимаю, что алгоритм определяется некой конечной формулой (если хотите - кодом алгоритма).

А я понимаю только кодом, а формулой - не понимаю.

epros писал(а):

Но я не понимаю, каким образом нумеруются алгоритмы! Гедель, насколько я помню, определил способ нумерации для всех объектов теории, но этот способ не подходит, поскольку такой алгоритм не является объектом теории - не записывается её формулой.

Я не понимаю, что означает фраза "алгоритм является объектом теории". Алгоритм имеет номер и всё! Лично мне больше ничего не надо. Является ли он там или не является объектом теории - да по барабану.

epros писал(а):

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

А я не понял этого Вашего "общего вопроса", потому что Вы не пояснили, что сия фраза означает. Лично мне для определения моей мета($\omega$)-доказуемости совершенно не нужно каким-то образом "записывать алгоритм, перечисляющий аксиомы, формулой в языке теории". Мне важно, что:
1) алгоритм существует (=> имеет номер);
2) существует алгоритм, который по номеру этого алгоритма вычисляет номер следующего алгоритма (т.е. того, который перечисляет аксиомы мета(n+1)-доказуемости);
3) существует алгоритм, который перечисляет все аксиомы мета(n)-доказуемостей для всех n (он тривиально строится из алгоритма в пункте 2);
4) для любой формулы $\Phi$ языка "0S+*=" я могу построить формулу этого же языка, которая будет по моему личному мнению утверждать, что $(\exists n)(\Phi\text{ мета(n)-доказуема})$ (эта формула строится на основе номера алгоритма из пункта 3 и стандартных конструкций, идущих от Гёделя).

epros писал(а):

С моей точки зрения "перечислить аксиомы" - это значит определить соответствие между аксиомами и их номерами. Может быть я неправильно Вас понял?

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

[epros]

маткиб писал(а):

У меня как раз всё просто. Алгоритм - это машина Тьюринга ( ru.wikipedia.org/wiki/Машина_Тьюринга ). МТ задаётся своей таблицей. Таблицу можно записать как строку символов некоторого фиксированного алфавита. Для строк символов можно взять обычную нумерацию. Тогда алгоритм имеет номер.

Разумеется код алгоритма можно записать строкой символов. Это и есть "формула", определяющая алгоритм. Вот только определена она не в языке той теории, аксиомы которой мы нумеруем. Возьмите в качестве примера нормальный алгоритм Маркова. Чтобы определить его код, нужны два служебных символа, которых нет в том алфавите, к словам которого будет применяться алгоритм.

маткиб писал(а):

Если алгоритм существует, то у него есть номер.

Это что же, очередная, в лучших традициях "классической" математики взятая с потолка аксиома? С моей точки зрения такое можно утверждать только после того, как определён общий способ нумерации алгоритмов. Гёдель определил общий способ нумерации объектов формальной теории (констант, переменных, формул и т.п.), но не способ нумерации алгоритмов, нумерующих аксиомы теории.

маткиб писал(а):

epros писал(а):

Я также понимаю, что алгоритм определяется некой конечной формулой (если хотите - кодом алгоритма).

А я понимаю только кодом, а формулой - не понимаю.

Код алгоритма - это и есть формула: в языке той теории, в которой определяются алгоритмы. Применительно к рассматриваемому случаю: алгоритмы, нумерующие аксиомы теории, определяются в мета-теории.

С другой стороны формулу арифметики тоже можно интерпретировать как алгоритм. Например, формула:
$\exists x,y,z \in \mathbb{N} (x \cdot y \cdot z = 6 \wedge x \ne y \wedge y \ne z \wedge z \ne x)$
предполагает вполне конкретный алгоритм её проверки, включающий разложение числа 6 на сомножители и т.п. Этот алгоритм следует из определений тех понятий, которые используются в формуле.

маткиб писал(а):

Я не понимаю, что означает фраза "алгоритм является объектом теории". Алгоритм имеет номер и всё! Лично мне больше ничего не надо. Является ли он там или не является объектом теории - да по барабану.

Тогда определите общий способ нумерации алгоритмов. Только не забывайте, что нам нужно пронумеровать именно алгоритмы, нумерующие аксиомы теории.

маткиб писал(а):

Лично мне для определения моей мета($\omega$)-доказуемости совершенно не нужно каким-то образом "записывать алгоритм, перечисляющий аксиомы, формулой в языке теории". Мне важно, что:
1) алгоритм существует (=> имеет номер);
2) существует алгоритм, который по номеру этого алгоритма вычисляет номер следующего алгоритма (т.е. того, который перечисляет аксиомы мета(n+1)-доказуемости);
3) существует алгоритм, который перечисляет все аксиомы мета(n)-доказуемостей для всех n (он тривиально строится из алгоритма в пункте 2);
4) для любой формулы $\Phi$ языка "0S+*=" я могу построить формулу этого же языка, которая будет по моему личному мнению утверждать, что $(\exists n)(\Phi\text{ мета(n)-доказуема})$ (эта формула строится на основе номера алгоритма из пункта 3 и стандартных конструкций, идущих от Гёделя).

Как видите, у меня возникают вопросы уже к первому пункту.

маткиб писал(а):

epros писал(а):

С моей точки зрения "перечислить аксиомы" - это значит определить соответствие между аксиомами и их номерами. Может быть я неправильно Вас понял?

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

Аха, т.е. Вы уточняете, что перечисляющий алгоритм $\xi(k)$ выплёвывает не сами аксиомы теории (строки), а Гёделевские номера соответствующих формул? Таким образом перечисляющий алгоритм является чисто арифметическим (перерабатывает число в число), а поэтому с Вашей точки зрения его не может не быть в теории? Я правильно Вас понял?

Хочу заметить, что это существа дела абсолютно не изменит. Моё доказательство несуществования формулы для $\xi(k)$ в языке теории остаётся в силе. Просто нужно там, где в доказательстве упоминается "формула $\varphi_k(n)$ теории" нужно говорить: "Гёделевский номер формулы $\varphi_k(n)$ теории".

[маткиб]

epros писал(а):

Аха, т.е. Вы уточняете, что перечисляющий алгоритм $\xi(k)$ выплёвывает не сами аксиомы теории (строки), а Гёделевские номера соответствующих формул? Таким образом перечисляющий алгоритм является чисто арифметическим (перерабатывает число в число), а поэтому с Вашей точки зрения его не может не быть в теории? Я правильно Вас понял?

Вот именно! Мы всё делаем с номерами, и только с ними.

epros писал(а):

маткиб писал(а):

Если алгоритм существует, то у него есть номер.

Это что же, очередная, в лучших традициях "классической" математики взятая с потолка аксиома? С моей точки зрения такое можно утверждать только после того, как определён общий способ нумерации алгоритмов.

Никакая это не аксиома. Способ нумерации алгоритмов определён (возьмите любой, какой Вам нравится, способ нумерации таблиц машин Тьюринга). Если это было не понятно, то добавлю: нас интересуют только алгоритмы, которые в некоторые моменты времени выдают натуральные числа, либо такие, которые выдают ровно одно число (если завершаются). Иногда нас интересуют алгоритмы, имеющие вход (натуральное число), а иногда - без входа. Для каждого из этих типов можно взять отдельную нумерацию. Например, алгоритм, перечисляющий номера аксиом - это алгоритм без входа, а алгоритм, преобразующий номер перечисляющего алгоритма в номер другого перечисляющего алгоритма - это алгоритм со входом.

epros писал(а):

маткиб писал(а):

Я не понимаю, что означает фраза "алгоритм является объектом теории". Алгоритм имеет номер и всё! Лично мне больше ничего не надо. Является ли он там или не является объектом теории - да по барабану.

Тогда определите общий способ нумерации алгоритмов. Только не забывайте, что нам нужно пронумеровать именно алгоритмы, нумерующие аксиомы теории.

Нам не нужно нумеровать алгоритмы, перечисляющие аксиомы теории. Нам нужно занумеровать алгоритмы, выдающие последовательности натуральных чисел, и потом выбрать один, который будет выплёвывать номера аксиом теории.

epros писал(а):

Хочу заметить, что это существа дела абсолютно не изменит. Моё доказательство несуществования формулы для $\xi(k)$ в языке теории остаётся в силе. Просто нужно там, где в доказательстве упоминается "формула $\varphi_k(n)$ теории" нужно говорить: "Гёделевский номер формулы $\varphi_k(n)$ теории".

Перепишите Ваше доказательство с нужными заменами и снабдив его определением, что же Вы собираетесь доказывать (сам я этого сделать не способен). Тогда я укажу конкретное место, где у Вас ошибка.

[epros]

маткиб писал(а):

Например, алгоритм, перечисляющий номера аксиом - это алгоритм без входа

У Вас странные представления об алгоритмах. По моим понятиям алгоритм - это некая целостная программа действий, которая заканчивается неким результатом. Поэтому мне странно говорить о каких-то этапах или "шагах" алгоритма, на каждом из которых выдаётся некий "промежуточный результат". С моей точки зрения алгоритм, перечисляющий аксиомы, в качестве результата выдаёт аксиому (или Гёделевский номер соответствующей формулы языка теории - без разницы), поэтому его входом должен быть номер аксиомы в последовательности. Естественно, результат выполнения алгоритма для $k \text{-того}$ аргумента может определяться через результат выполнения алгоритма для $(k-1) \text{-вого}$ аргумента, т.е. формула может быть рекурсивной. В принципе это согласуется с Вашим представлением о "бесконечном" алгоритме без входа, который выполняется "по шагам". Я просто уточняю понятия: алгоритм должен иметь точку останова, иначе он "неразрешим" и, соответственно, малоинтересен.

Существенный момент заключается в том, что алгоритм $\xi(k)$ вообще можно считать "определённым" только после того, как определён его код (в форме конечной строки), который позволяет для произвольного значения $k$ аргумента вычислить результат выполнения алгоритма. Т.е. нельзя отделаться общим заявлением о том, что "какой-то результат выполнения на любом $k \text{-том}$ шаге будет получен", - пока нет общей формулы, определяющей код алгоритма, нет и самого алгоритма.

маткиб писал(а):

Нам не нужно нумеровать алгоритмы, перечисляющие аксиомы теории. Нам нужно занумеровать алгоритмы, выдающие последовательности натуральных чисел, и потом выбрать один, который будет выплёвывать номера аксиом теории.

Во-первых, об аксиомах какой теории идёт речь? Насколько я помню, речь была не об одной теории, а о бесконечном ряде мета(n)-расширений арифметики. У каждого мета(n)-расширения своя аксиоматика и, соответственно, должен быть свой алгоритм, перечисляющий аксиомы.

Во-вторых, проблема заключается в том, как Вы выберете именно алгоритм, перечисляющий аксиомы, из совокупности всех возможных алгоритмов, выдающих последовательности натуральных чисел. Одного заявления о том, что "в совокупности таковых алгоритмов нужный нам непременно найдётся" мне недостаточно: нет указания как получить алгоритм - значит нет и алгоритма.

маткиб писал(а):

Перепишите Ваше доказательство с нужными заменами и снабдив его определением, что же Вы собираетесь доказывать (сам я этого сделать не способен). Тогда я укажу конкретное место, где у Вас ошибка.

По-моему я совершенно чётко сформулировал "что я собираюсь доказывать": что алгоритм, перечисляющий аксиомы любой формальной теории, расширяющей арифметику, нельзя записать (определить) формулой в языке теории (даже если этот алгоритм работает только с числами).

Зачем мне это нужно я тоже уже несколько раз высказал: Потому что мне неизвестен способ определения номеров для алгоритмов, перечисляющих аксиомы. Если бы такие алгоритмы можно было записать формулами теории, то их номерами стали бы Гёделевские номера соответствующих формул.

Ваше заявление о том, что можно занумеровать все алгоритмы, определяющие последовательности чисел (я не буду отрицать, что это возможно), меня не успокаивает. Поскольку мне нужны не "все алгоритмы", а те и только те, которые определяют последовательности аксиом рассматриваемых теорий. Без этого Вы не сделаете даже первого шага $F(n)$ - не определите какое число $n$ нужно подать на вход функции $F$.