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

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

Спасибо!
Я думаю, более подходящее название: "Логика и методология формализма в математике".

[longstreet]

Определитесь. Либо "Логика и методология формализмов в математике", подразумевая под формализмами формальные теории. Либо "Логика и методология математического формализма" подразумевая направление в основании математики.

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

Похоже, что "Методология математического формализма", наиболее отражает суть.

(Оффтоп)

Можете попросить модераторов переименовать тему.

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

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

Похоже, что "Методология математического формализма", наиболее отражает суть.

(Оффтоп)

Можете попросить модераторов переименовать тему.

Очень хорошо! Краткость - сестра таланта. )
Мне бы только хотелось отразить в названии, что это первая версия, потому что из за найденных недостатков, её придётся переписать.

Давайте поговорим ещё о математической строгости.
Синонимом этого понятия является правильность.
Неформальные доказательства могут быть правильными, но в случае сложных доказательств, это очень трудно проверить.
В настоящее время существуют формальные языки высокого уровня, например $COQ$ или $Mizar$.
В будущем, появятся более простые языки, перевод доказательств на которые будет не таким сложным делом.
Тогда строгими математическими доказательствами будут считаться только доказательства, переведённые на формальный язык.

[longstreet]

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

Давайте поговорим ещё о математической строгости.
Синонимом этого понятия является правильность.

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

-- 04.06.2012, 11:52 --

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

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

Об этом сложно говорить с уверенностью. А вдруг появится сильный искусственный интеллект? Тогда и переводить на формальный язык не придётся...

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

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

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

Давайте поговорим ещё о математической строгости.
Синонимом этого понятия является правильность.

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

А почему слово "правильность" неприменима к формальному доказательству?
Компьютер проверил его - значит оно правильно.

Я смотрел определение понятия "математической строгости" (mathematical rigor) в словарях.

Вот цитата из философского словаря:

"Как показывает история науки, понятие С. развивалось постепенно. В ходе общего прогресса науки обычно оказываются превзойденными каноны С. представлявшиеся ранее абсолютно безупречными. Так обстояло, в частности, дело с геометрией Евклида. Долгое время она являлась идеалом С., но в 19 в. Н.М. Лобачевский писал о ней: «...Никакая Математическая наука не должна бы начинаться с таких темных понятий, с каких, повторяя Евклида, начинаем мы Геометрию, и... нигде в Математике нельзя терпеть такого недостатка строгости, какой принуждены были допустить в теории параллельных линий»."

Получается, что геометрия Евклида не является строгой, а формальная геометрия Гильберта является.

Дайте своё определение математической строгости, и объясните почему оно отличается от общепринятого.

[longstreet]

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

А почему слово "правильность" неприменима к формальному доказательству?

Не устоялось. Так же как не говорят "праведное доказательство". Устоялись логические термины "истинность" и "ложность". Формальное доказательство не может быть правильным (чтобы то вообще значило)? Оно либо истинно, либо ложно. И то условно, как в логике.

Примем две аксиомы: "каждый человек может летать", "Иванов $-$ человек". Отсюда следует (можно доказать теорему), что "Иванов может летать". Этот вывод (эта теорема) истинна в том смысле, что она действительно следует из принятых аксиом. Как видите, даже термин "истинность" условен, потому что мы принимаем правила логики, по которым из ложных посылок может следовать ложный аргумент (или даже истинный). Но утверждение в рамках принятых аксиом истинно.

Вы же это знаете (раз об этом пишите). Вот и не выдумывайте.

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

Компьютер проверил его - значит оно правильно.

Не значит. (Банально: компьютер может ошибиться.) $100500$ раз обсуждалось. В наши дни компьютер научили вычислять интегралы; так зачем же их учат брать...

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

Дайте своё определение, и объясните почему оно отличается от общепринятого.

Ничем не отличается. Из общепринятого и следует, что аксиоматизация $-$ это проверка истинности.

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

