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

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