Логические исчисления, аксиомы, теоремы, гипотезы

[Xaositect]

Так я это и говорю. Обозначение $A \vDash B$ для логического следования (в любой модели $A$ истинно $B$) более общепринятое.

[grizzly]

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

$99.999\dots9$% существующих математических доказательств никогда не формализовывалось.

Здесь, наверное, прозвучит офтопом, но я попытаюсь сориентироваться в порядках. К сегодняшнему дню человечество опубликовало порядка 3 млн. математических статей (по словам С.Вольфрама -- вряд ли он ошибается в порядках); разные системы называют разные количества формализованных статей -- здесь, например, говорят о тысяче. Грубо, мы можем оценить порядок в 3 тыс. То есть, около 99.9% не формализованы.

[arseniiv]

(Оффтоп)

Спасибо Xaositect, а то я отсутствовал.

[beroal]

ZhiSe в сообщении #1232000 писал(а):

Ещё вопрос. Если я взял книгу по какой-либо математикой теории (например, по математическому анализу, теории множеств или даже по самой математической логике), и хочу, чтобы лучше понять доказательство, записывать это доказательство на формализованном языке какого-либо логического исчисления, то можно из книги понять, какое логическое исчисление в книге используется (кроме классического исчисления Д. Гильберта, в которой 10 аксиом, читал также про т.н. импликативно-негативные исчисления Ф. Фреге и Я. Лукасевича, в которых используются только логические союзы импликации и отрицания)?

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

• классическое/интуиционистское;
• теория множеств/теория типов;
• варианты аксиомы выбора.

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

Понять, какое именно формальное логическое исчисление соответствует математическому тексту на естественном языке, обычно трудно. В тексте опущены детали, и открывается простор для фантазии, для разных формализаций. Есть так называемый «естественный вывод» («natural deduction»). Он назван «естественным», потому что наиболее близко соответствует структуре неформальных логических рассуждений. По-моему, он наиболее удобен для практики. Я советую начать с него.

[beroal]

ZhiSe в сообщении #1231962 писал(а):

Также в логическом исчислении существуют определения доказуемой формулы (теоремы) и выводимой формулы (выводимости).

Наверное, вы уже заметили, что определения этих терминов подозрительно похожи. По этому вопросу есть примечание в переводе учебника Мендельсона на странице 39 (издание 1971 года). Привожу в сокращённом виде.

Цитата:

Слово «proof» употребляется в двух различных смыслах. Во-первых, оно употребляется в некотором, определенном выше, точном смысле, как название для специального вида конечных последовательностей формул теории L («вывод в L»). В другом смысле оно означает последовательность предложений английского языка (дополненного различными техническими терминами), о которой предполагается, что она служит обосновывающей аргументацией в пользу того или иного утверждения о теории L (или какой-нибудь другой формальной теории). Вообще язык, который мы изучаем (в данном случае язык L), называется языком-объектом, а язык, на котором мы формулируем и доказываем различные результаты об этом языке-объекте, называется метаязыком. … [… Дело в том, что два различных смысла слова «proof», о которых говорится в этом примечании, в русской литературе выражаются обычно с помощью двух различных терминов: «вывод» и «доказательство». Такой терминологией мы и пользуемся всюду в переводе книги. (Прим. перев.)]

Итак, «вывод» пишется на языке-объекте, «доказательство» пишется на метаязыке. Можно выбрать в качестве метаязыка и языка-объекта один и тот же язык. Метаязык и язык-объект — это роли, назначенные языкам. Да, метаязык может быть формальным (не английским, не русским), мы можем рассуждать на формальном метаязыке, несмотря на написанные в этой теме страшилки, что это страшно длинно и трудно.

Важно, что это различие между ролями языков (следовательно, также различие между терминами «вывод» и «доказательство») нужны только для теоретического исследования логики. На практике мы выбираем какой-то один удобный язык доказательств и пишем на нём, и нет смысла прыгать между языками. Я считаю выбор терминов неудачным: попробуй догадаться, какой термин соответствует какой роли языка. На мой взгляд, «вывод» и «доказательство» есть одно и то же. Я бы выбрал термины «объектный вывод» или «объектное доказательство» и «метавывод» или «метадоказательство». А в контексте, когда роль языка одна, использовал бы термин «вывод» или «доказательство».

