Теорема Лёба

[маткиб]

epros писал(а):

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

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

epros писал(а):

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

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

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

В том предложении, видимо, речь шла об исходной теории (арифметике Пеано).

epros писал(а):

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

Какое указание Вам нужно? Программу что ли выписать? Думаю, Вы самостоятельно сможете написать программу, которая перечисляет аксиомы Пеано, а потом и номер у неё определить.

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

function F(n: натуральное): натуральное;
var
  s, s1: string;
begin

  s := программа на почти паскале, соответствующая алгоритму с номером n;

  s1 := 'if (n чётно) then begin n := n div 2; s1 := формула с номером n; s2 := формула, построенная на основе Гёделевской техники, утверждающая о доказуемости формулы с номером n в теории с аксиомами, номера которых перечисляются алгоритмом с номером ' + inttostr(n) + '; s3 := s2 + "->" + s1; result := номер s3; exit; end else n := n div 2;';

  Приписать к s после begin s1 и добавить объявления необходимых переменных (при необходимости переименовать);

  result := номер s;

end;

epros писал(а):

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

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

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

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

Вот Вы пример привели

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 на сомножители и т.п. Этот алгоритм следует из определений тех понятий, которые используются в формуле.

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

epros писал(а):

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

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

[epros]

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

Какое указание Вам нужно? Программу что ли выписать? Думаю, Вы самостоятельно сможете написать программу, которая перечисляет аксиомы Пеано, а потом и номер у неё определить.

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

Первоначально а полагал, что имея последовательность алгоритмов $\xi_0(k), \xi_1(k), \xi_2(k), ...$, перечисляющих, соответственно, аксиомы теории, мета(1)-, мета(2)- и т.д. теорий, причём алгоритмы пронумерованы последовательно, Вы хотите с помощью диагональной процедуры нумерации построить алгоритм $\xi_{\omega}(n)$, перечисляющий все аксиомы всех мета-уровней. Т.е. $\xi_{\omega}(n) = \xi_i(k)$ , где $i$ и $k$ довольно просто выражаются через $n$.

Проблема здесь только одна: у нас нет общей формулы (если хотите - кода) для $\xi_i(k)$, а значит нет и общей формулы для $\xi_{\omega}(n)$. Очевидно, что существование формул для каждого $i$ не означает существования общей формулы для всех $i$. А нет формулы (кода) алгоритма - значит нет и самого алгоритма.

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

function F(n: натуральное): натуральное;
var
  s, s1: string;
begin

  s := программа на почти паскале, соответствующая алгоритму с номером n;

  s1 := 'if (n чётно) then begin n := n div 2; s1 := формула с номером n; s2 := формула, построенная на основе Гёделевской техники, утверждающая о доказуемости формулы с номером n в теории с аксиомами, номера которых перечисляются алгоритмом с номером ' + inttostr(n) + '; s3 := s2 + "->" + s1; result := номер s3; exit; end else n := n div 2;';

  Приписать к s после begin s1 и добавить объявления необходимых переменных (при необходимости переименовать);

  result := номер s;

end;

Мне непонятно:
1. Зачем нужны эти странные преобразования номера n в код s и обратно?
2. Всё-таки что такое n? Это Гёделевский номер формулы $\Phi$, для которой строится аксиома $(M_k \vdash \Phi) \to \Phi$, или это всё-таки "номер алгоритма, перечисляющего аксиомы"?

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

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

Вот Вы пример привели

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 на сомножители и т.п. Этот алгоритм следует из определений тех понятий, которые используются в формуле.

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

Формулам арифметики ставятся в соответствие алгоритмы согласно определениям присутствующих в формулах арифметических операций. Не вижу в этом никакой принципиальной проблемы. Давайте рассмотрим другой пример: Вот мы с Вами согласились с тем, что алгоритм $\xi(k)$, перечисляющий аксиомы, принимает на входе число (номер аксиомы) и выдаёт в результате число (Гёделевский номер соответствующей формулы). А вот пример арифметического выражения, которое тоже принимает на входе число и выдаёт на выходе число:
$\xi(k) = k \cdot (k+1) \cdot (k+2) / 3 - k + 1$

Может (в принципе) подобное арифметическое выражение быть определением такого алгоритма? А в чём проблема? Последовательность вычисления арифметических операций определена, а это и есть "алгоритм" вычисления численного результата из заданного численного аргумента.

[маткиб]

epros писал(а):

Мне нужно понять, как Вы нумеруете такие программы и, соответственно, как восстанавливаете их код по номеру.

Ладно. Пусть программа - это строка символов $x_0x_1\ldots x_n$ в алфавите $\{0,1,\ldots,255\}$. Тогда её номером будет $(x_0+1)+(x_1+1)\cdot 257+(x_2+1)\cdot 257^2+\ldots+(x_n+1)\cdot 257^n$.

epros писал(а):

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

А я не понимаю, что Вы подразумеваете под кодом. Саму программу как строку символов что ли? А фокусы нужны только для одного: чтобы построить утверждение в языке 0+*S=, которое является свойством строк вертикальных палочек, но не является мета(n) доказуемым в арифметике Пеано ни для какого n.

epros писал(а):

Мне непонятно:
1. Зачем нужны эти странные преобразования номера n в код s и обратно?

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

epros писал(а):

