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

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

Я добавил раздел об обосновании системы аксиом.

Глава 1. Введение в основания математики на основе логики первого порядка.

1.1
Что такое математика.
Формализация математических доказательств.
Логический вывод одних утверждений из других.
Определение математических понятий аксиомами.
Определение математической теории системой аксиом.
Строгость доказательства и логический вывод из аксиом.
Неопределяемые и определяемые понятия.
Математические определения и аксиомы определения.
Неполнота "определения" неопределяемых понятий системой аксиом.
Обоснование системы аксиом.
Аксиомы и схемы аксиом.
Методы доказательства и их обоснование.
Логика первого порядка.
Роль теории множеств в основаниях математики.
Математическая логика и вопросы непротиворечивости и полноты математических теорий.
Обоснование системы аксиом.

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

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

Математические доказательства основаны на логике, которая позволяет выводить одни утверждения из других.
Основное правило логического вывода называется Modus ponens, оно позволяет вывести истинность некоторого утверждения $\beta$ из истинности двух других утверждений $\alpha$ и "если $\alpha$, то $\beta$".
Примером применения правила Modus ponens является вывод утверждения:
"число 1001001 делится на 3" из утверждений: "сумма цифр числа 1001001 делится на 3" и "если сумма цифр числа 1001001 делится на 3, то число 1001001 делится на 3".
Правило Modus ponens применяют один или более раз, до тех пор, пока ни будет получено доказываемое утверждение.
Поскольку доказательство опирается на уже известные истины, то первоначальные истины доказать невозможно.
Утверждения, принимаемые за истину без доказательства, называются аксиомами.

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

Например, стандартная теория арифметики определяется аксиомами Пеано, евклидова геометрия - аксиомами Евклида, а стандартная теория множеств - аксиомами Цермело-Френкеля.
Определение любой математической теории состоит из определения её понятий, которое даётся в форме аксиом.

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

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

Любое математическое определение порождает аксиому, которая является утверждением, верным "по определению".
Аксиомы, порождаемые математическими определениями, называются аксиомами определения.

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

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

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

В математике есть стандартная логическая система, которая называется логикой первого порядка.
В этом введении мы выбрали логику первого порядка в качестве базовой логики.
Логика первого порядка может показаться необычной начинающему из-за короткой формы записи утверждений в этой логике.
Например, утверждение "для любого x: x=x" можно записать в короткой форме "x=x".
В логике первого порядка есть два правила вывода: Modus ponens и правило обобщения, которое позволяет из короткой формы утверждения получить более длинную.
Например, используя правило обобщения, можно из утверждения "x=x" получить утверждение: "для любого x: x=x".

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

Изучением логики первого порядка и других формальных логических систем занимается особый раздел математики, который называется математической логикой.
Математическая логика также изучает вопросы непротиворечивости и полноты математических теорий.
Система аксиом математической теории (и сама теория) нызывается противоречивой, если в ней можно доказать некоторое утверждение $\alpha$ и его отрицание "не $\alpha$".
Система аксиом математической теории (и сама теория) называется полной, если любое утверждение теории можно или доказать или опровергнуть.
В идеале, система аксиом математической теории должна быть непротиворечивой и полной, но этот идеал недостижим.
Если теория достаточна для того, чтобы в ней можно было определить арифметику, то такая теория не является полной и утверждение о непротиворечивости теории невозможно доказать в рамках этой теории.
Это следует из двух теорем австрийского математика Курта Гёделя, которые были опубликованы в 1931 году.
Неполнота математической теории объясняется неполнотой "определения" её неопределяемых понятий системой аксиом.
Утверждение о непротиворечивости теории можно перевести на язык арифметики, и, в таком виде, оно не следует из аксиом теории.
Это не значит, что нельзя доказать непротиворечивость арифметики никаким способом.
Доказательства непротиворечивости арифметики имеются в теории множеств.

Система аксиом математической теории не нуждается в доказательстве, но это не значит, что она не нуждается в обосновании.
Целью такого обоснования является ответ на три вопроса:
1) выполняются ли аксиомы для понятий, которые мы имеем ввиду
2) достаточно ли хорошо аксиомы определяют эти понятия
3) непротиворечива ли система аксиом
Иногда, к существующей теории присоединяют аксиому, которая может казаться парадоксальной, и доказывают, что полученная теория непротиворчива, если непротиворечива первоначальная теория.
Классическим примером этого является неевклидова геометрия.
В этом случае система аксиом определяет непривычные для нас понятия, с которыми у нас нет непосредственного опыта.
Тем не менее такая теория может оказаться полезной, и мы можем даже впоследствии столкнуться с непривычной реальностью, которую эта теория определяет.
Мы не будем вдаваться в обширную тему обоснования аксиом, заметим только, что новые аксиомы принимаются нечасто и после всестороннего обсуждения.

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

