マクロ規則（derived rules）とか定理とか
規則 MP' : A, A⊃B |- B
A A⊃B
----------[Exch]
A⊃B A
---------[MP]
B
規則 ∧の交換 : A∧B |- B∧A
A∧B
-------------------[Dup]
A∧B A∧B
----[Sel-2] ----[Sel-1]
B A
---------------[And]
B∧A
規則 Cut : A⊃B, B⊃C |- A⊃C
#1
---
A⊃B A
---------[MP]
B B⊃C
---------------[MP']
C
-------[DT #1]
A⊃C
規則 Proj-1 : A, B |- A
A B
-------[And]
A∧B
------[Sel-1]
A
規則 Proj-2 : A, B |- B （Proj-1に同じ）
規則 ∧-Dup : A |- A∧A
A
--------[Dup]
A A
--------[And]
A∧A
公式 A⊃(B⊃A)
#2 #1
--- ---
A B
---------[Proj-1]
A
-------[DT #1]
B⊃A
----------[DT #2]
A⊃(B⊃A)
規則 (A∧A)⊃B |- A⊃B
#1
---
A
----[∧-Dup]
(A∧A)⊃B A∧A
----------------[MP]
B
------[DT #1]
A⊃B
規則 (A⊃B)⊃C |- (A∧B)⊃C
#2
----
#1 A∧B
---- -----[Sel-2]
A B
--------------[Proj-2]
B
------[DT #1]
A⊃B (A⊃B)⊃C
----------------------------[MP']
C
---------[DT #2]
(A∧B)⊃C
公式 [A⊃(B⊃C)]⊃[(A⊃B)⊃(A⊃C)] （ A⊃(B⊃C) |- (A⊃B)⊃(A⊃C) で示す。）
#1
---
#2 A⊃(B⊃C) A
------ -----------------[MP]
A⊃B B⊃C
-------------------[Cut]
A⊃C
------------[DT #1]
A⊃(A⊃C)
---------[Th] ----------[a derived rule]
A⊃(A∧A) (A∧A)⊃C
-------------------------[Cut]
A⊃C
---------------[DT #2]
(A⊃B)⊃(A⊃C)
↑いくらなんでも長すぎないか、これ？