2. Всё-таки что такое n? Это Гёделевский номер формулы $\Phi$, для которой строится аксиома $(M_k \vdash \Phi) \to \Phi$, или это всё-таки "номер алгоритма, перечисляющего аксиомы"?

n у меня - это имя параметра у функций, причём как у F, так и у той, что перечисляет аксиомы (т.е. номер которой подается на вход F и возвращается на выходе). Чтобы не было путаницы, перепишу программу так, что на вход F подается n, а на вход перечисляющих функций - m (и чтобы имена переменных там и там были разными):

function F(n: натуральное): натуральное;
var
  s, s1: string;
begin

  s := программа на почти паскале, соответствующая алгоритму с номером n;

  s1 := 'if (m чётно) then begin m := m div 2; ss1 := формула с номером m; ss2 := формула, построенная на основе Гёделевской техники, утверждающая о доказуемости формулы с номером m в теории с аксиомами, номера которых перечисляются алгоритмом с номером ' + inttostr(n) + '; ss3 := ss2 + "->" + ss1; result := номер ss3; exit; end else m := m div 2;';

  Приписать к s после begin s1 и добавить объявления необходимых переменных (при необходимости переименовать);

  result := номер s;

end;

epros писал(а):

Формулам арифметики ставятся в соответствие алгоритмы согласно определениям присутствующих в формулах арифметических операций. Не вижу в этом никакой принципиальной проблемы. Давайте рассмотрим другой пример: Вот мы с Вами согласились с тем, что алгоритм $\xi(k)$, перечисляющий аксиомы, принимает на входе число (номер аксиомы) и выдаёт в результате число (Гёделевский номер соответствующей формулы). А вот пример арифметического выражения, которое тоже принимает на входе число и выдаёт на выходе число:
$\xi(k) = k \cdot (k+1) \cdot (k+2) / 3 - k + 1$

Может (в принципе) подобное арифметическое выражение быть определением такого алгоритма? А в чём проблема? Последовательность вычисления арифметических операций определена, а это и есть "алгоритм" вычисления численного результата из заданного численного аргумента.

Всё равно ничего не понимаю. Во-первых, у нас в синтаксисе нет вычитания и деления, поэтому Ваш пример сразу не подходит. И что, Вы рассматриваете в качестве определений алгоритмов только такие формулы, которые содержат только константы, переменные и функциональные символы (т.е. никаких логических символов и кванторов)? Т.е. класс вычислимых функций у Вас - это множество всех функций, которые получаются из 0, x+1, x+y, x*y с помощью суперпозиции? Но ведь это полиномы с целыми неотрицательными коэффициентами! Кому нафиг нужен такой класс вычислимых функций, не удовлетворяющий тезису Чёрча-Тьюринга (причём совсем)? В такой постановке я не удивлюсь, что Ваше утверждение про непредставимость будет верно

[epros]

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

Ладно. Пусть программа - это строка символов $x_0x_1\ldots x_n$ в алфавите $\{0,1,\ldots,255\}$. Тогда её номером будет $(x_0+1)+(x_1+1)\cdot 257+(x_2+1)\cdot 257^2+\ldots+(x_n+1)\cdot 257^n$.

Хорошо. Теперь у меня по крайней мере будет понимание того, что Вы нумеруете алгоритмы по их кодам. А то в некоторый момент у меня даже возникло подозрение, что Вы хотите их нумеровать по таблицам входов - выходов.

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

А я не понимаю, что Вы подразумеваете под кодом. Саму программу как строку символов что ли?

Да, "сама программа как строка символов" обычно называется её "кодом", а что же ещё?

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

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

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

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

Всё равно ничего не понимаю. Во-первых, у нас в синтаксисе нет вычитания и деления, поэтому Ваш пример сразу не подходит.

Ну, это не столь существенно. Я привёл просто "арифметическую" формулу, а не собственно формулу в указанном Вами синтаксисе. Вы же понимаете, что вычитание и деление в принципе можно записать в указанном Вами синтаксисе.

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

И что, Вы рассматриваете в качестве определений алгоритмов только такие формулы, которые содержат только константы, переменные и функциональные символы (т.е. никаких логических символов и кванторов)? Т.е. класс вычислимых функций у Вас - это множество всех функций, которые получаются из 0, x+1, x+y, x*y с помощью суперпозиции?

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

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

В такой постановке я не удивлюсь, что Ваше утверждение про непредставимость будет верно

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

P.S. Вы как-то оставили без внимания моё соображение относительно отсутствия общей формулы (кода) для алгоритма $\xi_{\omega}(k)$, перечисляющего все аксиомы всех уровней мета-доказуемости. Ваши доводы пока не убеждают меня в наличии таковой. Понятно, что если у нас есть ряд формул $\xi_0(k), \xi_1(k), \xi_2(k), ...$, то можно пронумеровать все возможные результаты их выполнения, но не факт, что у нас есть общий алгоритм для построения любого из этих результатов.

[маткиб]

epros писал(а):

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

,так и не удосужившись сформулировать утверждение, которое Вы доказали.

epros писал(а):

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

Всё равно ничего не понимаю. Во-первых, у нас в синтаксисе нет вычитания и деления, поэтому Ваш пример сразу не подходит.

Ну, это не столь существенно. Я привёл просто "арифметическую" формулу, а не собственно формулу в указанном Вами синтаксисе. Вы же понимаете, что вычитание и деление в принципе можно записать в указанном Вами синтаксисе.

