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

[ZhiSe]

Добрый день,

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

$A \rightarrow (B \rightarrow A)$

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

Формула $B$ называется доказуемой, если существует конечная последовательность формул

$B_1, ..., B_t$ (1)

в которой $B_t = B$ и каждая из формул является либо аксиомой, либо получается по правилу вывода из некоторых предыдущих формул последовательности (1).

Формула $B$ называется выводимой из системы формул (посылок, гипотез)

$A_1, ..., A_t$ (2)

если существует конечная последовательность формул

$B_1, ..., B_t$ (3)

в которой $B_t = B$ и каждая из формул является либо аксиомой, либо теоремой, либо посылкой (гипотезой) из (2), либо получена по правилу вывода из предыдущих формул последовательности (3).

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

[arseniiv]

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

[ZhiSe]

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

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

Взял цитату в одной из книг:

Цитата:

Д. Гильбертом и его школой (1920 - 1930) были развиты новые методы обоснования математики, основывающиеся на построении математической теории как синтаксической теории, в которой все аксиомы записываются формулами в некотором алфавите и точно указываются правила вывода одних формул из других. Таким образом, в теорию как составная часть должна была входить математическая логика."

Здесь написано, что математическая логика входит как составная часть в другие математические теории. Можно ли сделать вывод, что какая-либо математическая теория, со своим алфавитом, аксиомами, будет содержать в себе, не только свои (внелогические) аксиомы, но и общие для всех математических теорий логические аксиомы (выбранного логического исчисления, классического, например, или какого-либо другого)?

[Anton_Peplov]

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

Можно ли сделать вывод, что какая-либо математическая теория, со своим алфавитом, аксиомами, будет содержать в себе, не только свои (внелогические) аксиомы, но и общие для всех математических теорий логические аксиомы (выбранного логического исчисления, классического, например, или какого-либо другого)?

Да, разумеется. Посмотрите, как строится арифметика Пеано (например, в книге Клини. Математическая логика). В качестве ее аксиом принимаются:
1) все аксиомы исчисления предикатов первого порядка (включая и аксиомы логики высказываний)
2) восемь собственно арифметических аксиом
3) схема аксиом, формализующая метод математической индукции.

[ZhiSe]

Все стало намного понятнее.

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

[Anton_Peplov]

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

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

Как правило, это крайне трудоемкое дело. Язык формальной теории очень беден - хотя на нем в принципе можно записать любое доказательство соответствующей неформальной теории, это такое же "в принципе", как "в принципе, можно вычерпать бассейн чайной ложкой". Попробуйте, например, записать в арифметике Пеано какую-нибудь простенькую школьную теоремку про делимость. Даже вместо $a < b$ придется писать $\exists x \ x' + a = b$. Говорят, более удобные средства формализации предоставляет теория типов и пруверы типа Coq, но я в этой области не ориентируюсь, лучше спросить у знатоков. В любом случае - как средство лучше понять доказательство полная формализация абсолютно не пригодна. Какие-то блок-схемы, чтобы понять структуру доказательства в целом ("предположим, что $A$, из этого следует $B$ и $C$"), подробное расписывание трудных мест - да. Но не полная формализация. Это все равно, что записать программу в процессорных командах - вряд ли это поможет ее лучше понять, не правда ли?

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

можно из книги понять, какое логическое исчисление в книге используется

$99.999\dots9$% существующих математических доказательств никогда не формализовывалось. Но логика в этих доказательствах применяется классическая (включающая закон исключенного третьего и т.д.) То есть и формализовывать их нужно в формальной теории, построенной на классической логике.
Если теорема доказывается в неклассической логике, об этом сообщают заранее, и таких теорем Вы нигде не встретите, кроме книг собственно по основаниям математики.

[Z1X]

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

Можно ли сделать вывод, что какая-либо математическая теория, со своим алфавитом, аксиомами, будет содержать в себе, не только свои (внелогические) аксиомы, но и общие для всех математических теорий логические аксиомы

Именно как логические аксиомы? Насколько я понимаю, нет, нельзя, это уже будут схемы аксиом.

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

В качестве ее аксиом принимаются:
1) все аксиомы исчисления предикатов первого порядка (включая и аксиомы логики высказываний)

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

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

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

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

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

