Логика и методология математики.

[Феликс Шмидель]

Да, конечно, f_n(x) и есть вычислимые функции, а F(x) - невычислима. Если взять вместо текстов Т_n программы, которые дают натуральные числа на каждом шаге исполнения программы, то приведённое доказательство доказывает также несуществование алгоритма, определяющего для любой такой программы, останавливается ли она или нет.

[Феликс Шмидель]

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

[Николай]

Феликс Шмидель писал(а):

Определим функцию F(x)=f_n(x)+1 и докажем, что нет программы, которая эту функцию вычисляет.
Предположим, что такая программа есть, и F(x)=f_n(x). Тогда f_n(n)=F(n)=f_n(n)+1, что невозможно.
Полученное противоречие доказывает, что такой программы нет.

Тогда простой пример - функция $ f(x)=x вычислима на упомянутой Вами машине Тьюринга очень просто. Функция $ F(x)=x+1 вычислима также просто (я даже программы смогу написать ). Или я неправильно Вас понял?

[Феликс Шмидель]

Во-первых у меня написано: "Определим функцию F(x)=f_x(x)+1 ...", а не так как вы процитировали.
Во-вторых, в определении F(x) участвует не одна функция, а все функции последовательности f_1(x), f_2(x), ...

[Николай]

О, я думал - у Вас опечатка - извините . Тогда вынужден признать, что не понимаю, как определяется функция $ F(x). Если не трудно - поясните.

[Феликс Шмидель]

Она определяется так: F(1)=f_1(1)+1, F(2)=f_2(2)+1, F(3)=f_3(3)+1 и т.д.

[Николай]

Теперь понятно. Тогда определённая таким образом $ F(x) действительно "не укладывается" в последовательность $ f_1(x),f_2(x),..., хотя её невычислимость на машине Тьюринга выглядит удивительно, т.к. для любой вычислимой $ f(x) функция $ f(x)+1 также вычислима.

[Феликс Шмидель]

Комментарий к приведённому доказательству Теоремы Гёделя.

Будем считать Т_1, Т_2, ... программами, которые, беря натуральное число на вводе, дают натуральные числа, на каждом шагу исполнения. Программы Т_{n_1}, Т_{n_2}, ... останавливаются, если на вводе их индекс, а все остальные программы зацикливаются.
Согласно терминологии теории алгоритмов, множество индексов {n_1, n_2, ... } - неразрешимо, т.е. нет алгоритма, позволяющего для любого натурального числа определить принадлежит оно этому множеству или нет.
С другой стороны, рассматриваемое множество индексов полуразрешимо, и перечислимо. Эти понятия определяются в теории алгоритмов, где доказывается, что полуразрешимость и перечислимость это эквивалентные понятия.
Заметим, что множество индексов {n_1, n_2, ...} перечислимо, но не в этом порядке (не в порядке возрастания), иначе оно было бы разрешимо.
В 1970 году, Юрий Матиясевич доказал, что любое перечислимое множество является диофантовым, т.е. элементы множества характеризуются тем, что они принадлежат решениям некоторого диофантового уравнения.
Значит утверждение о том, что "программа Т_n останавливается, если на вводе индекс n" эквивалентно некоторому арифметическому утверждению относительно n. Cреди этих утверждений есть такие, которые невозможно ни доказать, ни опровергнуть. Понятия "доказать" и "опровергнуть" арифметическое утверждение зависят от выбора системы аксиом арифметики. Предположим мы написали программу вычисления F(x). Эта программа выполняет такие программы Т_n относительно которых она найдёт "доказательство", что они останавливаются, если на вводе индекс n. Но если на самом деле они не останавливаются, то мы не сможем утверждать, что она вычисляет F(x), и не сможем придти к противоречию, доказывающему теорему Геделя. Это произойдёт, если выбрать противоречивую или нездравую систему аксиом.

[Феликс Шмидель]

C учётом этого комментария дадим доказательство теоремы Гёделя о неполноте в немного другой форме:

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

Рассмотрим программы, которые берут натуральное число на вводе и дают натуральные числа на каждом шагу исполнения. Программы либо останавливаются, давая натуральное число на выводе, либо зацикливаются. Занумеруем каким-либо способом все эти программы и обозначим их функциями f_1(x), f_2(x), ... которые они вычисляют. Каждая из этих функций определена только для тех значений x, для которых соответствующая программа останавливается, если на вводе x.
Определим функцию F(n)=f_n(n)+1, если f_n(n) определена, и F(n)=1, если f_n(n) не определена.
Поскольку функция F(n) определена для всех натуральных значений n и F(n)\ne$f_n(n), то нет программы, которая её вычисляет.
Рассмотрим последовательность утверждений вида: "f_n(n) определена"
Не существует программы, определяющей истинность или ложность каждого из этих утверждений (при n=1, 2, ...), потому что с применением такой программы алгоритм вычисления функции F(n) очевиден.
Теорема Гёделя доказана.