В каком смысле записать?

Можно, например, считать, что функцию $f(x_1,\ldots,x_n)$ можно записать, если существует такая формула $\Phi(x_1,\ldots,x_n,y)$, что $(y=f(x_1,\ldots,x_n))$ эквивалентно истинности $\Phi(x_1,\ldots,x_n,y)$. Тогда действительно много функций можно будет записать (например, деление, вычитание, возведение в степень и т.д.), но Вам это не подходит, потому что:
1. Используется понятие истинности, которое Вам не нравится.
2. Понятие алгоритма Вы на основе этого не сформулируете, потому что уже на этом этапе происходит нарушение тезиса Чёрча-Тьюринга в "большую" сторону (т.е. существует записываемая невычислимая по Тьюрингу функция).
3. Ваше доказательство работать не будет, потому что работать с истинностью в самой теории Вы не сможете (теорема Тарского).

А в каком смысле Вы понимаете слово "записать", я не понимаю.

epros писал(а):

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

Итак, с Вас определение, каким образом арифметическим формулам ставятся в соответствие алгоритмы (точнее, вычислимые функции, потому что, алгоритм, как я понимаю, - это и есть сама формула).

Например, какой алгоритм (или вычислимая функция?) соответствует формуле с одной свободной переменной $t$:

$$ (\forall x_1)(\forall y_1)(\forall z_1)(\forall x_2)(\forall y_2)(\forall z_2)\neg(x_1\cdot x_1\cdot x_1+y_1\cdot y_1\cdot y_1=z_1\cdot z_1\cdot z_1\ \&\ x_2\cdot x_2\cdot x_2+y_2\cdot y_2\cdot y_2=z_2\cdot z_2\cdot z_2\ \&\ z_2 = z_1 + t) $$

?

epros писал(а):

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

Сформулируйте уже наконец это Ваше утверждение, а то я весь в нетерпении

epros писал(а):

P.S. Вы как-то оставили без внимания моё соображение относительно отсутствия общей формулы (кода) для алгоритма $\xi_{\omega}(k)$, перечисляющего все аксиомы всех уровней мета-доказуемости. Ваши доводы пока не убеждают меня в наличии таковой. Понятно, что если у нас есть ряд формул $\xi_0(k), \xi_1(k), \xi_2(k), ...$, то можно пронумеровать все возможные результаты их выполнения, но не факт, что у нас есть общий алгоритм для построения любого из этих результатов.

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

[epros]

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

epros писал(а):

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

,так и не удосужившись сформулировать утверждение, которое Вы доказали.

Я не понял, чего ещё-то Вы хотите? Что такое "алгоритм $\xi(k)$, перечисляющий аксиомы" мы с Вами вроде бы уже договорились: Это, если хотите, программа, принимающая на вход любое натуральное число $k$ (порядковый номер аксиомы), а на выходе выдающая гёделевский номер $n$ соответствующей формулы теории. "Выразить арифметической формулой" это значит записать в синтаксисе арифметики выражение, соответствующее равенству $n = \xi(k)$.

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

Можно, например, считать, что функцию $f(x_1,\ldots,x_n)$ можно записать, если существует такая формула $\Phi(x_1,\ldots,x_n,y)$, что $(y=f(x_1,\ldots,x_n))$ эквивалентно истинности $\Phi(x_1,\ldots,x_n,y)$.

Вы что-то мудрите. $y=f(x_1,\ldots,x_n)$ - это и есть "такая формула". Если, конечно, она записана в синтаксисе арифметики.

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

но Вам это не подходит, потому что:
1. Используется понятие истинности, которое Вам не нравится.

Неужели? И к чему же мне здесь пришить это пресловутое "понятие истинности"? Если мне вдруг придёт в голову записать функцию $f(x) = x + 2$ какой-то другой формулой, которая "эквивалентна её истинности", то я, конечно, могу это сделать. Например, я могу записать такую формулу:
$y = 1 + (x + 1)$
Она "другая" в том смысле, что не совпадает посимвольно с формулой $y = x + 2$, но она по Вашему выражению "эквивалентна её истинности". Ну и что? Зачем мне тут нужно какое-то специфическое "понятие истинности", если утверждение об эквивалентности (равносильности) формул я могу записать, например, так:
$\forall x,y \in \mathbb{N}(y = x + 2 \leftrightarrow y = 1 + (x + 1))$

Как видите, это тоже формула в синтаксисе той же арифметики.

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

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

А зачем мне формулировать на основе этого понятие алгоритма? Меня вполне устраивает понятие алгоритма, сформулированное до меня. Например, понятие "нормального алгоритма", введённое Марковым. Или понятие рекурсивно вычислимой функции.

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

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

Моё доказательство ничего не говорит о понятии "истинности".

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

А в каком смысле Вы понимаете слово "записать", я не понимаю.

В прямом. Символами алфавита теории записать строку, являющуюся формулой в синтаксисе теории.

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

Например, какой алгоритм (или вычислимая функция?) соответствует формуле с одной свободной переменной $t$:

$$ (\forall x_1)(\forall y_1)(\forall z_1)(\forall x_2)(\forall y_2)(\forall z_2)\neg(x_1\cdot x_1\cdot x_1+y_1\cdot y_1\cdot y_1=z_1\cdot z_1\cdot z_1\ \&\ x_2\cdot x_2\cdot x_2+y_2\cdot y_2\cdot y_2=z_2\cdot z_2\cdot z_2\ \&\ z_2 = z_1 + t) $$

