Выводы в исчислении высказываний



Введение

В документе собраны 357 выводов формул в исчислении высказываний с двумя связками (импликация, отрицание) и правилом вывода modus ponens. В отличии от базы MetaMath, каждый вывод самодостаточен и не ссылается на другие выводы. Не используется также теорема дедукции. Данная подборка создана для изучения взаимосвязий формул исчисления и проверки различных систем аксиом, которые получаются перебором моделей. Все выводы найдены при помощи онлайновой системы поиска вывода. Ниже приведен пример вывода формулы P→P:

0. ax F1P→(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
I F1 2 F1 F2

В первой колонке идёт номер формулы вывода. Во второй - способ вывода: 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)


Именованные формулы

P->(Q->P);#F1; // Из системы Фреге (F1-F5)
(P->(Q->R))->((P->Q)->(P->R));#F2; // Часто встречается в системах аксиом
(P->Q)->((Q->R)->(P->R));#T; // Транзитивность импликации
(P->(Q->R))->(Q->(P->R));#C; // Перестановка посылок
(P->Q)->((R->P)->(R->Q));#TC; // Комбинация (T) и (C)
((P->Q)->P)->P;#P; // Закон Пирса
P->(((Q->R)->Q)->Q);#PP; // Удлинённый закон Пирса
((P->Q)->P)->(R->P);#PPC;
P->P;#I; // Принцип тождественности высказывания
P->(Q->Q);#PI;
(P->Q)->(P->Q);#II;
P->((P->Q)->Q);#IIC;
(P->(P->Q))->(P->Q);#I1;
P->((Q->R)->(Q->R));#PII;
(P->Q)->(((P->R)->Q)->Q);#A1; // Формулы с 2-я переменными
((P->Q)->R)->((P->R)->R);#A1C;
((P->Q)->P)->((P->Q)->Q);#A2;
P->(Q->(R->P));#T1; // Формулы с 3-я переменными
P->(Q->(R->Q));#T2;
((P->(Q->R))->Q)->Q;#T3;
((P->Q)->R)->(Q->R);#T4;
(P->Q)->(P->(R->Q));#T5;
((P->Q)->R)->((R->P)->P);#T6;
P->((Q->R)->((P->Q)->R));#T7;
(P->Q)->(((P->R)->P)->Q);#T8;
(P->((Q->R)->Q))->(P->Q);#T9;
((P->Q)->(R->P))->(R->P);#T10;
(((P->Q)->(R->Q))->S)->((R->P)->S);#Q1; // Формулы с 4-я переменными
(P->(Q->R))->((S->Q)->(P->(S->R)));#Q2;
(P->((Q->R)->Q))->(S->(P->Q));#Q3;
((P->Q)->R)->(S->((R->P)->P));#Q4;
((((P->Q)->P)->P)->R)->(S->R);#Q5;
(P->((Q->R)->Q))->((Q->S)->(P->S));#Q6;
(((P->Q)->(R->Q))->(Q->S))->(T->(Q->S));#P1; // Формулы с 5-ю переменными
(P->((Q->(R->S))->R))->((R->T)->(P->T));#P2;
((P->(Q->R))->S)->((Q->T)->((S->Q)->T));#P3;
((P->Q)->R)->((R->P)->(S->P));#L1; // Единственная импликативная аксиома Лукашевича
(P->Q)->(!Q->!P);#F3; // Из системы Фреге (F1-F5)
!!P->P;#F4; // Из системы Фреге (F1-F5)
P->!!P;#F5; // Из системы Фреге (F1-F5)
(!P->!Q)->(Q->P);#L; // Из системы Лукашевича (F1,F2,L)
P->(!P->Q);#L2; // Из системы Лукашевича (T,L1,L2)
(!P->P)->P;#L3; // Из системы Лукашевича (T,L1,L2)
!!P->(Q->P);#N1;
P->(!Q->!(P->Q));#N2; // Нужна для доказательства теоремы о полноте
(!P->Q)->(!Q->P);#N3; // Коммутативность дизъюнкции
!(P->!Q)->P;#N4; // P&Q->P
P->(Q->!(P->!Q));#N5; // P,Q->P&Q
!(P->!Q)->!(Q->!P);#N6; // Коммутативность конъюнкции
!P->(P->Q);#L2C; // Применение к L2 перестановки C
((((P->Q)->(!R->!S))->R)->T)->((T->P)->(S->P));#M; // Единственная аксиома Мердита