Вы посмотрите на современные публикации с изложением доказательства теорем в нормальных научных журналах. Вы там не увидите спуска до самого низкого формального уровня и механического вывода. Почему? Это просто не нужно: стенки прозрачные.

-- 04.06.2012, 13:47 --

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

Получается, что геометрия Евклида не является строгой, а формальная геометрия Гильберта является.

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

У Гильберта теория строгая. Но он не опускается до самого низкого формального уровня в доказательствах. Откройте его "Основания геометрии" и посмотрите.

-- 04.06.2012, 13:51 --

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

-- 04.06.2012, 13:52 --

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

-- 04.06.2012, 13:57 --

Кстати, сам же Гильберт поставил известный список проблем. Так вот проблема №23 заключается в аксиоматизации физики.

По-вашему получается, что Гильберт считал физику неверной и чтобы сделать её верной, он считал нужным её аксиоматизировать, так что ли? Это неправильно. Он считал её верной и считал нужным аксиоматизировать.

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

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

Формальное доказательство не может быть правильным (чтобы то вообще значило)?

Примем две аксиомы: "каждый человек может летать", "Иванов $-$ человек". Отсюда следует (можно доказать теорему), что "Иванов может летать". Этот вывод (эта теорема) истинна в том смысле, что она действительно следует из принятых аксиом. Как видите, даже термин "истинность" условен, потому что мы принимаем правила логики, по которым из ложных посылок может следовать ложный аргумент (или даже истинный). Но утверждение в рамках принятых аксиом истинно.

Истиной является то, что этот вывод следует из принятых аксиом, но само доказательство того, что "Иванов может летать" не является ни истинным ни ложным. Истинным или ложным может быть утверждение, но не доказательство. Доказательство может быть правильным или неправильным.
Доказательство, которое ссылается на аксиомы - правильное, если вывод следует из аксиом. При этом вывод может быть ложным, если приняты ложные аксиомы. Например, доказательство парадокса Банаха-Тарского, основанное на аксиоме выбора является правильным. А как определить правильность доказательства этого парадокса, если оно не основывается на аксиомах?

[longstreet]

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

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

Вот именно, я так Вам и говорил:

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

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

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

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

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

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

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

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

Компьютер проверил его - значит оно правильно.

Не значит. (Банально: компьютер может ошибиться.) $100500$

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

[longstreet]

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

Есть методы которые могут сделать ошибку маловероятной.

Дело не только в ошибке. Почитайте наконец серьёзные обсуждения на эту тему. (сходу посоветовать не могу, но $100500$ раз встречал, проблема четырёх красок, Гротендик и Ко и т.д.)

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

Алгоритм проверки доказательства на языке логики первого порядка несложен.

Алгоритм вычисления интегралов ещё проще.

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

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

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

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

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

Тогда скажите, существует ли хоть одно правильное доказательство, что сумма углов треугольника равна 180 градусам?

[longstreet]

Да что ж такое!? Я же сказал, что нет ни "правильных" ни "неправильных" доказательств.

Если вопрос в том, существует ли хоть одно аксиоматическое доказательство того, что сумма углов треугольника равна $180$ градусам, то ответ: "Да, существует". Но это само по себе неинтересно (можно составить теорию, в которую это утверждение будет входить как аксиома, и что?), интересно то, выводится ли это из каких-то конкретных естественных аксиом, или нет.

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

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

Да что ж такое!? Я же сказал, что нет ни "правильных" ни "неправильных" доказательств.

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

Я Вас правильно понял?

[longstreet]

Нет. Вы упускаете кое-что.

При формальном подходе к доказательству математических теорем. Есть только истинные и ложные доказательства (и то в условном смысле, в каком? - см. выше).

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

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

Нет. Вы упускаете кое-что.

При формальном подходе к доказательству математических теорем. Есть только истинные и ложные доказательства (и то в условном смысле, в каком? - см. выше).

А при неформальном подходе, есть правильные доказательства?
Например, утверждения, что сумма углов треугольника равна 180 градусам?