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

Введение

Рассматриваем все тавтологии логики высказываний, в которых импликация - единственная связка. Ниже перечисляются известные мне схемы полных, независимых аксиом, при помощи которых можно получить все импликативные тавтологии, пользуясь только правилом вывода modus ponens.

(F1,F2,P)

P->(Q->P); #F1;
(P->(Q->R))->((P->Q)->(P->R)); #F2;
((P->Q)->P)->P; #P;
Это базовая система аксиом. Из F1,F2 следует теорема дедукции, а из всех трёх аксиом - полнота импликативного исчисления.

(F1,T,P)

P->(Q->P); #F1;
(P->Q) -> ((Q->R)->(P->R)); #T;
((P->Q)->P)->P; #P;
Аксиому F2 в базовой системе можно заменить на транзитивность T.

(T,C,I,A1)

(P->Q) -> ((Q->R)->(P->R)); #T;
(P->(Q -> R)) -> (Q->(P->R)); #С;
P->P; #I;
(P->Q)->(((P->R)->Q)->Q); #A1;
Система из 4-х независимых аксиом. Ниже идут соответствующие выводы. При этом вывод F1 <= T,C,A1,I на самом деле не требует аксиомы T (можно доказать таблицами), но он не найден. Это самая длинная из известных система.

(T,PP)

(P->Q) -> ((Q->R)->(P->R)); #T;
P->(((Q->R)->Q)->Q); #PP;
Эта система интересна тем, что из неё все выводится достаточно быстро (на отсечении 8 импликаций).

(T,PP2)

(P->Q) -> ((Q->R)->(P->R)); #T;
((P->(Q->R))->Q)->Q; #PP2;
Выводим из них систему (T,C,I,A1)

(L1)

((P->Q)->R)->((R->P)->(S->P)); #L1;
Единственная аксиома Лукшевича

Кандидаты для проверки

(P->(Q->R)) -> ((P->Q)->(P->R)); #F2;
((P->(Q->R))->Q)->Q; #PP2;
P->(Q->P); #F1;
(P->Q)->(((Q->R)->P)->Q); #71;

P->P; #I;
((P->(Q->R))->S)->((S->Q)->Q); #199;
(P->(Q ->R))->(Q->(P->R)); #C;
((P->Q)->R)->((R->P)->P);#57;

(P->Q) -> ((Q->R)->(P->R)); #T;
((P->Q)->P)->(R->P); #14; 

F1 <= T,C,A1,I

1. ax-1     (P->Q)->((Q->R)->(P->R))
2. ax-2     (P->(Q->R))->(Q->(P->R))
3. ax-3     P->P
4. ax-4     (P->Q)->(((P->R)->Q)->Q)
5. mp(1,2)  (P->Q)->((R->P)->(R->Q))
6. mp(2,1)  ((P->(Q->R))->S)->((Q->(P->R))->S)
7. mp(3,2)  P->((P->Q)->Q)
8. mp(3,4)  ((P->Q)->P)->P
9. mp(7,1)  (((P->Q)->Q)->R)->(P->R)
10.mp(8,5)  (P->((Q->R)->Q))->(P->Q)
11.mp(10,6) ((P->Q)->(R->P))->(R->P)
12.mp(11,9) P->(Q->P)

F2 <= T,A1

1. ax-1     (P->Q)->((Q->R)->(P->R))
2. ax-2     (P->Q)->(((P->R)->Q)->Q)
3. mp(1,1)  (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(2,1)  ((((P->Q)->R)->R)->S)->((P->R)->S)
5. mp(2,3)  (P->Q)->((((Q->R)->S)->(P->R))->(P->R))
6. mp(4,3)  (P->((Q->R)->S))->((Q->S)->(P->S))
7. mp(5,6)  (((P->Q)->R)->(S->Q))->((S->P)->(S->Q)))
8. mp(7,3)  (P->(Q->R))->((P->Q)->(P->R))

P <= I,A1