Перечень выводов

F1<=(L1) (M) (T,PP) (PP,Q1) (T,Q4) (F2,Q4) (T,T3) (T3,Q1) (T,C,P) (T,P,T1) (T,C,I,A1) (T,C,I,A1C) (T,L2,L3)
F2<=(T,PP) (T,PP) (T,T3) (T,A1) (T3,Q1) (PP,Q1) (T,Q4) (F1,T,P) (T,C,P) (T,P,T1) (F1,C,T7,T8)
P<=(L1) (M) (PP) (T,PP) (I,A1) (F1,A1) (T,Q4) (T,T3) (F2,Q4) (T3,Q1) (F1,F2,L) (F1,F2,L) (F1,C,T8)
T<=(L1) (F1,F2) (F1,F2) (F1,F2) (T3,Q1) (PP,Q1) (PP,Q1) (C,T7)
C<=(L1) (PP,Q1) (T,PP) (T,T3) (T3,Q1) (F1,F2) (F1,F2) (F1,F2) (T,Q4) (F1,T,P) (T,P,T1)
TC<=(T,C) (F1,F2) (F1,F2) (T,PP) (T,T3) (T,Q4) (C,T7) (T3,Q1) (PP,Q1) (F1,T,P)
PP<=(L1) (M) (F1,P) (F1,A1) (T,T3) (T,Q4) (F2,Q4) (T3,Q1) (F1,C,T8) (F1,F2,L) (F1,F2,L) (T,C,P) (T,P,T1) (T,C,I,A1)
T3<=(L1) (M) (T,PP) (T,Q4) (F2,Q4) (PP,Q1) (F1,T,P) (T,C,P) (T,P,T1) (F1,F2,P) (F1,F2,A1) (F1,F2,L) (F1,F2,L) (F1,C,T7,T8) (T,C,I,A1)
PPC<=(L1) (M) (T,PP) (F1,T8) (T,T3) (T,Q4) (F2,Q4) (T3,Q1) (PP,Q1) (F1,F2,P) (F1,T,P) (F1,F2,L) (F1,F2,L) (T,C,I,A1)
PI<=(L1) (M) (F1,F2) (F1,C) (F2,Q4) (T,PP) (T,T3) (T,Q4) (T3,Q1) (PP,Q1) (F1,T,P) (T,C,I,A1)
I<=(L1) (M) (F1,F2) (F1,C) (F1,A1) (T,Q4) (F2,Q4) (T,PP) (T,T3) (C,PP) (T3,Q1) (PP,Q1) (F1,T,P) (T,C,P) (T,P,T1)
I1<=(L1) (M) (F1,F2) (F2,A1) (T,PP) (T,P) (T,T3) (T,Q4) (F2,Q4) (T3,Q1) (C,I,A1) (F1,C,T7,T8)
T9<=(L1) (T3,Q1) (PP,Q1) (F1,F2,L) (F1,F2,L) (T,Q4) (F2,Q4) (T,PP) (T,T3) (F1,F2,P) (F1,T,P) (T,C,I,A1) (F1,C,T7,T8)
T5<=(L1) (F1,F2) (T,PP) (T,T3) (T,Q4) (T3,Q1) (PP,Q1) (F2,Q4) (F1,C,T7) (T,C,P) (T,P,T1) (F1,T,P) (T,C,I,A1)
T7<=(L1) (F1,F2) (F1,F2) (T,C) (T,PP) (T,T3) (T,Q4) (T3,Q1) (PP,Q1) (F1,T,P) (T,C,I) (T,P,T1)
A1<=(L1) (T,PP) (T,Q4) (F2,Q4) (PP,Q1) (T,T3) (T3,Q1) (F1,T,P) (T,C,P) (T,P,T1) (F1,F2,L) (F1,C,T7,T8)
A1C<=(L1) (L1) (C,A1) (T,PP) (T,Q4) (F2,Q4) (T,T3) (T3,Q1) (PP,Q1) (F1,T,P) (T,C,P) (T,P,T1) (F1,F2,L) (F1,C,T7,T8)
T1<=(L1) (M) (F1,F2) (F1,T) (F1,C) (T,PP) (T,Q4) (T,T3) (T3,Q1) (PP,Q1) (T,C,P) (T,C,I,A1)
T2<=(L1) (M) (F1) (T,PP) (T,T3) (T3,Q1) (PP,Q1) (F2,Q4) (T,C,I,A1) (T,Q4)
IIC<=(L1) (F1,F2) (F1,F2) (F2,Q4) (F1,C) (C,I) (T,T3) (T3,Q1) (PP,Q1) (F1,T,P) (T,PP) (T,Q4)
II<=(L1) (T,Q4) (T,T3) (T3,Q1) (PP,Q1)
T10<=(L1) (T,PP) (T,Q4) (T,T3) (T3,Q1) (PP,Q1) (F2,Q4) (F1,F2,P) (F1,T,P) (F1,F2,L) (F1,F2,L) (T,C,I,A1) (F1,C,T7,T8)
T8<=(L1) (T,P) (T,PP) (T,T3) (T,Q4) (T3,Q1) (PP,Q1) (F1,F2,P) (T,I,A1) (F1,F2,L) (F1,F2,L)
Q1<=(L1) (T) (F1,F2) (F1,F2) (F1,C,T7,T8)
Q2<=(T) (Q1) (F1,F2) (C,T7)
Q3<=(L1) (T,PP) (T,T3) (T,Q4) (T3,Q1) (PP,Q1) (F1,F2,P) (F1,T,P) (F1,F2,L) (F1,F2,L) (F1,C,T7,T8) (T,C,I,A1)
Q4<=(L1) (T,PP) (T,T3) (T3,Q1) (PP,Q1) (F1,F2,P) (F1,T,P) (T,C,I,A1) (F1,F2,L) (F1,C,T7,T8)
Q5<=(L1) (M) (T,T3) (T,Q4) (T3,Q1) (PP,Q1) (F1,F2,P) (F1,T,P) (F1,F2,L) (F1,F2,L) (T,C,I,A1) (F1,C,T7,T8)
Q6<=(F1,F2,L)
P1<=(L1) (M)
P2<=(F1,F2,L)
L1<=(T,PP) (T,Q4) (T,T3) (T3,Q1) (PP,Q1) (F1,F2,P) (T,C,P) (F1,T,P) (T,P,T1) (F1,F2,A1) (F1,F2,L) (T,C,I,A1) (F1,C,T7,T8)
F3<=(F1,F2,L) (F1,F2,L)
F4<=(M) (F1,F2,L) (T,L2,L3)
F5<=(M) (F1,F2,L) (F1,F2,L)
L<=(T,L2,L3)
L2<=(M) (F1,F2,L) (F1,F2,L)
L3<=(M) (F1,F2,L)
N3<=(F1,F2,L)
L2C<=(M) (F1,F2,L)
N1<=(M) (F1,F2,L)
N2<=(F1,F2,L)
N5<=(F1,F2,L) (F1,F2,L)

