Logica
Tools
for
Thought
Hilbert Proofs
Id
Premises
Goal
1
p => r
Premise
2
r => (q => r)
Implication Creation
3
(r => (q => r)) => (p => (r => (q => r)))
Implication Creation
4
p => (r => (q => r))
Implication Elimination
3
2
5
(p => (r => (q => r))) => ((p => r) => (p => (q => r)))
Implication Distribution
6
(p => r) => (p => (q => r))
Implication Elimination
5
4
7
p => (q => r)
Implication Elimination
6
1
1
(~q => ~p) => (p => q)
Implication Reversal
2
((~q => ~p) => (p => q)) => (~p => ((~q => ~p) => (p => q)))
Implication Creation
3
~p => ((~q => ~p) => (p => q))
Implication Elimination
2
1
4
(~p => ((~q => ~p) => (p => q))) => ((~p => (~q => ~p)) => (~p => (p => q)))
Implication Distribution
5
(~p => (~q => ~p)) => (~p => (p => q))
Implication Elimination
4
3
6
~p => (~q => ~p)
Implication Creation
7
~p => (p => q)
Implication Elimination
5
6
1
p => q
Premise
2
(q => r) => (p => (q => r))
Implication Creation Schema
3
(p => (q => r)) => ((p => q) => (p => r))
Implication Distribution Schema
4
(q => r) => ((p => q) => (p => r))
Transitivity
2
3
5
(p => q) => ((q => r) => (p => q))
Implication Creation Schema
6
(q => r) => (p => q)
Implication Elimination
5
1
7
(q => r) => (p => r)
Conditional Deduction
4
6
1
q => r
Premise
2
p => (q => r)
Implication Creation
1
3
(p => q) => (p => r)
Implication Distribution
2
1
p => (q => r)
Premise
2
(p => (q => r)) => (q => (p => (q => r)))
Implication Creation Schema
3
q => (p => (q => r))
Implication Elimination
2
1
4
(p => (q => r)) => ((p => q) => (p => r))
Implication Distribution Schema
5
((p => (q => r)) => ((p => q) => (p => r))) => (q => ((p => (q => r)) => ((p => q) => (p => r))))
Implication Creation Schema
6
q => ((p => (q => r)) => ((p => q) => (p => r)))
Implication Elimination
5
4
7
q => ((p => q) => (p => r))
Conditional Deduction
3
6
8
(q => ((p => q) => (p => r))) => ((q => (p => q)) => (q => (p => r)))
Implication Distribution Schema
9
(q => (p => q)) => (q => (p => r))
Implication Elimination
8
7
10
q => (p => q)
Implication Creation Schema
11
q => (p => r)
Implication Elimination
9
10
1
p => (q => r)
Premise
2
p => q
Premise
3
(p => q) => (p => r)
Implication Distribution
1
4
p => r
Implication Elimination
3
2
1
p => r
Premise
2
q => ~r
Premise
3
~~q => q
Negation Elimination Schema
4
~~q => (q => ~r)
Implication Creation
2
5
(~~q => q) => (~~q => ~r)
Implication Distribution
4
6
~~q => ~r
Implication Elimination
5
3
7
r => ~q
Implication Reversal
6
8
p => (r => ~q)
Implication Creation
7
9
(p => r) => (p => ~q)
Implication Distribution
8
10
p => ~q
Implication Elimination
9
1
1
p => q
Premise
2
p => ~q
Premise
3
p => ~p
Contradiction
1
2
4
~p
Implication Reduction
3
1
p => q
Premise
2
q => ~~q
Negation Introduction Schema
3
p => ~~q
Transitivity
1
2
4
~q => ~q
Identity Schema
5
~q => ~p
Contradiction
4
3
1
p => (q => r)
Premise
2
p => q
Premise
3
(p => (q => r)) => ((p => q) => (p => r))
Implication Distribution
4
(p => q) => (p => r)
Implication Elimination
3
1
4
p => r
Implication Elimination
4
2
1
q => r
Premise
2
(q => r) => (p => (q => r))
Implication Creation
3
p => (q => r)
Implication Elimination
2
1
4
(p => (q => r)) => ((p => q) => (p => r))
Implication Distribution
5
(p => q) => (p => r)
Implication Elimination
4
3
1
p
Premise
2
~p
Premise
3
~p => (~q => ~p)
Implication Creation
4
~q => ~p
Implication Elimination
3
2
5
(~q => ~p) => (p => q)
Implication Reversal
6
p => q
Implication Elimination
5
4
7
q
Implication Elimination
6
1
1
p => (p => p)
Implication Creation
2
p => ((p => p) => p)
Implication Creation
3
(p => ((p => p) => p)) => ((p => (p => p)) => (p => p))
Implication Distribution
4
(p => (p => p)) => (p => p)
Implication Elimination
3
2
5
p => p
Implication Elimination
4
1
1
(~q => ~p) => (p => q)
Implication Reversal
2
((~q => ~p) => (p => q)) => (~p => ((~q => ~p) => (p => q)))
Implication Creation
3
~p => ((~q => ~p) => (p => q))
Implication Elimination
2
1
4
(~p => ((~q => ~p) => (p => q))) => ((~p => (~q => ~p)) => (~p => (p => q)))
Implication Distribution
5
(~p => (~q => ~p)) => (~p => (p => q))
Implication Elimination
4
3
6
~p => (~q => ~p)
Implication Creation
7
~p => (p => q)
Implication Elimination
5
6
1
p => (p => p)
Implication Creation Schema
2
p => ((p => p) => p)
Implication Creation Schema
3
(p => ((p => p) => p)) => ((p => (p => p)) => (p => p))
Implication Distribution Schema
4
(p => (p => p)) => (p => p)
Implication Elimination
3
2
5
p => p
Implication Elimination
4
1
1
p
Premise
2
p => (q => p)
Implication Creation Schema
3
q => p
Implication Elimination
2
1
1
p => (q => r)
Premise
2
(p => (q => r)) => ((p => q) => (p => r))
Implication Distribution Schema
3
(p => q) => (p => r)
Implication Elimination
2
1
1
p => ~p
Premise
2
p => (~p => ~(p => ~p))
Inconsistency Schema
3
(p => (~p => ~(p => ~p))) => ((p => ~p) => (p => ~(p => ~p)))
Implication Distribution Schema
4
(p => ~p) => (p => ~(p => ~p))
Implication Elimination
3
2
5
p => ~(p => ~p)
Implication Elimination
4
1
6
~~(p => ~p) => ~p
Contrapositive
5
7
(p => ~p) => ~~(p => ~p)
Negation Introduction Schema
8
(p => ~p) => ~p
Transitivity
6
7
9
~p
Implication Elimination
8
1
1
~q => ~p
Premise
2
(~q => ~p) => (p => q)
Implication Reversal Schema
3
p => q
Implication Elimination
2
1
1
p
Premise
2
~p
Premise
3
~q => ~p
Implication Creation
2
4
p => q
Implication Reversal
3
5
q
Implication Elimination
4
1
1
(~q => ~p) => (p => q)
Implication Reversal Schema
2
((~q => ~p) => (p => q)) => (~p => ((~q => ~p) => (p => q)))
Implication Creation Schema
3
~p => ((~q => ~p) => (p => q))
Implication Elimination
2
1
4
(~p => ((~q => ~p) => (p => q))) => ((~p => (~q => ~p)) => (~p => (p => q)))
Implication Distribution Schema
5
(~p => (~q => ~p)) => (~p => (p => q))
Implication Elimination
4
3
6
~p => (~q => ~p)
Implication Creation Schema
7
~p => (p => q)
Implication Elimination
5
6
1
p => q
Premise
2
~q
Premise
3
~q => ~p
Contrapositive
1
4
~p
Implication Elimination
3
2
1
~~p
Premise
2
~~~~p => ~~p
Implication Creation
1
3
~p => ~~~p
Implication Reversal
2
4
~~p => p
Implication Reversal
3
5
p
Implication Elimination
4
1
1
~~p => (~~~~p => ~~p)
Implication Creation Schema
2
(~~~~p => ~~p) => (~p => ~~~p)
Implication Reversal Schema
3
~~p => (~p => ~~~p)
Transitivity
1
2
4
(~p => ~~~p) => (~~p => p)
Implication Reversal Schema
5
~~p => (~~p => p)
Transitivity
3
4
6
(~~p => (~~p => p)) => ((~~p => ~~p) => (~~p => p))
Implication Distribution Schema
7
(~~p => ~~p) => (~~p => p)
Implication Elimination
6
5
8
~~p => ~~p
Identity Schema
9
~~p => p
Implication Elimination
7
8
1
p
Premise
2
~~~p => ~p
Negation Elimination Schema
3
p => ~~p
Implication Reversal
2
4
~~p
Implication Elimination
3
1
1
~~~p => ~p
Negation Elimination Schema
2
(~~~p => ~p) => (p => ~~p)
Implication Reversal Schema
3
p => ~~p
Implication Elimination
2
1
1
p => q
Premise
2
q => r
Premise
3
p => (q => r)
Implication Creation
2
4
(p => q) => (p => r)
Implication Distribution
3
5
p => r
Implication Elimination
4
1