Даже вместо $a < b$ придется писать $\exists x \ x' + a = b$.

Смысл использования сокращений в том, что каждый раз — не придется.

[Anton_Peplov]

Z1X в сообщении #1232008 писал(а):

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

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

[Z1X]

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

Все равно придется выписывать доказательства кучи самоочевидных фактов.

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

[Anton_Peplov]

Я называю самоочевидным, например, такой факт: в иррациональном числе как минимум две цифры встречаются после запятой бесконечное количество раз.

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

[Z1X]

Десятичная (и вообще $n$-ичная) арифметика формализуется довольно легко, но громоздко (и чем больше $n$, тем оно по понятным причинам громоздче). К математике это прямого отношения не имеет.

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

где этот факт используется.

Где, например?

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

А потом нужно записать еще и доказательство этого утверждения из аксиом ZFC. Яду мне, яду.

Я уже упоминал необходимость использования сокращений. Расшифровку этих сокращений и перевод на язык ZFC можете поручить пруфчекеру. На дворе все же не каменный век. Никто сейчас уже не будет вычерпывать ваши бассейны вручную, да еще такими неподходящими средствами.

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

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

А зачем вам доказательство-то так записывать? Один раз определите числа как кортежи (строки).

Вообще, теория систем счисления — совершенно отдельная наука. Научность здесь — ключевой тезис, ибо при желании все можно нужным образом формализовать, притом неединственным образом. Скажем, может ли произвольная строка цифр начинаться с нуля? Если да, то десятичное число — уже не строка, а множество строк. На языке ZFC там будет разный синтаксис в разных случаях. Но семантически получится одно и то же.

[arseniiv]

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

Язык формальной теории очень беден

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

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

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

Это не совсем правильная цель. Формализуется логика, чтобы можно было механически убедиться в корректности вывода. Это ортогонально человекопонятности такого формализованного вывода. Гляньте на выводы в Metamath, опять же.

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

-- Сб июл 08, 2017 00:20:14 --

(Оффтоп)

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

формальных теорий

Вообще мне лично не нравится такое словоупотребление. Уже привык к тому, что (если контекст — матлогика) теория — это замкнутое относительно логического следования множество формул, а если хочется говорить о какой-то системе вывода в целом, то так стоит и говорить: «система вывода», ибо они бывают совершенно несвязанными с логикой, но с теми же общими свойствами (скажем, таким: $(A\vdash B)\mathbin\& (B\vdash C)\Rightarrow (A\vdash C)$). Язык — также множество формул (всех рассматриваемых), всевозможные языки первого порядка и некоторые другие можно взаимно однозначно поставить в соответствие их сигнатурам — наборам внелогических символов (вместе с их свойствами), встречающихся в формулах языка. Теория аксиоматизируема множеством формул $\mathcal A$, если из него выводятся все входящие в неё — при этом безразлично, формально добавляем мы эти формулы к логическим аксиомам или рассматриваем как кучу посылок. Можно даже логические аксиомы включать в $\mathcal A$, исключив их из определения выводимости, но это будет неудобно при разговорах об аксиоматизируемости теорий — например, конечной аксиоматизируемости. И при некоторых других.

[Z1X]

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

теория — это замкнутое относительно логического следования множество формул

С чего вы так решили? Это определение теории? А если логические исчисления, на которых строится система вывода, вообще не содержат следования, а только, скажем, дизъюнкцию и отрицание, тогда эта система уже не может быть теорией?

Наверное, вы подразумевали какую-то другую замкнутость?

[Xaositect]

Z1X в сообщении #1232397 писал(а):

С чего вы так решили? Это определение теории? А если логические исчисления, на которых строится система вывода, вообще не содержат следования, а только, скажем, дизъюнкцию и отрицание, тогда эта система уже не является теорией?

Логическое следование тут - это не импликация, это $\vDash$.

[Z1X]

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

Логическое следование - это не импликация, это $\vDash$.

Но в источниках дается совсем другая информация!
https://ru.wikipedia.org/w/index.php?ti ... edirect=no

Цитата:

Не следует путать импликацию (→) и логическое следование (⇒). Импликация как логическое выражение может сама принимать значения истины или лжи. Логическое же следование A ⇒ B утверждает, что во всех случаях, когда формула A истинна, B также будет истинно.