Выводы из аксиом ипликативного исчисления

Эти аксиомы и формулы не содержат отрицания. Нижний индекс у формул означает длину вывода и максимальное число импликаций (самая длинная формула вывода). Для формул без ссылки вывод ещё не найден. Во второй колонке приведено число выводов (num) из данной системы аксиом. Дальше медианные средние длины вывода (len) и самой длинной по числу импликаций формулы вывода (imp). Система импликативных аксиом полна, если из них выводятся формулы (F1,F2,P).

axiomsnumlenimp
(L1)273110=>F1 7,11; P 20,10; T 37,10; C 51,10; PP 20,10; T3 25,10; PPC 5,11; PI 12,8; I 7,11; I1 31,10; T9 39,10; T5 41,9; T7 56,10; A1 47,9; A1C 47,10; A1C 60,9; T1 9,11; T2 15,8; IIC 43,9; II 12,8; T10 24,8; T8 37,9; Q1 38,10; Q3 48,10; Q4 48,10; Q5 20,8; P1 2,8; (F2, TC, PII, A2, T4, T6, Q2, Q6, P2, P3)

(T,PP)27118=>F1 9,8; F2 12,9; F2 19,7; P 2,4; P 3,5; C 16,8; TC 15,8; T3 10,8; PPC 11,8; PI 11,8; I 11,8; I1 5,7; T5 19,8; T7 14,8; A1 10,7; A1C 15,7; T1 14,8; T2 14,8; IIC 14,8; T9 8,7; T10 16,8; T8 4,5; Q1 2,7; Q2 3,7; Q3 5,7; Q4 6,7; L1 15,8; (II, PII, A2, T4, T6, Q5, Q6, P1, P2, P3)