?

Например, так:
Берём предъявленное в качестве аргумента число $t$ и, по очереди подставляя числа вместо переменных $x_1, y_1, ...$ и т.д., проверяем, действительно ли не выполняются все три указанных равенства для всех переменных. Разумеется, такой алгоритм не будет иметь точки останова, но никто и не обещал.

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

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

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

[маткиб]

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

epros писал(а):

Я не понял, чего ещё-то Вы хотите? Что такое "алгоритм $\xi(k)$, перечисляющий аксиомы" мы с Вами вроде бы уже договорились: Это, если хотите, программа, принимающая на вход любое натуральное число $k$ (порядковый номер аксиомы), а на выходе выдающая гёделевский номер $n$ соответствующей формулы теории. "Выразить арифметической формулой" это значит записать в синтаксисе арифметики выражение, соответствующее равенству $n = \xi(k)$.

вытекает, что формула называется выражающей функцию $f(x_1,\ldots,x_n)$, если $\Phi$ соответствует (т.е. семантически эквивалентна) равенству $y=f(x_1,\ldots,x_n)$.

А отсюда

epros писал(а):

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

Например, какой алгоритм (или вычислимая функция?) соответствует формуле с одной свободной переменной $t$:

$$ (\forall x_1)(\forall y_1)(\forall z_1)(\forall x_2)(\forall y_2)(\forall z_2)\neg(x_1\cdot x_1\cdot x_1+y_1\cdot y_1\cdot y_1=z_1\cdot z_1\cdot z_1\ \&\ x_2\cdot x_2\cdot x_2+y_2\cdot y_2\cdot y_2=z_2\cdot z_2\cdot z_2\ \&\ z_2 = z_1 + t) $$

?

Например, так:
Берём предъявленное в качестве аргумента число $t$ и, по очереди подставляя числа вместо переменных $x_1, y_1, ...$ и т.д., проверяем, действительно ли не выполняются все три указанных равенства для всех переменных. Разумеется, такой алгоритм не будет иметь точки останова, но никто и не обещал.

следует рекурсивное определение:
1) Если $\Phi$ - элементарная формула (т.е. вида $t_1=t_2$), то $\Phi$ соответствует алгоритм, получающий на вход значения всех свободных переменных и тупо вычисляющий значение $\Phi$ на них.
2) Если $\Phi$ имеет вид $(\exists x)\Psi$, то ей соответствует алгоритм, перебирающий значения $x=0,1,2,\ldots$, и для каждого $x$ запускающий алгоритм для $\Psi$; если запускаемый сказал "да", то выдать "да".
3) Если $\Phi$ имеет вид $(\forall x)\Psi$, то соответствует зацикливающийся алгоритм;
4) Если $\Phi$ имеет вид $\Psi_1\&\Psi_2$, $\Psi_1\vee\Psi_2$, $\Psi_1\rightarrow\Psi_2$ или $\neg\Psi_1$, то соответствующий алгоритм запускает алгоритмы для $\Psi_1$ и $\Psi_2$ (или только для $\Psi_1$) и выдаёт результат соответствующей логической операции над их результатами.

Из этого определения, например, следует, что квантор $\forall$ в принципе не нужен (потому что сразу приводит к зацикливанию). И это определение для алгоритмов, возвращающих "да"/"нет" (хотя для выдачи натуральных чисел это определение легко переделывается).

Модификации:
1) Особая обработка нескольких подряд идущих кванторов существования: если $\Phi$ имеет вид $(\exists y_1)\ldots(\exists y_m)\Psi$, то алгоритм перебирает векторы $(y_1,\ldots,y_m)$, и для каждого запускает вычисление $\Psi$.
2) При вычислении логических операций использовать "ленивые вычисления", т.е. если, например, в выражении $A\vee B$ уже известно, что $A$ истинно, то $B$ можно не вычислять.
3) Если $\Phi$ есть $\Psi_1\vee\Psi_2$, то алгоритмы для $\Psi_1$ и $\Psi_2$ запускать параллельно, и выдавать ответ "да" в случае, если какой-то из них скажет "да" (завершения другого не ждать). Аналогично для $\Psi_1\rightarrow\Psi_2$.

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

Так какое определение правильное?

epros писал(а):

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

Можно, например, считать, что функцию $f(x_1,\ldots,x_n)$ можно записать, если существует такая формула $\Phi(x_1,\ldots,x_n,y)$, что $(y=f(x_1,\ldots,x_n))$ эквивалентно истинности $\Phi(x_1,\ldots,x_n,y)$.

Вы что-то мудрите. $y=f(x_1,\ldots,x_n)$ - это и есть "такая формула". Если, конечно, она записана в синтаксисе арифметики.

$f$ - это вообще функция, а не формула, поэтому она не может быть "уже записана" в синтаксисе теории.

epros писал(а):

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

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

[epros]

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

отсюда

epros писал(а):

Я не понял, чего ещё-то Вы хотите? Что такое "алгоритм $\xi(k)$, перечисляющий аксиомы" мы с Вами вроде бы уже договорились: Это, если хотите, программа, принимающая на вход любое натуральное число $k$ (порядковый номер аксиомы), а на выходе выдающая гёделевский номер $n$ соответствующей формулы теории. "Выразить арифметической формулой" это значит записать в синтаксисе арифметики выражение, соответствующее равенству $n = \xi(k)$.

