Есть ли строгость в математике?

[AGu]

hexamino в сообщении #232952 писал(а):

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

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

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

P.S. Простите за банальность.

P.P.S. AD, простите за невольные пересечения с Вашим сообщением, которое я увидел за несколько секунд до отправки своего.

[rishelie]

Профессор Снэйп в сообщении #232840 писал(а):

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

думаю, аксиомам ZF не противоречит следующее: автор темы не существует, все это лишь случайный глюк сервера

-- Ср авг 05, 2009 11:55:57 --

А верим мы действительно во многое, как оказалось. Например, в закон исключенного третьего или modus ponens. Впрочем, когда-то и в пятый постулат Евклида верили. А теперь предпочитают говорить ЕСЛИ. На самом же деле есть, по-видимому, некая система символики и правил, которые просты и понятны каждому a priori. Например, чаще всего не требуется разъяснять понятия символа, переобозначений или правило силлогизма (не при историках будь сказано )

[Виктор Викторов]

Уважаемый AGu!

У меня вопрос чуть в сторону. Вы написали:

AGu в сообщении #232795 писал(а):

Привожу соответствующее доказательство в арифметике Пеано: $({\text`}\,0=0\,{\text'})$.

Ваше доказательство из одной строчки (формулы). Это, по-моему, слишком длинно. Поэтому вопрос: является ли (формальным) доказательством пустой список формул?

[AGu]

Виктор Викторов в сообщении #233026 писал(а):

AGu в сообщении #232795 писал(а):

Привожу соответствующее доказательство в арифметике Пеано: $({\text`}\,0=0\,{\text'})$.

Ваше доказательство из одной строчки (формулы). Это, по-моему, слишком длинно. Поэтому вопрос: является ли (формальным) доказательством пустой список формул?

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

[Garik2]

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

[Виктор Викторов]

AGu в сообщении #233028 писал(а):

Виктор Викторов в сообщении #233026 писал(а):

AGu в сообщении #232795 писал(а):

Привожу соответствующее доказательство в арифметике Пеано: $({\text`}\,0=0\,{\text'})$.

Ваше доказательство из одной строчки (формулы). Это, по-моему, слишком длинно. Поэтому вопрос: является ли (формальным) доказательством пустой список формул?

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

Вот и я так думал, но тут высказался Клини. Страница 52 его Математической логики теорема 9 утверждает: (ii) При $m$, $p\ge0$ Если $A_1$, …, $A_m\vdash B_1$, …, $A_1$, …, $A_m\vdash B_p$ и $B_1$, …, $B_p\vdash C$, то $A_1$, …, $A_m\vdash C$.

Что получается при p = 0?

[hexamino]

AD в сообщении #233010 писал(а):

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

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

[AGu]

Виктор Викторов в сообщении #233032 писал(а):

Вот и я так думал, но тут высказался Клини. Страница 52 его Математической логики теорема 9 утверждает: (ii) При $m$, $p\ge0$ Если $A_1$, …, $A_m\vdash B_1$, …, $A_1$, …, $A_m\vdash B_p$ и $B_1$, …, $B_p\vdash C$, то $A_1$, …, $A_m\vdash C$.

Что получается при p = 0?

При $p=0$ здесь получается, что из $\vdash C$ следует $A_1,\dots,A_m\vdash C$. И это, разумеется, верно. Не вижу связи с (не)пустотой доказательств. На всякий случай: запись $\vdash C$ вовсе не означает, что $C$ имеет «пустое доказательство». Она означает, что $C$ выводится (непустым доказательством) из одних только аксиом исчисления (см. стр. 48).

[hexamino]

AGu в сообщении #233011 писал(а):

Доведение такого доказательства до абсолютно формального вида -- это творческая работа просвещенного читателя, которую авторы доказательств, разумеется, стараются облегчить, но в пределах разумного, т.е. без занудного разжевывания, граничащего с неуважением к читателю. И автор, и читатель, как правило, «верят», что неформальное описание доказательства можно превратить в формальное доказательство. Собственно, верят они не в само доказательство или его шаги, а в собственные силы -- мол, если очень захочется, все удастся полностью формализовать.

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

[AGu]

hexamino в сообщении #233041 писал(а):

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

Согласен.

[AD]

hexamino в сообщении #233034 писал(а):

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

Да, Вы правы, это приводит к катастрофе. И этим регулярно пользуются местные тролли. Но эта вера, как и понятие "собеседник", находится за пределами математики.

Да, чтобы начать строить математику, нужно сначала объяснить "правила "игры" в буковки". (кавычки стоят вот так: {(}) )

[Виктор Викторов]

AGu в сообщении #233037 писал(а):

Виктор Викторов в сообщении #233032 писал(а):

Вот и я так думал, но тут высказался Клини. Страница 52 его Математической логики теорема 9 утверждает: (ii) При $m$, $p\ge0$ Если $A_1$, …, $A_m\vdash B_1$, …, $A_1$, …, $A_m\vdash B_p$ и $B_1$, …, $B_p\vdash C$, то $A_1$, …, $A_m\vdash C$.

Что получается при p = 0?

При $p=0$ здесь получается, что из $\vdash C$ следует $A_1,\dots,A_m\vdash C$. И это, разумеется, верно. Не вижу связи с (не)пустотой доказательств. На всякий случай: запись $\vdash C$ вовсе не означает, что $C$ имеет «пустое доказательство». Она означает, что $C$ выводится (непустым доказательством) из одних только аксиом исчисления (см. стр. 48).

Так-то оно так, но также и $A_1$ …, $A_m\vdash $, $\vdash C$ и, следовательно, $A_1$, …, $A_m\vdash C$.
С $C$ всё ясно, но чисто формально вместо $B$ после последовательности из $A$ должна идти пустота.

[rishelie]

Виктор Викторов в сообщении #233090 писал(а):

Так-то оно так, но также и $A_1$ …, $A_m\vdash $, $\vdash C$ и, следовательно, $A_1$, …, $A_m\vdash C$.
С $C$ всё ясно, но чисто формально вместо $B$ после последовательности из $A$ должна идти пустота.

нее.. если уж дословно переписывать, то тут сказано, что если $A_i$ противоречивы, $C$ истинно, то из $A_i$ выводимо $C$. По сути $A\vdash$ означает, что из $A$ выводимо все, что угодно. Это не пустота там, а все возможные высказывания.

[Профессор Снэйп]

Ради хохмы замечу, что чисто формально имеет место быть секвенция $\vdash$ (с пустыми левой и правой частями). Её доказуемость равносильна противоречивости исчисления

[AGu]

Виктор Викторов в сообщении #233090 писал(а):

AGu в сообщении #233037 писал(а):

Виктор Викторов в сообщении #233032 писал(а):

Вот и я так думал, но тут высказался Клини. Страница 52 его Математической логики теорема 9 утверждает: (ii) При $m$, $p\ge0$ Если $A_1$, …, $A_m\vdash B_1$, …, $A_1$, …, $A_m\vdash B_p$ и $B_1$, …, $B_p\vdash C$, то $A_1$, …, $A_m\vdash C$.

Что получается при p = 0?

При $p=0$ здесь получается, что из $\vdash C$ следует $A_1,\dots,A_m\vdash C$. И это, разумеется, верно. Не вижу связи с (не)пустотой доказательств. На всякий случай: запись $\vdash C$ вовсе не означает, что $C$ имеет «пустое доказательство». Она означает, что $C$ выводится (непустым доказательством) из одних только аксиом исчисления (см. стр. 48).

Так-то оно так, но также и $A_1$ …, $A_m\vdash $, $\vdash C$ и, следовательно, $A_1$, …, $A_m\vdash C$.
С $C$ всё ясно, но чисто формально вместо $B$ после последовательности из $A$ должна идти пустота.

Вы ошиблись, посчитав, что запись $A_1,\dots,A_m\vdash B_1,\ \dots,\ A_1,\dots,A_m\vdash B_p$ при $p=0$ превращается в $A_1,\dots,A_m\vdash$. На самом деле при $p=0$ эта запись превращается в пустоту (что я и написал ). Действительно, если $\varphi_1,\dots,\varphi_p$ -- набор условий $\varphi_i$ (метаформул в данном случае), то во что он превращается при $p=0$? Разумеется, в пустой набор условий. Например, Вы ведь не считаете, что список условий $x>y_1,\ \dots,\ x>y_p$ при $p=0$ превращается в $x>$ , не правда ли?