-- Mon Jul 10, 2017 11:01:07 --

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

В любом случае - как средство лучше понять доказательство полная формализация абсолютно не пригодна. Какие-то блок-схемы, чтобы понять структуру доказательства в целом ("предположим, что $A$, из этого следует $B$ и $C$"), подробное расписывание трудных мест - да. Но не полная формализация. Это все равно, что записать программу в процессорных командах - вряд ли это поможет ее лучше понять, не правда ли?

Не раз встречал рассказ об ужасах «полной формализации», и каждый раз он ставил меня в тупик. Ситуация выглядит так. Когда кто-то спрашивает, как можно выразить какую-то теорему или доказательство более формально, обязательно появляется человечек, рассказывающий, что «полная формализация» — это плохо. Мне очевидно, что его цель — отвадить людей от формализации вообще, полной или неполной. Этот риторический приём подозрительно похож на «ложную дилемму» — или полная формализация, или никакая. А ведь никто не просил полной формализации. Просто человеку не понятно, он хочет разобраться, он хочет подробностей. Формализация — это хороший способ написать подробности. Лучший, который придуман на данный момент.

В качестве компенсации я расскажу о прелестях формализации. Лично мне формализация помогает разобраться в тёмных определениях и запутанных доказательствах. Если какое-то место в тексте мне не понятно, не понятно, «кто на ком стоял», я пытаюсь его формализовать, и нахожу или пробел в моих представлениях о предмете, или пробел в учебнике. Благодаря этому ясно, что делать дальше: повторить учебный материал, задать вопрос на форуме, искать другой учебник. Проблема приобрела чёткие очертания. Это единственная причина, ради которой я выучил логику. Ради практического применения для написания доказательств. Никто меня не заставлял ни в узах, ни в фирмах. Теория логики меня не очень интересует. Поэтому я всем, даже практикам, рекомендую выучить формальный язык логики. Язык очень прост по сравнению с любым естественным языком, например, английским или японским. Грамматики там кот наплакал. Большую часть времени займёт практическая тренировка. Чёткость мышления, которую он вырабатывает, просто поразительно выше, чем у обыденного мышления.

[Anton_Peplov]

beroal в сообщении #1232531 писал(а):

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

Кто здесь спрашивал, как можно выразить какую-то теорему или доказательство более формально? По-моему, у ТС речь шла именно о полной формализации:

ZhiSe в сообщении #1232000 писал(а):

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

beroal в сообщении #1232531 писал(а):

А ведь никто не просил полной формализации.

ТС как раз просил (см. цитату выше).

beroal в сообщении #1232531 писал(а):

Мне очевидно, что его цель — отвадить людей от формализации вообще, полной или неполной.

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

[beroal]

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

Кто здесь спрашивал, как можно выразить какую-то теорему или доказательство более формально? По-моему, у ТС речь шла именно о полной формализации:
ZhiSe в сообщении #1232000

wrote:
и хочу, чтобы лучше понять доказательство, записывать это доказательство на формализованном языке какого-либо логического исчисления

Я не вижу слова «полный» в цитате. Пусть ТС сам решает, какая формализация ему нужна.

[Anton_Peplov]

Я понял

ТС писал(а):

записывать это доказательство на формализованном языке какого-либо логического исчисления

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

[ZhiSe]

Спасибо. Разобрался. Аксиома - есть аксиома, её можно рассматривать как теорему (тогда доказательство состоит всего из одного шага), но не как гипотезу. Гипотеза - это посылка, утверждение, пока не имеющая доказательства. Например, в теории множеств - континуум-гипотеза. Их можно использовать, но тогда результаты не будут теоремами. Всякая формализованная математическая теория является расширением формализованного исчисления предикатов, её (внелогические) аксиомы добавляются к (логическим) аксиомам ФИП. Аксиом будет бесконечное множество, т.к. в ФИП аксиомы являются схемами аксиом.

beroal в сообщении #1232523 писал(а):