вытекает, что формула называется выражающей функцию $f(x_1,\ldots,x_n)$, если $\Phi$ соответствует (т.е. семантически эквивалентна) равенству $y=f(x_1,\ldots,x_n)$.

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

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

1) Если $\Phi$ - элементарная формула (т.е. вида $t_1=t_2$), то $\Phi$ соответствует алгоритм, получающий на вход значения всех свободных переменных и тупо вычисляющий значение $\Phi$ на них.

Это я не вполне понял. $t_1$ и $t_2$ это и есть свободные переменные? Тогда это формула предиката равенства, которой может соответствовать алгоритм сравнения двух объектов.

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

2) Если $\Phi$ имеет вид $(\exists x)\Psi$, то ей соответствует алгоритм, перебирающий значения $x=0,1,2,\ldots$, и для каждого $x$ запускающий алгоритм для $\Psi$; если запускаемый сказал "да", то выдать "да".

Да. На всякий случай уточню, что для запуска $\Psi$ для следующего $x$ не нужно дожидаться окончания выполнения для предыдущего $x$. Как только хотя бы один из запущенных алгоритмов для $\Psi$ скажет "да", алгоритм в целом считается завершившимся с результатом "да".

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

3) Если $\Phi$ имеет вид $(\forall x)\Psi$, то соответствует зацикливающийся алгоритм;

Не совсем так, ибо результат "нет" тоже может приниматься. Если он получен хотя бы для одного из $x$, то весь алгоритм в целом считается завершившимся с результатом "нет".

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

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

4) Если $\Phi$ имеет вид $\Psi_1\&\Psi_2$, $\Psi_1\vee\Psi_2$, $\Psi_1\rightarrow\Psi_2$ или $\neg\Psi_1$, то соответствующий алгоритм запускает алгоритмы для $\Psi_1$ и $\Psi_2$ (или только для $\Psi_1$) и выдаёт результат соответствующей логической операции над их результатами.

С логическими операциями всё не так просто. Например, чтобы доказать отрицание, необходимо доказать неразрешимость алгоритма, доказывающего $\Psi$. Обычно это выполняется путём сведения предположения $\Psi$ к противоречию. Что такое "противоречие" (или "абсурд") - это отдельная песня. Насколько я понимаю, большинство конструктивистов принимают его за базовое (неопределимое) понятие, т.е. полагают, что в любой формальной системе существует высказывание, которое считается очевидным образом неверным. Например, в арифметике таковым можно считать высказывание $1 = 2$. Вывод его из $\Psi$ означает доказательство $\neg \Psi$ (т.е. опровержение $\Psi$).

Но есть и варианты логики без отрицания и, соответственно, без понятия об абсурде.

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

1) Особая обработка нескольких подряд идущих кванторов существования: если $\Phi$ имеет вид $(\exists y_1)\ldots(\exists y_m)\Psi$, то алгоритм перебирает векторы $(y_1,\ldots,y_m)$, и для каждого запускает вычисление $\Psi$.
2) При вычислении логических операций использовать "ленивые вычисления", т.е. если, например, в выражении $A\vee B$ уже известно, что $A$ истинно, то $B$ можно не вычислять.
3) Если $\Phi$ есть $\Psi_1\vee\Psi_2$, то алгоритмы для $\Psi_1$ и $\Psi_2$ запускать параллельно, и выдавать ответ "да" в случае, если какой-то из них скажет "да" (завершения другого не ждать). Аналогично для $\Psi_1\rightarrow\Psi_2$.

В принципе тут всё правильно, хотя с импликацией тоже есть тонкости.

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

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

Так какое определение правильное?

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

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

Здесь возможны несколько вариантов:
1. Формулы (или алгоритмы) несомненно равны тогда, когда посимвольно совпадают их коды.
2. Может оказаться так, что мы располагаем доказательством совпадения результатов выполнения алгоритмов или значений формул для всех возможных значений аргументов. В этом случае формулы и алгоритмы тоже можно считать "эквивалентными". Но этот случай предполагает, что мы не столкнулись ни с одним случаем возможной неразрешимости алгоритма или недоказуемости формулы (ни при одном из значений аргументов).
3. Если мы пока не смогли достичь точки останова алгоритма или не смогли получить доказательство формулы для некоторых значений аргументов, то мы всё-таки можем считать их "эквивалентными" в том смысле, что для всех случаев, когда результаты (выполнения алгоритма или доказательства формулы) точно известны, между ними не возникает противоречий.