1. ax-1     P->P
2. ax-2    (P->Q)->(((P->R)->Q)->Q)
3. mp(1,2) ((P->Q)->P)->P


P <= T,PP

1. ax-1    (P->Q)->((Q->R)->(P->R))
2. ax-2    P->(((Q->R)->Q)->Q)
3. mp(1,2) ((P->Q)->P)->P

 F1 <= T,PP 

1. ax-1    (P->Q)->((Q->R)->(P->R))
2. ax-2     P->(((Q->R)->Q)->Q)
3. mp(1,1) (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(1,2) ((P->Q)->P)->P
5. mp(2,1) ((((P->Q)->P)->P)->R)->(S->R)
6. mp(5,3) (P->((Q->R)->Q))->(S->(P->Q))
7. mp(6,1) ((P->(Q->R))->S)->((Q->((R->T)->R))->S)
8. mp(6,7) ((P->Q)->((P->R)->P))->(S->(T->P))
9. mp(8,4) P->(Q->P)

 F2 <= T,PP 

1. ax-1     (P->Q)->((Q->R)->(P->R))
2. ax-2      P->(((Q->R)->Q)->Q)
3. mp(1,1)  (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(1,2)  ((P->Q)->P)->P
5. mp(2,1)  ((((P->Q)->P)->P)->R)->(S->R)
6. mp(3,3)  (P->(Q->R))->((S->Q)->(P->(S->R)))
7. mp(4,3)  (P->(P->Q))->(P->Q)
8. mp(3,5)  P->((Q->(Q->R))->(Q->R))
9. mp(7,1)  ((P->Q)->R)->((P->(P->Q))->R)
10.mp(8,6)  (P->(Q->(Q->R)))->(S->(P->(Q->R)))
11.mp(10,3) (P->Q)->(R->((Q->(P->S))->(P->S)))
12.mp(6,9)  (P->(P->(Q->R)))->((S->Q)->(P->(S->R)))
13.mp(11,12)(P->(Q->(R->S)))->((R->Q)->(P->(R->S)))
14.mp(1,13) (P->(Q->R))->((P->Q)->(P->R))

 I <= T,PP 

1. ax-1     (P->Q)->((Q->R)->(P->R))
2. ax-2      P->(((Q->R)->Q)->Q)
3. mp(1,1)  (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(1,2)  ((P->Q)->P)->P
5. mp(2,1)  ((((P->Q)->P)->P)->R)->(S->R)
6. mp(4,1)  (P->Q)->(((P->R)->P)->Q)
7. mp(5,3)  (P->((Q->R)->Q))->(S->(P->Q))
8. mp(1,6)  (((P->Q)->R)->(P->Q))->((Q->S)->(P->S))
9. mp(7,3)  ((P->Q)->R)->(S->((R->P)->P))
10.mp(9,8)  (((P->Q)->Q)->R)->(Q->R)
11.mp(4,10) P->P

 PP2 <= T,PP 

1. ax-1    (P->Q)->((Q->R)->(P->R))
2. ax-2    P->(((Q->R)->Q)->Q)
3. mp(1,1) (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(1,2) ((P->Q)->P)->P
5. mp(2,1) ((((P->Q)->P)->P)->R)->(S->R)
6. mp(4,3) (P->(P->Q))->(P->Q)
7. mp(5,3) (P->((Q->R)->Q))->(S->(P->Q))
8. mp(7,1) ((P->(Q->R))->S)->((Q->((R->T)->R))->S)
9. mp(7,6) (P->((Q->R)->Q))->(P->Q)
10.mp(8,9) ((P->(Q->R))->Q)->Q

 C <= T,PP 

1. ax-1     (P->Q)->((Q->R)->(P->R))
2. ax-2      P->(((Q->R)->Q)->Q)
3. mp(1,1)  (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(1,2)  ((P->Q)->P)->P
5. mp(2,1)  ((((P->Q)->P)->P)->R)->(S->R)
6. mp(4,1)  (P->Q)->(((P->R)->P)->Q)
7. mp(3,3)  (P->(Q->R))->((S->Q)->(P->(S->R)))
8. mp(4,3)  (P->(P->Q))->(P->Q)
9. mp(5,3)  (P->((Q->R)->Q))->(S->(P->Q))
10.mp(1,6)  (((P->Q)->R)->(P->Q))->((Q->S)->(P->S))
11.mp(9,3)  ((P->Q)->R)->(S->((R->P)->P))
12.mp(9,8)  (P->((Q->R)->Q))->(P->Q)
13.mp(12,3) ((P->Q)->R)->((R->P)->P)
14.mp(11,10)(((P->Q)->Q)->R)->(Q->R)
15.mp(13,14) P->((P->Q)->Q)
16.mp(15,7) (P->(Q->R))->(Q->(P->R))

 A1 <= T,PP 

1. ax-1    (P->Q)->((Q->R)->(P->R))
2. ax-2    P->(((Q->R)->Q)->Q)
3. mp(1,1) (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(1,2) ((P->Q)->P)->P
5. mp(2,1) ((((P->Q)->P)->P)->R)->(S->R)
6. mp(4,3) (P->(P->Q))->(P->Q)
7. mp(5,3) (P->((Q->R)->Q))->(S->(P->Q))
8. mp(7,6) (P->((Q->R)->Q))->(P->Q)
9. mp(8,3) ((P->Q)->R)->((R->P)->P)
10.mp(9,3) (P->Q)->(((P->R)->Q)->Q)

 L1 <= T,PP 

1. ax-1     (P->Q)->((Q->R)->(P->R))
2. ax-2     P->(((Q->R)->Q)->Q)
3. mp(1,1)  (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(1,2)  ((P->Q)->P)->P
5. mp(2,1)  ((((P->Q)->P)->P)->R)->(S->R)
6. mp(3,3)  (P->(Q->R))->((S->Q)->(P->(S->R)))
7. mp(4,3)  (P->(P->Q))->(P->Q)
8. mp(5,3)  (P->((Q->R)->Q))->(S->(P->Q))
9. mp(7,1)  ((P->Q)->R)->((P->(P->Q))->R)
10.mp(8,3)  ((P->Q)->R)->(S->((R->P)->P))
11.mp(10,1) ((P->((Q->R)->R))->S)->(((R->T)->Q)->S)
12.mp(10,3) (P->Q)->(R->(((P->S)->Q)->Q))
13.mp(6,9)  (P->(P->(Q->R)))->((S->Q)->(P->(S->R)))
14.mp(12,13)(P->((Q->R)->S))->((Q->S)->(P->S))
15.mp(14,11)((P->Q)->R)->((R->P)->(S->P))


I <= T,PP2

1. ax-1     (P->Q)->((Q->R)->(P->R))
2. ax-2     ((P->(Q->R))->Q)->Q
3. mp(1,1)  (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(2,1)  (P->Q)->(((R->(P->S))->P)->Q)
5. mp(3,1)  (((P->Q)->R)->S)->((((Q->T)->(P->T))->R)->S)
6. mp(4,1)  ((((P->(Q->R))->Q)->S)->T)->((Q->S)->T)
7. mp(3,3)  (P->(Q->R))->((S->Q)->(P->(S->R)))
8. mp(4,4)  ((P->((Q->R)->S))->(Q->R))->(((T->(Q->U))->Q)->R)
9. mp(1,5)  (((P->Q)->(R->Q))->S)->((S->T)->((R->P)->T))
10.mp(7,1)  (((P->Q)->(R->(P->S)))->T)->((R->(Q->S))->T)
11.mp(6,3)  (P->((Q->(R->S))->R))->((R->T)->(P->T))
12.mp(8,6)  (((P->Q)->R)->(P->Q))->(((S->(P->T))->P)->Q)
13.mp(2,10) (P->(((P->(Q->R))->S)->R))->(P->(Q->R))
14.mp(11,9) (((P->Q)->((R->P)->Q))->S)->(((T->(P->U))->R)->S)
15.mp(12,9) ((((P->(Q->R))->Q)->S)->T)->((Q->(Q->S))->T)
16.mp(2,15) ((P->Q)->((P->Q)->P))->P
17.mp(14,13)(((P->Q)->((R->P)->Q))->S)->(P->S)
18.mp(16,17)P->P

A1 <= T,PP2

1. ax-1     (P->Q)->((Q->R)->(P->R))
2. ax-2     ((P->(Q->R))->Q)->Q
3. mp(1,1)  (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(2,1)  (P->Q)->(((R->(P->S))->P)->Q) 4728
5. mp(1,3)  (P->Q)->(((P->R)->S)->((Q->R)->S))
6. mp(3,1)  (((P->Q)->R)->S)->((((Q->T)->(P->T))->R)->S)
7. mp(4,1)  ((((P->(Q->R))->Q)->S)->T)->((Q->S)->T)
8. mp(5,1)  ((((P->Q)->R)->((S->Q)->R))->T)->((P->S)->T)
9. mp(2,6)  ((((P->Q)->R)->(S->R))->P)->P
10.mp(2,7)  ((P->Q)->P)->P
11.mp(7,3)  (P->((Q->(R->S))->R))->((R->T)->(P->T))
12.mp(11,2) (P->Q)->(P->Q)
13.mp(11,3) ((P->(Q->R))->S)->((Q->T)->((S->Q)->T))
14.mp(9,6)  ((((P->Q)->R)->(((S->T)->Q)->R))->S)->S
15.mp(9,8)  ((((P->Q)->(R->Q))->S)->P)->((P->Q)->(R->Q))
16.mp(10,8) ((P->Q)->P)->((P->Q)->Q)
17.mp(16,13)(P->Q)->(((((P->R)->S)->S)->P)->Q)
18.mp(14,15)((P->Q)->R)->((((P->Q)->S)->Q)->R)
19.mp(17,1) ((((((P->Q)->R)->R)->P)->S)->T)->((P->S)->T
20.mp(12,18)(((P->Q)->R)->Q)->(P->Q)
21.mp(20,19)(P->Q)->(((P->R)->Q)->Q)

C <= T,PP2

1. ax-1     (P->Q)->((Q->R)->(P->R))
2. ax-2     ((P->(Q->R))->Q)->Q
3. mp(1,1)  (((P->Q)->(R->Q))->S)->((R->P)->S)
4. mp(2,1)  (P->Q)->(((R->(P->S))->P)->Q)
5. mp(3,1)  (((P->Q)->R)->S)->((((Q->T)->(P->T))->R)->S)
6. mp(4,1)  ((((P->(Q->R))->Q)->S)->T)->((Q->S)->T)
7. mp(3,3)  (P->(Q->R))->((S->Q)->(P->(S->R)))
8. mp(1,5)  (((P->Q)->(R->Q))->S)->((S->T)->((R->P)->T))
9. mp(7,1)  (((P->Q)->(R->(P->S)))->T)->((R->(Q->S))->T)
10.mp(2,6)  ((P->Q)->P)->P
11.mp(6,3)  (P->((Q->(R->S))->R))->((R->T)->(P->T))
12.mp(2,9)  (P->(((P->(Q->R))->S)->R))->(P->(Q->R))
13.mp(10,3) (P->(P->Q))->(P->Q)
14.mp(9,6)  ((P->(Q->R))->S)->((P->(((P->(Q->R))->T)->R))->S)
15.mp(11,8) (((P->Q)->((R->P)->Q))->S)->(((T->(P->U))->R)->S)
16.mp(15,12)(((P->Q)->((R->P)->Q))->S)->(P->S)
17.mp(13,14)(P->(((P->(P->Q))->R)->Q))->(P->Q)
18.mp(17,16) P->((P->Q)->Q)
19.mp(18,7) (P->(Q->R))->(Q->(P->R))