Доказуемость ВТФ

[ervadi]

Теорема Ферма доказуема в аксиоматике Пеано?
Или доказано, что элементарных доказательств ВТФ несуществует?

[Xaositect]

Насколько я знаю, полного анализа на эту тему еще нет. Этим занимается, в частности, Колин МакЛарти, есть его обзор (PDF) на тему того, какие именно сильные средства используются в доказательстве Уайлса и статьи (раз, два), в которых описываются слабая теория множеств и теория типов, позволяющие эти средства формализовать. До PA пока не дошло, но вроде бы консенсус в том, что скорее всего все формализуется в PA.

[ervadi]

Спасибо, почитаю!
А что у конструктивистов? Док-во Уайлса конструктивно?

[Nik_Nikols]

ervadi в сообщении #1047094 писал(а):

Теорема Ферма доказуема в аксиоматике Пеано?

Года три назад я задавал этот вопрос, точнее, два вопроса, поскольку ваш требует некоторого уточнения: http://dxdy.ru/topic60958.html. Второй из вопросов был о доказуемости ВТФ в PA для каждого фиксированного (стандартного) показателя n. Профессор Снэйп уверенно ответил "да", доказуема. Может быть, ему что-то известно?

[HisShadow]

(Оффтоп)

Профессор Снэйп умер, к сожалению :(

[Anton_Peplov]

ervadi в сообщении #1047245 писал(а):

Док-во Уайлса конструктивно?

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

Что можно назвать конструктивным доказательством гипотезы Таниямы-Шимуры? Построение алгоритма, который для любой данной эллиптической кривой строит модулярную форму и обратно?

(Оффтоп)

Кстати, вот в связи, в частности, и с теоремой Ферма мне всегда было интересно: конструктивное доказательство существования - это построение примера, а как можно конструктивно доказать несуществование? Взять хотя бы такую обыкновенную вещь, как бесконечность множества всех простых чисел. Доказательство Евклида позволяет по любому набору простых чисел построить превосходящее их простое число. Можно ли назвать это доказательство конструктивным доказательством несуществования самого большого простого числа?

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

[arseniiv]

(Оффтоп)

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

[epros]

Anton_Peplov в сообщении #1054785 писал(а):

а как можно конструктивно доказать несуществование?

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

[Anton_Peplov]

(Оффтоп)

arseniiv в сообщении #1054795 писал(а):

Есть системы вывода, где никак нельзя получить неконструктивное доказательство.

Я не о том. Когда мы договариваемся, какое доказательство считать конструктивным, а какое неконструктивным, мы тем самым выбираем и системы вывода, которые можно/нельзя использовать.
Пример не совсем про доказательства, но из области околоконструктивных исследований. Как построить конструктивный вариант понятия "множество нулевой (канонической) лебеговой меры на прямой"? В классической математике множество имеет нулевую меру, если для каждого $\varepsilon > 0$ найдется его покрытие мерой меньше $\varepsilon$. Счастье, что действительные $\varepsilon$ можно заменить рациональными, а произвольные элементы покрытия - промежутками с рациональными концами. Это позволяет алгоритму принимать и выводить данные. Можно назвать эффективно нулевым множество, для которого есть алгоритм, который по любому рациональному $\varepsilon > 0$ выдает покрытие интервалами суммарной длиной меньше $\varepsilon$. Но как быть, если в таком покрытии обязательно бесконечное число членов (как, скажем, в покрытии $\mathbb{N}$)? Можно ограничиться тем, что алгоритм для каждого $n$ выдает $n$-ный член покрытия. Такие множества называются эффективно нулевыми по Мартин-Лёфу. Можно потребовать, чтобы алгоритм для каждого рационального $\delta$ выдавал $n$ первых членов покрытия, суммарная длина которых отличается от меры всего покрытия не более чем на $\delta$. Такие множества называются эффективно нулевыми по Шнорру, и это более узкий класс. А можно вообще запретить покрытия с бесконечным числом членов, потребовав, чтобы оно было обязательно конечным. Такие множества называются эффективно нулевыми по Курцу, и это еще более узкий класс (в частности, $\mathbb{N}$ в него не входит). Вопрос, какое из определений считать "уже достаточно конструктивным", определяется личными вкусами математика. А из этого уже будет вытекать, какие теоремы останутся справедливыми в таких ограничениях.

Винни-Пух писал(а):

Вопрос в том, чему пчелы больше доверяют.

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

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

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

[Someone]

Anton_Peplov в сообщении #1054985 писал(а):

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

Доказательство несуществования проводится по схеме $(A\Rightarrow(B\wedge\neg B))\Rightarrow\neg A$. Доказательство от противного — по схеме $(\neg A\Rightarrow(B\wedge\neg B))\Rightarrow\neg\neg A$. В классической логике $\neg\neg A\Leftrightarrow A$. В интуиционистской логике из $\neg\neg A$ не следует $A$.

[Anton_Peplov]

Спасибо, Someone!

[epros]

Упс, Someone уже ответил. Но я всё же приведу свой ответ, ибо успел написать к нему развёрнутые примеры.

Anton_Peplov в сообщении #1054985 писал(а):

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

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

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

Что тут сложного? Аксиома $(p \to\perp) \to \neg p$ в конструктивном анализе действует так же, как и в классическом. Предположим, что существует максимальное натуральное число $n$. Но число $n+1$ больше, значит число $n$ -- не максимальное. Противоречие. Значит предположение о существовании максимального натурального числа опровергнуто. Ни у какой "философской интерпретации" конструктивного анализа не может быть никаких претензий к такому доказательству несуществования, потому что здесь нет снятия двойного отрицания.

А вот пример доказательства от противного. Любое действительное число либо равно нулю, либо можно отличить от нуля. Предположим, что не любое число таково. Т.е. существует действительное число $a$, которое 1) не равно нулю, но которое 2) невозможно отличить от нуля. Но из (2) следует равенство $a$ нулю (по определению равенства чисел), т.е. противоречие с (1). Значит предположение опровергнуто: Неверно отрицать, что любое действительное число либо равно нулю, либо можно отличить от нуля. До этого места у конструктивного анализа нет никаких претензий к доказательству. Но далее классический анализ снимает двойное отрицание, утверждая, что любое действительное число либо равно нулю, либо можно отличить от нуля. А вот этого уже конструктивный анализ не приемлет. На самом деле, в конструктивном анализе данное утверждение недоказуемо.

[ervadi]

То есть док-во Уайлса конструктивисты бы приняли, но до

Цитата:

Построение алгоритма, который для любой данной эллиптической кривой строит модулярную форму и обратно

еще не дошли?