Все рассмотренные Вами способы построения формул арифметики, экивалентных алгоритмам, и алгоритмов, эквивалентных формулам арифметики, соответствуют по крайней мере 3-ему варианту интерпретации понятия эквивалентности. Это соответствует и конструктивному пониманию формулы $\Psi \leftrightarrow \xi$, где $\Psi$ - формула, а $\xi$ - результат выполнения алгоритма. Т.е. эта формула доказана, если доказана $\Psi$ и алгоритм $\xi$ сказал "да", а также если опровергнута $\Psi$ и $\xi$ сказал "нет", и эта формула опровергнута, если доказана $\Psi$ и $\xi$ сказал "нет", а также если опровергнута $\Psi$ и $\xi$ сказал "да". Во всех остальных случаях, т.е. если либо $\Psi$ не разрешена, либо $\xi$ не достиг точки останова, данная формула эквивалентности считается неразрешённой. Так вот, если мы докажем неопровержимость этой формулы эквивалентности (в конструктивной логике неопровержимость - это двойное отрицание, и из неё не всегда следует доказанность формулы), то мы спокойно можем считать эквивалентность в 3-ем смысле доказанной. Это к вопросу о том, что является арифметической формулой, "эквивалентной" алгоритму (как Вы выразились, "семантически"). Что касается вопроса о том, что является алгоритмом, "эквивалентным" арифметической формуле, то описанные способы построения алгоритмов по арифметическим формулам автоматически гарантируют эквивалентность в том же (т.е в 3-ем) смысле, хотя не всегда гарантируют разрешимость алгоритма даже там, где формула разрешима.

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

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

$f$ - это вообще функция, а не формула, поэтому она не может быть "уже записана" в синтаксисе теории.

Выше я рассматривал пример функции $y = x + 2$. Разве эта функция не определяется формулой? Или Вы считаете, что "первоначально" функция существует не в виде формулы, а где-то в Вашем "воображаемом мире", и только иногда оказывается выраженной формулой? С моей точки зрения функция определена в теории только тогда, когда для неё указана формула. Если формулы нет, то нет и функции, а есть только абстрактные разговоры о ней.

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

epros писал(а):

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

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

Вообще-то я постепенно прихожу к мысли, что в отношении мета($\omega$)-доказуемости Вы правы. Т.е. алгоритмы $\xi_n(k)$, перечисляющие аксиомы любого уровня мета($n$)-доказуемости, можно записать одной рекурсивно вычислимой функцией двух переменных $n$ и $k$.

Правда это похоже на какую-то логическую игру, поскольку, как я понимаю, чтобы реально вычислить эту функцию уже для очень небольших $n$ и $k$ (скажем, для $n \ge 2$) не хватит вычислительных ресурсов всей Вселенной. Т.е. реально мы не только никогда не сможем воспользоваться какими-либо преимуществами мета($\omega$)-доказуемости, мы вряд ли сможем даже мета(2)-доказать что-либо действительно интересное. Даже Гёделевское $G$ для арифметики, доказуемое на мета(1)-уровне, "вживую" вроде бы никто ещё не выписал, да и вряд ли это кому-нибудь нужно, ибо в этом высказывании, кроме его доказуемости лишь на мета(1)-уровне, нет абсолютно ничего интересного. Так что если говорить не о логических играх, а о чём-то полезном, то лучше рассматривать на ближайших мета-уровнях только то, что действительно интересно, но вряд ли легко доказуемо в самой арифметике. Например, есть нерешённая математическая проблема существования нечётных совершенных чисел. Возможно, она и неразрешима в теории, зато может быть разрешится на мета-уровне.

В этом смысле мета($\omega$)- и более высокие уровни доказуемости интересны разве что с точки зрения чистой логики. Кстати, как я понимаю, на мета($\omega$)-уровне доказуемо только то, что доказуемо на каком-либо из мета($n$)-уровней. Т.е. этот уровень (в отличие от уровней, соответствующих непредельным ординалам) не доказывает ничего нового.

[маткиб]

С алгоритмами, соответствующими формулам, я понял всё до вот этого момента

epros писал(а):

С логическими операциями всё не так просто. Например, чтобы доказать отрицание, необходимо доказать неразрешимость алгоритма, доказывающего $\Psi$. Обычно это выполняется путём сведения предположения $\Psi$ к противоречию. Что такое "противоречие" (или "абсурд") - это отдельная песня. Насколько я понимаю, большинство конструктивистов принимают его за базовое (неопределимое) понятие, т.е. полагают, что в любой формальной системе существует высказывание, которое считается очевидным образом неверным. Например, в арифметике таковым можно считать высказывание $1 = 2$. Вывод его из $\Psi$ означает доказательство $\neg \Psi$ (т.е. опровержение $\Psi$).

Т.е. у Вас к этому определению ещё и какие-то формальные выводы приплетаются?

epros писал(а):

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

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

$$ (\forall x)(\forall y)(\forall z)(x=0\vee y=0\vee\neg(x\cdot x\cdot x+y\cdot y\cdot y=z\cdot z\cdot z)) $$

как ни крути будет соответствовать незавершающийся алгоритм, однако в арифметике Пеано эту формулу можно доказать.

epros писал(а):

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

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

epros писал(а):

В этом смысле мета($\omega$)- и более высокие уровни доказуемости интересны разве что с точки зрения чистой логики. Кстати, как я понимаю, на мета($\omega$)-уровне доказуемо только то, что доказуемо на каком-либо из мета($n$)-уровней. Т.е. этот уровень (в отличие от уровней, соответствующих непредельным ординалам) не доказывает ничего нового.

И здесь Вы заблуждаетесь. Пример я уже приводил:
$(\exists n)(\mathrm{PA}_n\vdash(0=S(0)))\rightarrow(0=S(0))$,
где $\mathrm{PA}_n$ - мета(n)-арифметика Пеано,
мета($\omega$)-доказуема, но не мета(n) доказуема ни для какого n (потому что Вторая Теорема Гёделя). В этом смысле, если задать (алгоритмически) некоторый начальный отрезок ординалов, то получившаяся трансфинитная последовательность теорий будет строго монотонной.