Я внёс исправления в раздел об обосновании системы аксиом:

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

[grizzly]

Насколько серьёзны могут быть альтернативы к аксиоматическим подходам? Поверхностное ознакомление с т.н. "генетическими" построениями теорий особого уважения не вызвали. но может я их недооценил по невежеству? это вообще может называться математикой или нет?
Ещё было бы любопытно узнать, в чём принципиальное отличие (в рамках обсуждаемого) "неаксиоматической теории топологических пространств" (УДК 515.122.3), раз уж таковая имеется.
(Если честно, последний вопрос порождён праздным любопытством; мотивации самому разбираться в этой теории недостаточно, но вдруг кто-то может без усилий поделиться уже готовым мнением.)

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

Я понятия об этом не имею.
Что такое "неаксиоматическая теория топологических пространств" и где об этом пишется?

[grizzly]

Я лучше сниму оба вопроса. Это я не туда полез, сорри (вопросы задавал по памяти прошлых лет, не потрудившись обновить понимание).

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

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

Меня не удовлетворяет последняя версия введения.
Например, меня не удовлетворяет определение:

Цитата:

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

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

[Someone]

Феликс Шмидель в сообщении #951173 писал(а):

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

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

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

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

Someone в сообщении #951179 писал(а):

Думаю, что, приложив определённые (и немалые) усилия, доказательство Евклида можно "допилить" до строгого.

Что значит, думаю? Какие в этом могут быть сомнения?

[Xaositect]

Someone в сообщении #951179 писал(а):

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

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

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

Даже если не знать, что теорема Евклида формализована, совершенно ясно, что это можно сделать.
Я хотел написать, что убедительность доказательства зависит от его смысла, а возможность формализации от его формы.
Но в случае теоремы Евклида это не так.
Бурбаки пишут в "Теории Множеств":

Цитата:

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

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

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

Может можно написать так:

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

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

Я решил нумеровать версии введения. Следующая версия: 10.

Версия 10.

Глава 1. Введение в основания математики.

1.1
Что такое математика.
Доказательство и строгое доказательство.
Формализация математических доказательств.
Логический вывод одних утверждений из других.
Аксиомы и аксиоматические теории.
Первоначальные и определяемые понятия.
Математические определения и аксиомы определения.
Определение математических понятий аксиомами.
Определение математической теории системой аксиом.
Аксиомы и схемы аксиом.
Методы доказательства и их обоснование.
Логика первого порядка.
Роль теории множеств в основаниях математики.
Математическая логика и вопросы непротиворечивости и полноты математических теорий.
Неполнота определения первоначальных понятий системой аксиом.
Доказательства непротиворечивости арифметики.
Обоснование системы аксиом.

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

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

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

Хорошо об этом сказали Бурбаки ("Теория Множеств"):

Цитата:

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

Возможность формализации математических доказательств появилась только в 20-м веке после работ Гильберта, создания формальных математических языков и развития компьютерной техники.
До этого математические доказательства не были формальными, тем не менее, они были вполне убедительными.
Евклидово доказательство бесконечности последовательности простых чисел, данное более 2000 лет тому назад, убедительно и сегодня.
Но за два века до Евклида, древнегреческий философ Зенон убедительно показал, что Аххилес никогда не догонит черепаху, и что движения вообще не существует.
Эти и другие парадоксы показали, что не всегда можно полагаться на убедительность рассуждений и привели к идее проверки формы доказательства вне связи с его смыслом.

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

Математические доказательства основаны на логике, которая позволяет выводить одни утверждения из других.
Основное правило логического вывода называется Modus ponens, оно позволяет вывести истинность некоторого утверждения $\beta$ из истинности двух других утверждений $\alpha$ и "если $\alpha$, то $\beta$".
Примером применения правила Modus ponens является вывод утверждения:
"число 1001001 делится на 3" из утверждений: "сумма цифр числа 1001001 делится на 3" и "если сумма цифр числа 1001001 делится на 3, то число 1001001 делится на 3".
Правило Modus ponens применяют один или более раз, до тех пор, пока ни будет получено доказываемое утверждение.
Поскольку доказательство опирается на уже известные истины, то первоначальные истины доказать невозможно.

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

Основанные на аксиомах математические теории называются аксиоматическими.
Первая аксиоматическая теория - геометрия Евклида - появилась в древней Греции.
В конце 19-го века, Гильберт усовершенствовал геометрию Евклида, но аксиоматический метод при этом не изменился.
Гильберт создал формальный метод построения аксиоматических теорий.

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

