2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


В этом разделе нельзя создавать новые темы.

Если Вы хотите задать новый вопрос, то не дописывайте его в существующую тему, а создайте новую в корневом разделе "Помогите решить/разобраться (М)".

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

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

Обязательно просмотрите тему Правила данного раздела, иначе Ваша тема может быть удалена или перемещена в Карантин, а Вы так и не узнаете, почему.



Начать новую тему Ответить на тему
 
 Формализация логики высказываний
Сообщение15.02.2016, 11:11 


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

 Профиль  
                  
 
 Re: Формализация логики высказываний
Сообщение15.02.2016, 12:51 
Заслуженный участник


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

Итак, вывод. Нужно, чтобы (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 и не выводились с нечётным (и других нет). Это довольно просто — и алфавит маленький, и правила определения «истинности» простые.

 Профиль  
                  
 
 Re: Формализация логики высказываний
Сообщение15.02.2016, 13:21 


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

 Профиль  
                  
 
 Re: Формализация логики высказываний
Сообщение15.02.2016, 15:27 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Формализация логики высказываний
Сообщение15.02.2016, 15:46 
Заслуженный участник
Аватара пользователя


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

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

 Профиль  
                  
 
 Re: Формализация логики высказываний
Сообщение15.02.2016, 21:36 
Заслуженный участник


27/04/09
28128
damir_777 в сообщении #1099569 писал(а):
Я так понял определить, является ли формула тавтологией? А вот таблица истинности тоже является по-сути этим алгоритмом. Нужно просто посмотреть на последний ее столбец, на результат формулы. И если во всех строках единицы то формула истинна при любых значениях.
Да, конечно, это ещё один алгоритм. Метод резолюций Xaositect упомянул только что. Алгоритм Тарского — для конкретного языка первого порядка (разрешимый, но тоже беда со временем). Ещё есть всякие analytic tableaux (не знаю, как они по-русски).

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 6 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group