P.S. Если сравнить доказательства в арифметике Пеано с попытками допрыгнуть до луны, то построение мета(n)-доказательств можно сравнить с попытками залезть на луну по лестнице

Это я к тому, что есть и более сильные средства, обобщающие мета($\alpha$)-доказуемости для маленьких ординалов $\alpha$ (алгоритмический пример немаленького Вы не приведёте), только Вы эти средства не признаёте. И не признаете, пока петух не клюнет

[nikov]

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

И здесь Вы заблуждаетесь. Пример я уже приводил:
$(\exists n)(\mathrm{PA}_n\vdash(0=S(0)))\rightarrow(0=S(0))$,
где $\mathrm{PA}_n$ - мета(n)-арифметика Пеано,
мета($\omega$)-доказуема, но не мета(n) доказуема ни для какого n (потому что Вторая Теорема Гёделя).

Поясните, пожалуйста, почему эта формула мета($\omega$)-доказуема.

[маткиб]

nikov писал(а):

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

И здесь Вы заблуждаетесь. Пример я уже приводил:
$(\exists n)(\mathrm{PA}_n\vdash(0=S(0)))\rightarrow(0=S(0))$,
где $\mathrm{PA}_n$ - мета(n)-арифметика Пеано,
мета($\omega$)-доказуема, но не мета(n) доказуема ни для какого n (потому что Вторая Теорема Гёделя).

Поясните, пожалуйста, почему эта формула мета($\omega$)-доказуема.

Видимо, по определению

Потому что аксиомы мета-доказуемости - это аксиомы Пеано и схема аксиом
$(\exists n)(\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi$.

[nikov]

epros писал(а):

Фактически $S$ просто утверждает, что существует некое число (а уж метатеория знает, что это число - Гёделевский номер доказательства того, что 2+2=5).

Не совсем понял, как теория может что-то "знать". Какой смысл Вы вкладываете в это?

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

epros писал(а):

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

...
Но я (метатеория) не считаю эту теорию состоятельной, поскольку не принимаю все её выводы.

Я упорно не понимаю, почему Вы представляете метатеорию в виде некоего мыслящего существа, и какой смысл Вы в это вкладываете...

Добавлено спустя 10 минут 47 секунд:

epros писал(а):

Вот Вы высказали некоторое утверждение, согласно которому ZCF-доказательство "либо существует, либо нет". А я, например, не могу исключить вариант, что касательно некоторого высказывания A может быть доказана неразрешимость в ZFC вопроса существования его ZFC-доказательства. Как я понимаю, это бы противоречило Вашему утверждению?

Не противоречило бы. Со временем может быть разработана и получить всеобщее доверие более сильная теория, чем ZFC. В рамках этой теории может рассматриваться вопрос: "существует ли в ZFC доказательство высказывания A?". И ответом на этот вопрос может оказаться "не существует". И так как мы верим этой сильной теории, мы будем считать, что доказательство действительно не существует. Хотя в самой ZFC этот вопрос был неразрешим.

Добавлено спустя 11 минут:

epros писал(а):

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

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

Добавлено спустя 17 минут 37 секунд:

epros писал(а):

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

Чтобы доказать $G$, Гёдель использовал дополнительно аксиому о корректности арифметики Пеано (если быть точным, в языке арифметики это будет схема аксиом), которая выглядит как $\mathrm{Prf}_{\mathrm{PA}}(\Phi)\rightarrow\Phi$.

Конечно же, в самой теории не может быть такой схемы аксиом. Но, принимая теорию, мы автоматически принимаем и это.

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

[epros]

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

Т.е. у Вас к этому определению ещё и какие-то формальные выводы приплетаются?

М-мм, я не понял, что Вы имеете в виду под "приплетанием формальных выводов"?

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

Я, конечно не понял Вашего определения алгоритма, соответствующего формуле (той части, что про логические операции),

Вы имеете в виду часть, касающуюся того, что мы можем считать формулу $\Psi$ соответствующей алгоритму $\xi$ если доказали $\neg \neg (\Psi \leftrightarrow \xi)$? Ну так это и есть утверждение о том, что ситуация, когда $\Psi$ говорит "да", а $\xi$ - "нет", или наоборот - т.е имеется противоречие между ними, не может возникнуть. При этом неразрешимость $\Psi$ или $\xi$ допустима.

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

но если никаких формальных выводов к этому определению не приплетать, то это Ваше утверждение будет очень сильно не соответствовать действительности. Например, формуле

$$ (\forall x)(\forall y)(\forall z)(x=0\vee y=0\vee\neg(x\cdot x\cdot x+y\cdot y\cdot y=z\cdot z\cdot z)) $$

как ни крути будет соответствовать незавершающийся алгоритм, однако в арифметике Пеано эту формулу можно доказать.

Ну да, а в чём проблема? Незавершаемость конкретного алгоритма ещё не означает опровержение доказываемого им утверждения. Алгоритм - это ведь всего лишь конкретный способ доказательства утверждения. Если способ оказался неудачным, это ещё не означает, что утверждение в принципе недоказуемо.

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

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

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

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

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

И здесь Вы заблуждаетесь. Пример я уже приводил:
$(\exists n)(\mathrm{PA}_n\vdash(0=S(0)))\rightarrow(0=S(0))$,
где $\mathrm{PA}_n$ - мета(n)-арифметика Пеано,
мета($\omega$)-доказуема, но не мета(n) доказуема ни для какого n (потому что Вторая Теорема Гёделя).

Может я туплю, но по-моему это n равно 1. Ведь $0=S(0)$ - это же высказывание в синтаксисе арифметики, правильно? А раз так, то для него должна быть аксиома уже в схеме мета-аксиом первого уровня:
$(\mathrm{PA}_1 \vdash \Phi) \to \Phi$
В схемах следующих мета-уровней такие аксиомы тоже будут, только арифметизация утверждения о доказуемости будет другой (экспоненциально более громоздкой).

Кстати, доказуемость на мета($\omega$)-уровне только того, что доказуемо на каком-либо из мета(n)-уровней, по-моему следует из достаточно простых соображений:

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

[nikov]

epros писал(а):

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

Алфавит-то зачем менять?? Например, формула $\mathrm{Prf}_{\mathrm{PA}}(\Phi)\rightarrow\Phi$ - суждение о высказываниях теории, но для для ее формулировки достаточно алфавита арифметики Пеано.

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

epros писал(а):

AGu писал(а):

От первого до второго -- вроде бы, крохотный шажок?
Для любого предложения $\varphi$ мы имеем $\mathbb N\vDash\varphi$ или $\mathbb N\vDash\neg\varphi$. Стало быть, если $\varphi$ неразрешимо, то либо $\varphi$, либо $\neg\varphi$ -- искомое предложение (т.е. неразрешимое и истинное).

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

А что за аксиоматика такая?

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

epros писал(а):

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

Не нужно забывать, что не все свойства натуральных чисел можно вывести из аксиом Пеано.
1) Усиленная конечная теорема Рамсея (http://www.ltn.lv/~podnieks/gt_rus/gram7.htm#pril2). Это утверждение о свойствах натуральных чисел, для которой существует доказательство в ZFC. В 1977 году была доказана недоказуемость этой теоремы в рамках арифметики Пеано.
2) Доказано, что существует диофантово уравнение, которое не имеет решения в натуральных числах, однако это утверждение недоказуемо в арифметике Пеано (http://www.ltn.lv/~podnieks/gt_rus/gram6.htm#glava65).
3) Ну и конечно всякие утверждения о натуральных числах - гёделевских номерах: непротиворечивость арифметики, $\mathrm{Prf}_{\mathrm{PA}}(\Phi)\rightarrow\Phi$ и т.д. Это все тоже недоказуемые в арифметике Пеано утверждения о натуральных числах, которые мы считаем истинными.