(T,T3)27308=>F1 35,8; F2 19,8; P 5,8; C 19,10; TC 33,8; PP 29,8; PPC 36,8; PI 29,8; I 18,10; I1 7,8; T5 30,8; T7 31,8; A1 21,9; A1C 33,8; T1 39,8; T2 38,8; IIC 35,8; II 7,8; T9 31,8; T10 42,8; T8 5,8; Q1 2,7; Q2 3,7; Q3 30,8; Q4 33,8; Q5 29,8; L1 43,8; (PII, A2, T4, T6, Q6, P1, P2, P3)

(PP,Q1)27137=>F1 9,7; F2 13,8; P 2,4; T 11,7; T 11,7; C 12,7; TC 17,7; T3 14,7; PPC 17,7; PI 16,7; I 10,7; T9 7,7; T5 19,7; T7 17,7; A1 9,7; A1C 19,7; T1 17,7; T2 16,7; IIC 15,7; II 10,7; T10 17,7; T8 12,7; Q2 2,7; Q3 13,7; Q4 14,7; Q5 12,7; L1 22,7; (I1, PII, A2, T4, T6, Q6, P1, P2, P3)

(T3,Q1)27318=>F1 35,8; F2 21,8; P 11,9; T 7,8; C 20,9; TC 32,8; PP 29,8; PPC 35,8; PI 29,8; I 19,9; I1 10,8; T9 31,8; T5 29,8; T7 32,8; A1 33,8; A1C 32,8; T1 39,8; T2 37,8; IIC 35,8; II 6,8; T10 44,8; T8 7,8; Q2 2,7; Q3 31,8; Q4 33,8; Q5 30,8; L1 42,8; (PII, A2, T4, T6, Q6, P1, P2, P3)

(T,Q4)271210=>F1 10,10; F2 13,9; P 10,9; C 17,10; TC 15,9; PP 9,9; T3 10,8; PPC 17,10; PI 12,10; I 13,10; I1 13,10; T5 15,10; T7 16,10; A1 8,8; A1C 11,10; T1 16,10; T2 13,10; IIC 11,9; II 12,10; T9 17,10; T10 14,10; T8 12,9; Q1 2,7; Q2 3,7; Q3 12,10; Q5 11,10; L1 13,10; (PII, A2, T4, T6, Q6, P1, P2, P3)

(F2,Q4)151510=>F1 25,12; P 6,7; PP 5,7; T3 26,12; PPC 15,12; PI 13,8; I 9,8; I1 8,7; T5 26,10; A1 19,11; A1C 17,12; T2 25,10; IIC 7,7; T9 6,7; T10 31,10; (T, C, TC, II, PII, A2, T1, T4, T6, T7, T8, Q1, Q2, Q3, Q5, Q6, P1, P2, P3, L1)

(F1,F2,P)31106=>T 8,9; T 9,8; T 19,6; C 10,11; C 11,8; C 16,6; TC 5,8; TC 13,6; PP 3,4; T3 14,8; PPC 6,6; PI 5,6; I 4,6; I1 10,6; T5 4,6; T7 15,8; T7 26,6; T1 5,6; T2 2,3; IIC 8,7; IIC 12,6; T9 5,6; T10 19,8; T8 9,8; Q1 10,8; Q1 16,9; Q2 16,8; Q3 8,6; Q4 16,8; Q5 8,6; L1 17,9; (II, PII, A1, A1C, A2, T4, T6, Q6, P1, P2, P3)

(F1,F2,A1)27106=>P 4,5; T 8,9; T 9,8; T 19,6; C 10,11; C 11,8; C 16,6; TC 5,8; TC 13,6; PP 5,5; T3 17,8; PI 5,6; I 4,6; I 5,5; I1 10,6; I1 4,7; T5 4,6; T7 15,8; T7 26,6; T1 5,6; T2 2,3; IIC 8,7; IIC 12,6; Q1 10,8; Q1 16,9; Q2 16,8; L1 19,8; (PPC, II, PII, A1C, A2, T4, T6, T8, T9, T10, Q3, Q4, Q5, Q6, P1, P2, P3)

