Logica Tools for Thought Hilbert Proofs Name Description Depth Implication Creation Schema ⊢ p=>(q=>p) 0 Implication Distribution Schema ⊢ (p=>(q=>r))=>((p=>q)=>(p=r)) 0 Implication Reversal Schema ⊢ (~q=>~p)=>(p=>q) 0 Identity Schema ⊢ p=>p 1 Inconsistency Schema ⊢ ~p=>(p=>q) 1 Negation Elimination Schema ⊢ ~~p=>p 3 Negation Introduction Schema ⊢ p=>~~p 4   Implication Elimination {p=>q, p} ⊢ q 0 Implication Creation {p} ⊢ q=>p 1 Implication Distribution {p=>(q=>r)} ⊢ (p=>q)=>(p=r) 1 Implication Reversal {~q=>~p} ⊢ (p=>q) 1 Negation Elimination {~~p} ⊢ p 2 Negation Introduction {p} ⊢ ~~p 4 Inconsistency {p, ~p} ⊢ q 2 Conditional Deduction {p=>(q=>r), p=>q} ⊢ p=>r 2 Transitivity {p=>q, q=>r} ⊢ p=>r 2 Condition Introduction {q=>r} ⊢ (p=>q)=>(p=>r) 2 Conclusion Introduction {p=>q} ⊢ (q=>r)=>(p=>r) 3 Condition Reversal {p=>(q=>r)} ⊢ q=>(p=>r) 3 Contradiction {p=>r, q=>~r} ⊢ p=>~q 3 Contrapositive {p=>q} ⊢ ~q=>~p 4 Modus Tollens {p=>q, ~q} ⊢ ~p 5 Implication Reduction {p=>~p} ⊢ ~p 5 Contradiction Realization {p=>q, p=>~q} ⊢ ~p 6