[epros]

nikov писал(а):

Не совсем понял, как теория может что-то "знать". Какой смысл Вы вкладываете в это?

Очень простой и непосредственный смысл: Есть в теории соответствующие теоремы (или аксиомы) или нет. В том примере, насколько я помню, речь была о том, что в теории есть некая теорема, которая утверждает, что существует некое число, обладающее некими свойствами. И только в метатеории (но не в самой теории) можно найти теорему, утверждающую, что это высказывание равносильно 2+2=5.

nikov писал(а):

Я упорно не понимаю, почему Вы представляете метатеорию в виде некоего мыслящего существа, и какой смысл Вы в это вкладываете...

Нет, не мыслящего существа. Но мы (мыслящие существа), рассуждая, находимся в рамках некой теории. Например, находясь в рамках метатеории, мы можем утверждать несостоятельность некой теории.

nikov писал(а):

epros писал(а):

Вот Вы высказали некоторое утверждение, согласно которому ZCF-доказательство "либо существует, либо нет". А я, например, не могу исключить вариант, что касательно некоторого высказывания A может быть доказана неразрешимость в ZFC вопроса существования его ZFC-доказательства. Как я понимаю, это бы противоречило Вашему утверждению?

Не противоречило бы. Со временем может быть разработана и получить всеобщее доверие более сильная теория, чем ZFC. В рамках этой теории может рассматриваться вопрос: "существует ли в ZFC доказательство высказывания A?". И ответом на этот вопрос может оказаться "не существует". И так как мы верим этой сильной теории, мы будем считать, что доказательство действительно не существует. Хотя в самой ZFC этот вопрос был неразрешим.

Речь ведь была об утверждении, высказанном в рамках некой теории. Т.е. это её теорема, обоснованная выводом из её аксиом. "Более сильная теория" - это уже подмена точки зрения.

nikov писал(а):

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

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

nikov писал(а):

epros писал(а):

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

Чтобы доказать $G$, Гёдель использовал дополнительно аксиому о корректности арифметики Пеано (если быть точным, в языке арифметики это будет схема аксиом), которая выглядит как $\mathrm{Prf}_{\mathrm{PA}}(\Phi)\rightarrow\Phi$.

Конечно же, в самой теории не может быть такой схемы аксиом. Но, принимая теорию, мы автоматически принимаем и это.

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

Здесь существенна не схема аксиом, построенных с помощью Гёделевской нумерации внутри самой теории (что, конечно же, сложно), а простое утверждение внутри мета-теории (и на её языке, без всякой арифметизации):
$(\forall S \in T)((T \vdash S) \to S)$
Это утверждение читается как: "Теория $T$ доказывает только истинные утверждения" и означает состоятельность теории, что под силу понять и школьнику.