(F1,T,P)2577=>F2 14,9; C 11,8; TC 12,8; PP 3,4; T3 6,6; PPC 5,5; PI 6,5; I 5,5; I1 4,7; T5 9,7; T7 11,8; A1 11,7; A1C 16,8; T1 4,5; T2 2,3; IIC 8,7; T9 9,7; T10 7,8; T8 3,5; Q1 2,7; Q2 3,7; Q3 7,7; Q4 8,7; Q5 5,6; L1 18,7; (II, PII, A2, T4, T6, Q6, P1, P2, P3)

(T,C,P)1687=>F1 10,7; F2 11,7; TC 3,5; PP 10,7; T3 7,7; I 8,7; I1 4,7; T5 12,7; T7 7,7; A1 8,7; A1C 10,7; T1 15,7; T8 3,5; Q1 2,7; Q2 3,7; L1 15,7; (PPC, PI, II, IIC, PII, A2, T2, T4, T6, T9, T10, Q3, Q4, Q5, Q6, P1, P2, P3)

(T,P,T1)1597=>F1 5,5; F2 15,8; C 12,7; PP 5,5; T3 9,7; I 7,7; I1 4,7; T5 13,7; T7 12,8; A1 12,7; A1C 19,8; T8 3,5; Q1 2,7; Q2 3,7; L1 17,8; (TC, PPC, PI, II, IIC, PII, A2, T2, T4, T6, T9, T10, Q3, Q4, Q5, Q6, P1, P2, P3)

(T,C,I,A1)2597=>F1 12,7; F2 8,8; P 3,5; TC 3,5; PP 12,7; T3 9,7; PPC 14,7; PI 11,7; I1 5,5; T5 15,7; T7 7,7; T7 6,5; A1C 3,5; T1 15,7; T2 15,7; IIC 3,5; T9 7,5; T10 9,7; T8 5,5; Q1 2,7; Q2 3,7; Q3 13,7; Q4 19,7; Q5 12,7; L1 17,7; (II, PII, A2, T4, T6, Q6, P1, P2, P3)

(F1,C,T7,T8)24106=>F2 21,7; P 6,5; T 7,7; TC 6,7; PP 5,5; T3 18,5; PPC 3,5; PI 3,5; I 4,5; I1 11,5; T5 6,5; A1 34,7; A1C 31,7; T1 4,5; T2 2,3; IIC 5,5; T9 10,5; T10 22,6; Q1 17,7; Q2 8,7; Q3 13,6; Q4 22,7; Q5 10,6; L1 21,7; (II, PII, A2, T4, T6, Q6, P1, P2, P3)


Выводы из аксиом исчисления с отрицанием

Эти аксиомы и формулы содержат и импликацию, и отрицание. Нижний индекс означает длину вывода и максимальное число импликаций (самая длинная формула вывода). Для формул без ссылки вывод ещё не найден.

axiomsnumlenimp
(M)18249=>F1 6,9; P 96,10; PP 95,10; T3 96,10; PPC 26,9; PI 6,9; I 7,9; I1 95,10; T1 10,9; T2 5,9; Q5 96,10; P1 2,9; F4 15,9; F5 27,9; L2 9,9; L3 95,10; L2C 22,9; N1 24,9; (F2, T, C, TC, II, IIC, PII, A1, A1C, A2, T4, T5, T6, T7, T8, T9, T10, Q1, Q2, Q3, Q4, Q6, P2, P3, L1, F3, L, N2, N3, N4, N5, N6)

(F1,F2,L)59197=>P 22,8; P 28,6; T 8,9; T 9,8; T 19,6; C 10,11; C 11,8; C 16,6; TC 5,8; TC 13,6; PP 24,8; PP 27,6; T3 23,8; T3 33,6; PPC 19,8; PPC 29,6; PI 5,6; I 4,6; I1 10,6; T9 25,8; T9 28,6; T5 4,6; T7 15,8; T7 26,6; A1 37,8; A1C 37,8; T1 5,6; T2 2,3; IIC 8,7; IIC 12,6; T10 32,8; T10 33,6; T8 25,8; T8 33,6; Q1 10,8; Q1 16,9; Q2 16,8; Q3 28,8; Q3 34,6; Q4 37,8; Q5 25,8; Q5 29,6; Q6 29,8; P2 30,8; L1 27,8; F3 32,8; F3 36,7; F4 9,6; F5 12,8; F5 15,6; L2 12,7; L2 17,6; L3 10,6; N3 17,8; L2C 6,6; N1 7,6; N2 33,8; N5 24,8; N5 26,7; (II, PII, A2, T4, T6, P1, P3, N4, N6, M)

