Logica Tools
for
Thought
 
Hilbert
Copy Load Save Library
Objects  a, b, c
Functions  f, g

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