Понять, какое именно формальное логическое исчисление соответствует математическому тексту на естественном языке, обычно трудно. В тексте опущены детали, и открывается простор для фантазии, для разных формализаций. Есть так называемый «естественный вывод» («natural deduction»). Он назван «естественным», потому что наиболее близко соответствует структуре неформальных логических рассуждений. По-моему, он наиболее удобен для практики. Я советую начать с него.

Это вы имеете ввиду исчисление натуральной дедукции, он же метод допущений, натуральное исчисление, авторы Г. Генцен и С. Яськовский?

[grizzly]

ZhiSe в сообщении #1232563 писал(а):

Например, в теории множеств - континуум-гипотеза.

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

[beroal]

ZhiSe в сообщении #1232563 писал(а):

beroal в сообщении #1232523 писал(а):

Понять, какое именно формальное логическое исчисление соответствует математическому тексту на естественном языке, обычно трудно. В тексте опущены детали, и открывается простор для фантазии, для разных формализаций. Есть так называемый «естественный вывод» («natural deduction»). Он назван «естественным», потому что наиболее близко соответствует структуре неформальных логических рассуждений. По-моему, он наиболее удобен для практики. Я советую начать с него.

Это вы имеете ввиду исчисление натуральной дедукции, он же метод допущений, натуральное исчисление, авторы Г. Генцен и С. Яськовский?

Кажется, Генцен — автор. Видите ли, я в истории математики слаб. Тут вы знаете лучше меня. Почти вся литература, которую я читаю, на английском, поэтому эти названия мне ничего не говорят. Для определённости надо говорить о конкретных правилах вывода исчисления. К сожалению, у меня нет под рукой внятного документа. Может, вы знаете?

[arseniiv]

ZhiSe в сообщении #1232563 писал(а):

Спасибо. Разобрался. Аксиома - есть аксиома, её можно рассматривать как теорему (тогда доказательство состоит всего из одного шага), но не как гипотезу.

Как гипотезу тоже можно, просто в этом нет практического смысла.

[Someone]

ZhiSe в сообщении #1232563 писал(а):

Гипотеза - это посылка, утверждение, пока не имеющая доказательства. Например, в теории множеств - континуум-гипотеза. Их можно использовать, но тогда результаты не будут теоремами.

Ну почему же не будут? Очень даже будут. Математики — люди, как правило, аккуратные, и если я использую в доказательстве континуум-гипотезу, то я своих будущих читателей об этом предупреждаю. Выглядит это так:
Теорема ([CH]). …
А на формальном языке это будет так:
[CH]$\Rightarrow$\textellipsis

[Z1X]

ZhiSe в сообщении #1232563 писал(а):

Аксиома - есть аксиома, её можно рассматривать как теорему (тогда доказательство состоит всего из одного шага)

Чего тут рассматривать? Если исчисление уже задано, любая конкретная аксиома в нем либо является теоремой, либо нет. Известно, что в теориях первого порядка существует вывод $\dfrac {\varphi}{\varphi}$ для любой формулы $\varphi$. Поэтому в них все аксиомы можно считать теоремами, и их доказательство действительно состоит из одного шага. Однако возможны другие исчисления, где аксиомы не являются теоремами.

ZhiSe в сообщении #1232563 писал(а):

Гипотеза - это посылка, утверждение, пока не имеющая доказательства. Например, в теории множеств - континуум-гипотеза.

Открытые математические проблемы иногда в быту называют гипотезами. Но правильное понимание другое: предположим, есть правило вывода $\dfrac {\varphi_1, \ldots, \varphi_n}{\psi_1, \ldots, \psi_m}$; тогда гипотеза — это формула или схема формул $\varphi_i$ из верхнего ряда, а заключение (assertion) — $\psi_j$ из нижнего ряда.

ZhiSe в сообщении #1232563 писал(а):

Их можно использовать, но тогда результаты не будут теоремами.

В правильном литературном понимании можно использовать не их, а правила вывода, и результаты вывода из аксиом всегда будут теоремами. Скажем, в арифметике будет справедливо такое правило вывода $\dfrac {a+0=a}{a+0=a}$; здесь формула $a+0=a$ — это и аксиома, и теорема, и гипотеза, и заключение.

ZhiSe в сообщении #1232563 писал(а):

в ФИП аксиомы являются схемами аксиом.

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