blob: 1dffb6bf9d0bfbd33a5a5f2c54105526f7a18759 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
[ A -> B |- ~ B -> ~ A ]
------------------------------ Implication strategy
[ A -> B , ~ B |- ~ A ]
------------------------------ Negation rewrite
[ A -> B , ~ B |- A -> _|_ ]
------------------------------ Implication strategy
[ A , A -> B , ~ B |- _|_ ]
------------------------------ Modus ponens
[ A , A -> B , B , ~ B |- _|_ ]
------------------------------ Forgetting
[ B , ~ B |- _|_ ]
------------------------------ Ex falso quodlibet _|_
Ø
|