Первоначальные понятия принято называть "неопределяемыми", а непервоначальные - "определяемыми".
Дело в том, что обычные математические определения определяют непервоначальные понятия.
Аксиоматическое определение первоначальных понятий это особый вид определения.

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

Таким образом, аксиомы являются определением вводимых понятий и аксиоматических теорий в целом.
Например, стандартная теория арифметики определяется аксиомами Пеано, евклидова геометрия - аксиомами Евклида, а стандартная теория множеств - аксиомами Цермело-Френкеля.

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

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

В математике есть стандартная логическая система, которая называется логикой первого порядка.
В этом введении мы выбрали логику первого порядка в качестве базовой логики.
Логика первого порядка может показаться необычной начинающему из-за короткой формы записи утверждений в этой логике.
Например, утверждение "для любого x: x=x" можно записать в короткой форме "x=x".
В логике первого порядка есть два правила вывода: Modus ponens и правило обобщения, которое позволяет из короткой формы утверждения получить более длинную.
Например, используя правило обобщения, можно из утверждения "x=x" получить утверждение: "для любого x: x=x".

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

Изучением логики первого порядка и других формальных логических систем занимается особый раздел математики, который называется математической логикой.
Математическая логика также изучает вопросы непротиворечивости и полноты аксиоматических теорий.
Система аксиом аксиоматической теории (и сама теория) нызывается противоречивой, если в ней можно доказать некоторое утверждение $\alpha$ и его отрицание "не $\alpha$".
Система аксиом аксиоматической теории (и сама теория) называется полной, если любое утверждение теории можно или доказать или опровергнуть.
В идеале, система аксиом аксиоматической теории должна быть непротиворечивой и полной, но этот идеал недостижим.
Если теория достаточна для того, чтобы в ней можно было определить арифметику, то такая теория не является полной и утверждение о непротиворечивости теории невозможно доказать в рамках этой теории.
Это следует из двух теорем австрийского математика Курта Гёделя, которые были опубликованы в 1931 году.

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

Хорошо об этом сказал Миша Вербицкий:

Цитата:

Формальный метод подразумевает, что никакой связи между математическим миром и миром, окружающим нас, нет вовсе.
В качестве базовых понятий и аксиом можно брать что угодно. Для того, чтоб этот метод обоснования математики считался действенным, необходимо (как минимум) доказать, что из использованного набора аксиом нельзя получить противоречия: иначе в этой теории будет верно любое утверждение.
Действительно, "импликация с ложной посылкой истинна". Это свойство системы аксиом называется непротиворечивость.
Также нужно доказать, что любое утверждение можно доказать, либо опровергнуть, исходя из аксиом.
Это свойство теории называется полнота. В противном случае формальное описание математических объектов
неадекватно их сущности, хотя это не так просто видеть.
Дело в том, что математическим объектам можно приписать реальность безотносительно к аксиомам, которые ими описываются.
Скажем, аксиомы арифметики описывают теорию чисел, науку о решении диофантовых уравнений (уравнений в целых числах).
Утверждение "полиномиальное уравнение $P(t_1, t_2, ..., t_n) = 0$ не имеет целочисленных решений $t_1, ..., t_n$ может выводиться из аксиом арифметики (аксиом Пеано), а может и не выводиться.
Во втором случае, может случиться, что уравнение имеет решения.
Может случиться и так, что из аксиом арифметики невозможно вывести ни наличия, ни отсутствия решений.
Когда в какой-то теории есть утверждение $Q$, которое нельзя вывести из аксиом, и при этом нельзя вывести из аксиом его отрицание "не $Q$" эта система аксиом называется неполной.
"Математической реальности" такая система аксиом, очевидно, неадекватна.
Действительно, предположим, что, исходя из аксиом Пеано, нельзя ни доказать, ни опровергнуть утверждение $Q$ "полиномиальное уравнение $P(t_1, t_2, ..., t_n) = 0$ не имеет целочисленных решений $t_1, ..., t_n$".
В этой ситуации уравнение $P(t_1, t_2, ..., t_n) = 0$ таки не имеет решений, ибо, если бы такое решение было, мы бы могли его подставить в уравнение, и получить теорему "Q ложно".

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

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

[Someone]

Xaositect в сообщении #951218 писал(а):

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

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

Феликс Шмидель в сообщении #951182 писал(а):

Что значит, думаю? Какие в этом могут быть сомнения?

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

[epros]

Феликс Шмидель в сообщении #951225 писал(а):

Я хотел написать, что убедительность доказательства зависит от его смысла

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

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

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

Феликс Шмидель в сообщении #951225 писал(а):

Я хотел написать, что убедительность доказательства зависит от его смысла

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

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