Формализация логики высказываний

[damir_777]

Здравствуйте.
У меня возник такой вопрос по поводу формализации логики высказываний. Для чего нужна эта формализация? Ведь при формализации ограничиваются лишь некоторым набором аксиом, правилом вывода и знаками, которые будут участвовать в аксиомах. Например, в одной из формализаций , которую я сейчас изучаю по учебнику, ограничиваются тремя аксиомами, правило вывода Modus Ponens и двумя знаками: Отрицание и Импликация. Соответственно конъюнкция, дизъюнкция и эквивалентность выражаются через эти два знака. У меня поэтому возник вопрос, а зачем вводить такие ограничения, почему бы не использовать весь спектр знаков, пользоваться не тремя аксиомами, а множеством аксиом (тавтологий). Не получается ли , что при формализации мы проделываем лишнюю работу, выражая одни знаки через другие, подгоняя все формулы под выбранную структуру аксиом, пользуясь лишь одним правилом вывода, т.е загоняем себя в рамки. Конечно, можно создать свою формализацию, где будут использоваться все знаки и т.д., но я заметил что ограничиваются, как правило, несколькими, а все остальное выражают через них. То же с аксиомами.
Второй вопрос такой. Для того чтобы создать свою формализацию, мне нужно получается выбрать 1)Знаки ( к примеру, отрицание, конъюнкция, дизъюнкция)
2) Аксиомы (они же тавтологии), содержащие только эти знаки. 3) Правило вывода, ну к примеру, Modus Ponens ?
При выборе аксиом играет ли роль, какие именно я выберу тавтологии, или самое главное чтобы они содержали выбранные знаки?

[arseniiv]

Давайте от начала к концу. Зачем вообще нужны аксиоматические теории? Это один из способов определить множество истинных формул (в данном случае это ровно тавтологии, но в логике первого порядка ситуация становится интереснее), которое обычно бесконечное. Взяв любую формулу, было бы неплохо иметь алгоритм, определяющий её истинность (поскольку, ну знаете, не все множества разрешимы и уж тем более счётны — математика против этого ничего не имеет, а вот нам для счёта это очень полезно). Иногда он есть — в частности, в случае исчисления высказываний. И, конечно, не один, но эта тема — про вывод.

Итак, вывод. Нужно, чтобы (1) всякая выводимая формула была истинной и (2) всякая истинная формула была выводимой. Если первого ещё добиться легко и можно много где (например, можно всегда обойтись пустым множеством выводимых формул), то второе требует от выбора аксиом аккуратности. Можно взять и не включить что-нибудь важное; можно усердно добавлять и не надобавляться (но нам повезло: исчисление высказываний конечно аксиоматизируемо). Правила вывода, как диктует первое, должны как минимум выводить из истинных посылок истинные заключения. MP этому удовлетворяет, а произвольное правило — смотреть надо.

Можно жить легко и просто, если взять упомянутые вами аксиомы со связками $\to,\neg$ и добавить к ним аксиомы, определяющие другие связки через эти (можно побольше). А также взять Modus ponens и добавить к нему другие правила вывода, включающие, например, те новые связки. Так мы не уменьшим множество теорем, которое уже содержит все тавтологии, но при неудаче (аксиомы — не тавтологии, правила вывода не удовлетворяют тому, что выше) можем сделать теоремой не тавтологию. Это всё придётся показать — при том, что трёх аксиом и MP было уже вполне достаточно.

Тут есть компромисс: связки можно определить, в принципе, как сокращения. То есть, смотрим на $A\vee B$, а видим $\neg A\to B$; смотрим на $A\wedge B$, а видим $\neg(A\to\neg B)$ и т. д.. Процедура перевода легко формализуется. Новые правила вывода можно тоже сделать «сокращениями», но сокращениями уже кусков вывода (из гипотез) — они потому будут зваться производными правилами вывода. Удобные производные правила можно получить, «переведя» все аксиомы, например, системы Клини

(сюрприз внутри)

Клини как-то раз писал(а):

\begin{gather} F\to(G\to F) \\ (F\to G)\to((F\to(G\to H))\to(F\to H)) \\ F\to(G\to F\wedge G) \\ F\to F\vee G \\ F\to G\vee F \\ F\wedge G\to F \\ F\wedge G\to G \\ (F\to G)\to((H\to G)\to(F\vee H\to G)) \\ (F\to G)\to((F\to\neg G)\to\neg F) \\ \neg\neg F\to F \end{gather}

в производные правила, пользуясь и теоремой о дедукции. (Правда, сначала надо будет доказать из трёх аксиом остальные, если мы решили их не добавлять, и они станут тоже, по сути, производными правилами, но не такими удобными, какие можно получить допиливанием.) Например, из (4) можно получить правило вывода $\dfrac F{F\vee G}$. Формализация перевода вывода, использующего производные правила, в вывод, их не использующий, тоже легка. В итоге ничего нового вводить не потребовалось — только добавить правила перевода, которые никак не влияют на связь выводимости в этой системе с истинностью выводимого.

damir_777 в сообщении #1099541 писал(а):

или самое главное чтобы они содержали выбранные знаки?

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

Ну и немного ещё о том, важно ли, какие аксиомы выбирать: представьте, что формулы — это всего лишь произвольные непустые строки из двух букв A, B, и попробуйте найти какие-нибудь аксиомы и правила вывода, чтобы выводились все строки с чётным (конечно, включая ноль) числом A и не выводились с нечётным (и других нет). Это довольно просто — и алфавит маленький, и правила определения «истинности» простые.

[damir_777]

В принципе в общем понятно, но буду еще перечитывать разбираться. У меня вот пару вопросов. Вначале вы написали что неплохо было бы иметь алгоритм, определяющий истинность формулы. Я так понял определить, является ли формула тавтологией? А вот таблица истинности тоже является по-сути этим алгоритмом. Нужно просто посмотреть на последний ее столбец, на результат формулы. И если во всех строках единицы то формула истинна при любых значениях.
Второй вопрос связан с ПРОЛОГОМ. Я конечно адресую этот вопрос тем, кто знаком и работал с этим языком программирования. По-сути он решает задачу, при заданных фактах и правиле вывода, ну и также задается что нужно найти.
Получается формализация тут какрас и нужна, т.к мы в нем можем задать аксиомы, и правила вывода, и он по этой формализации будет решать задачи? Ну например, делать вывод, либо решать еще какие нибудь логические задачи. Я вот собираюсь только освоить этот язык, читал про него.

[iifat]

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

[Xaositect]

В Прологе сильно ограниченная система вывода, в отличие от аксиоматизаций исчисления предикатов или исчисления высказываний в нем используются только формулы вида $A_1 \wedge A_2 \wedge \dots \wedge A_n \to B$. Конечно, есть еще важные детали, связанные с тем, что там не высказывания, а предикаты, и что можно делать не только выводы, но и находить с помощью унификации аргументы предиката. Это позволяет делать вычисления, поэтому Пролог и является языком программирования, а не просто формальным логическим языком.

Ограниченность эта существует потому, что в такой системе выводимость проверяется быстро с помощью метода резолюций. Для полного исчисления высказываний это coNP-полная задача и решается она достаточно медленно, хотя на практике и это используется, называется SAT-решатели. Для исчисления предикатов это задача неразрешимая.

[arseniiv]

damir_777 в сообщении #1099569 писал(а):

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

Да, конечно, это ещё один алгоритм. Метод резолюций Xaositect упомянул только что. Алгоритм Тарского — для конкретного языка первого порядка (разрешимый, но тоже беда со временем). Ещё есть всякие analytic tableaux (не знаю, как они по-русски).