Выводы в исчислении высказываний
Введение
В документе собраны выводов формул в исчислении высказываний с двумя связками (импликация, отрицание) и правилом вывода modus ponens. В отличии от базы MetaMath, каждый вывод самодостаточен и не ссылается на другие выводы. Не используется также теорема дедукции. Данная подборка создана для изучения взаимосвязий формул исчисления и проверки различных систем аксиом, которые получаются перебором моделей. Все выводы найдены при помощи онлайновой системы поиска вывода. Ниже приведен пример вывода формулы P→P:
0. | ax | F1 | P→(Q→P) | |||
1. | ax | F2 | (P→(Q→R))→((P→Q→(P→R)) | |||
2. | mp | 0,1 | (P→Q)→(P→P) | |||
3. | mp | 0,2 | I | P→P |
В первой колонке идёт номер формулы вывода. Во второй - способ вывода: ax - "аксиомы", mp i j - правило modus ponens. Это правило: P, P→Q => Q применяется к формулам i,j, причем i - это всегда P, а j - это P→Q. Например, выше, для выполнения mp 0,1, необходимо унифицировать формулу 0: P→(Q→P) и посылку P→(Q→R) корневой импликации формулы 1. Для этого в ней делается подстановка P вместо R (это всё схемы аксиом). Более подробное описание можно найти во второй главе книги.
Выводы формул появляются при клике на линк в разделах "Перечень выводов" и "Выводы из аксиом". Выскочившее popup окошко можно закрыть ссылками "close" или "add". В последнем случае доказательство добавляется на страницу в раздел "Все выводы" (для дальнейшей печати). Выводы формул представлены также в формате metamath и графическом виде (дерево). Переключение форматов производится в заголовке popup oкна). Не все выводы пока оптимальны по длине, но со временем ситуация улучшается. :)
Аксиомы
В импликативном исчислении (без отрицания) мне известно множество кандидатов на системы полных и независимых аксиом. Из них проверены следующие (см. далее перечень всех формул):
Система из 1-й аксиомы: (L1)
Системы из 2-х аксиом: (T,PP)
(T,PA)
(PP,Q1)
(PA,Q1)
(T,Q4)
(F2,Q4)
Системы из 3-х аксиом: (F1,F2,P)
(F1,F2,A1)
(F1,T,P)
(T,C,P)
(T,P,S1)
Системы из 4-х аксиом: (T,C,I,A1) (F1,C,I3,T4)
Аналогичные системы аксиом исчисления c импликацией и отрицанием имеют вид:
Система из 1-й аксиомы: (M)
Системы из 3-х аксиом:(F1,F2,L)
(T,L2,L3)
Системы из 5-и аксиом:(F1,F2,F3,F4,F5)
Именованные формулы
Перечень выводов
Выводы из аксиом ипликативного исчисления
Эти аксиомы и формулы не содержат отрицания. Нижний индекс у формул означает длину вывода и максимальное число импликаций (самая длинная формула вывода). Для формул без ссылки вывод ещё не найден. Во второй колонке приведено число выводов (num) из данной системы аксиом. Дальше медианные средние длины вывода (len) и самой длинной по числу импликаций формулы вывода (imp). Система импликативных аксиом полна, если из них выводятся формулы (F1,F2,P).
Выводы из аксиом исчисления с отрицанием
Эти аксиомы и формулы содержат и импликацию, и отрицание. Нижний индекс означает длину вывода и максимальное число импликаций (самая длинная формула вывода). Для формул без ссылки вывод ещё не найден.