(T,L2,L3)5187=>F1 20,7; Q1 2,7; Q2 3,7; F4 20,7; L 18,7; (F2, C, TC, P, PP, PPC, I, PI, II, IIC, I1, PII, A1, A1C, A2, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, Q3, Q4, Q5, Q6, P1, P2, P3, L1, F3, F5, N1, N2, N3, N4, N5, N6, L2C, M)

(F1,F2,F3,F4,F5)21106=>T 8,9; T 9,8; T 19,6; C 10,11; C 11,8; C 16,6; TC 5,8; TC 13,6; PI 5,6; I 4,6; I1 10,6; T5 4,6; T7 15,8; T7 26,6; T1 5,6; T2 2,3; IIC 8,7; IIC 12,6; Q1 10,8; Q1 16,9; Q2 16,8; (P, PP, PPC, II, PII, A1, A1C, A2, T3, T4, T6, T8, T9, T10, Q3, Q4, Q5, Q6, P1, P2, P3, L1, L, L2, L3, N1, N2, N3, N4, N5, N6, L2C, M)


Все выводы

Показать все (их много, необходимо подождать)


Участвующие в них формулы 20 и более раз

120P
111Q1
85Q2
78II
70T2
67TC
66T9
65T8
62T4
54A2
53I
52Q6
51I1
51T5
49PP
48P2
48T
48T6
43P1
43Q3
41PPC
41Q5
41P3
41PII
39(P->Q)->(((((P->R)->S)->S)->P)->Q)
39IIC
39P->((!Q->!R)->(R->Q))
38(P->(((P->Q)->R)->Q))->(P->Q)
38((((P->Q)->Q)->R)->P)->((P->Q)->Q)
37(((P->Q)->Q)->R)->(((P->Q)->P)->R)
37(((((P->Q)->R)->S)->S)->(P->Q))->(P->Q)
37(P->Q)->((R->P)->((Q->S)->(R->S)))
37P->(((Q->R)->S)->(R->S))
37P->((Q->(R->S))->((Q->R)->(Q->S)))
37L2C
36(P->Q)->(((R->(P->S))->P)->Q)
36(P->(Q->(R->S)))->(P->((Q->R)->(Q->S)))
35((((P->(Q->R))->Q)->S)->T)->((Q->S)->T)
35(((P->Q)->((R->P)->Q))->(P->S))->(P->S)
35(P->P)->((Q->(P->P))->(P->P))
35(P->(Q->(R->R)))->((R->R)->(P->(R->R)))
31(P->Q)->(((P->R)->S)->((Q->R)->S))
31P->((P->Q)->(R->Q))
30(P->P)->(Q->(P->P))
29(P->Q)->(P->P)
28(P->(!Q->!R))->(P->(R->Q))
27((P->Q)->(R->P))->((P->Q)->(R->Q))
26(P->Q)->(R->(P->Q))
25P->((((Q->R)->(S->R))->S)->S)
25((P->Q)->(Q->R))->(S->(Q->R))
24((P->(Q->R))->(S->Q))->(T->(S->Q))
23Q4
23((P->(Q->R))->Q)->(S->Q)
22P->((Q->R)->(R->(Q->R)))
22(((P->Q)->(Q->(P->Q)))->R)->(S->R)
22P->(((Q->(R->Q))->R)->(S->R))
22((((P->(Q->P))->Q)->(R->Q))->S)->(T->S)
22P->((Q->R)->(S->(Q->R)))
22((P->Q)->(R->(Q->S)))->(T->(R->(Q->S)))
22P->(Q->(R->R))
22((P->(Q->P))->R)->R
22((((P->Q)->P)->P)->R)->R
22(((P->Q)->Q)->(Q->R))->(Q->R)
21(P->Q)->(((((P->R)->S)->(T->S))->P)->Q)
20P->(((Q->((R->S)->S))->(S->T))->(S->T))
20F1
20PI
20((P->Q)->P)->((P->Q)->(R->Q))
20(!P->P)->(!P->Q)