[Феликс Шмидель]

Идея приведённого доказательства теоремы Гёделя о неполноте состоит в том, что теорема Гёделя является простым следствием неразрешимости алгоритмической проблемы об остановке программ (halting problem).
В Википедии есть статья, где об этом говорится. В этой статье утверждается, что следствием неразрешимости проблемы остановки является ослабленная версия теоремы Гёделя, в которой вместе с условием о непротиворечивости системы аксиом фигурирует условие о здравости (soundness) этой системы.
Если система аксиом нездравая, и в ней можно доказывать ложные арифметические утверждения, то к ней относится рассуждение в конце нашего комментария к доказательству. В этом случае доказательство не проходит, и теорема не верна, потому что можно взять непротиворечивую, но нездравую систему аксиом арифметики, в которой любое утверждение можно или доказать или опровергнуть. Понятие здравости системы аксиом можно точно определить только по отношению к другой системе аксиом, принятой за эталон здравости.
В Википедии подчёркивается, что стандартное доказательство теоремы Гёделя не нуждается в условии о здравости системы аксиом, для него достаточно условия непротиворечивости. Однако, при условии включения аксиом Пеано (которое присутствует в теореме Гёделя), и выборе этих аксиом в качестве эталона здравости, непротиворечивость и здравость это эквивалентные понятия.

[Феликс Шмидель]

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

-- Сб июн 02, 2012 16:01:16 --

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

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

Это относится к любому изложению математического текста на обычном языке.
Для того, чтобы была возможность его перевода на формальный язык, он должен быть строгим.
Но, чтобы не затруднять понимание, эта строгость не должна быть чрезмерной.
Отдельные части математического текста излагаются в двух вариантах: один лучше выражает смысл, другой более строгий.

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

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

(Продолжение следует)

[Феликс Шмидель]

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

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

Можно упростить и правила обращения с аксиомными выражениями.
Подстановки вместо переменных объектов в них не нужны.

Недостатком темы является то, что в ней не обсуждается теория множеств, которая лежит в основании всей математики.

Можно было, например, сказать следующее:

В теории множеств рассматриваются произвольные коллекции объектов.
Принадлежность объекта $x$ коллекции $y$ обозначается выражением $x\in y$.
Элементом называется объект принадлежащий какой-либо коллекции.
Коллекция всех элементов $x$, обладающих свойством $\alpha$ обозначается выражением {$x|\alpha$}. Существование коллекции {$x|\alpha$} принимается за аксиому. Из этой аксиомы следует, что не любая коллекция является элементом.
Например, коллекция $A=${$x|x\not \in x$} не является элементом, иначе получается парадокс Рассела: $A\in A\Longleftrightarrow A\not \in A$.
Произвольные коллекции элементов называются классами, а классы, которые являются элементами, называются множествами.

Первоначальными понятиями в такой теории множеств являются утверждения:

I. "$x$-класс"
II. "$x\in y$"

Есть и другие варианты теории множеств, в которых все коллекции являются множествами, и понятие класса не вводится. В этих вариантах, аксиома о существовании коллекции {$x|\alpha$} имеет более сложный и менее общий вид, потому что на свойство $\alpha$ накладываются ограничения.


Такую теорию можно развить как в теорию множеств Келли-Морса, так и в теорию NFU, которая непротиворечива относительно арифметики.

Наконец, формулировка и доказательство теоремы Гедёля даны упрощённо, нестрого и неполно. В вопросе о здравости системы аксиом ошибки и полная путаница. Это понятие можно определить как семантически, так и формально и показать, что из здравости следует непротиворечивость, но не наоборот.
Недоказуемость утверждение Гёделя легко вывести из утверждения о здравости системы аксиом, но можно и из утверждения о непротиворечивости.
Для этого нужно использовать условия выводимости Гильберта-Бернайса-Лёба.
Важно показать, что утверждение "не $Prov(#(1=0))$ $\Rightarrow$ не $Prov(#G)$" является теоремой в арифметике $PA$.

Можно дать ссылки на книгу Гумина и книгу Peter Smith.

[longstreet]

Вы тут блог ведёте?

[Феликс Шмидель]

longstreet в сообщении #579904 писал(а):

Вы тут блог ведёте?

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

[longstreet]

Ну, Вы, например, понимаете, что математическая теория не обязательно должна быть аксиоматической?