| |
|
Logica |
Tools
for
Thought
|
|
| Name |
Description |
Depth |
| Negation Introduction |
{p} ⊢ ~~p |
0 |
| Negation Elimination |
{~~p} ⊢ p |
0 |
| And Introduction |
{p, q} ⊢ p&q |
0 |
| And Elimination |
{p&q} ⊢ {p, q} |
0 |
| Or Introduction |
{p} ⊢ {p|q, q|p} |
0 |
| Or Elimination |
{p|q, p=>r, q=>r} ⊢ r |
0 |
| Implication Elimination |
{p=>q, p} ⊢ q |
0 |
| Biconditional Introduction |
{p=>q, q=>p} ⊢ p<=>q |
0 |
| Biconditional Elimination |
{p<=>q} ⊢ {p=>q, q=>p} |
0 |
| Implication Creation |
{p} ⊢ q=>p |
1 |
| Implication Distribution |
{p=>(q=>r)} ⊢ (p=>q)=>(p=r) |
1 |
| Implication Reversal |
{~q=>~p} ⊢ p=>q |
1 |
| Inconsistency |
{p, ~p} ⊢ q |
1 |
| Conditional Deduction |
{p=>(q=>r), p=>q} ⊢ p=>r |
1 |
| Transitivity |
{p=>q, q=>r} ⊢ p=>r |
1 |
| Condition Introduction |
{q=>r} ⊢ (p=>q)=>(p=>r) |
1 |
| Conclusion Introduction |
{p=>q} ⊢ (q=>r)=>(p=>r) |
1 |
| Condition Reversal |
{p=>(q=>r)} ⊢ q=>(p=>r) |
1 |
| Modus Tollens |
{p=>q, ~q} ⊢ ~p |
1 |
| Implication Reduction |
{p=>~p} ⊢ ~p |
1 |
| Contradiction Realization |
{p=>q, p=>~q} ⊢ ~p |
1 |
| |
| Universal Conjunction |
{AX:(p(X)&q(X))} ⊢ AX:p(X)&AX:q(X) |
1 |
| Universal Implication |
{AX:(p(X)=>q(X))} ⊢ AX:p(X)=>AX:q(X) |
1 |
| Universal Reversal |
{AX:AY:p(X,Y)} ⊢ AY:AX:p(X,Y) |
1 |
| Existential Universal |
{EY:AX:p(X,Y)} ⊢ AX:EY:p(X,Y) |
1 |
|