Use these links to jump directly to the following topics

1,2 (5) PvQ 4vIaset lnum sent ann

~ (not) & (and) v (or) -> (if...then...) <-> (if and only if) @ (all) $ (some)

There are 10 primitive rules of proof for the sentential system | |
---|---|

AssumptionA
Wedge-Elimination 1,2 vE Wedge-Introduction 1 vI Ampersand-Elimination 1 &E Ampersand-Introduction 1,2 &I |
Arrow-Elimination1,2 ->EArrow Introduction 1 ->I (2)Reductio ad Absurdum 1,2 RAA (3)Double-Arrow Elimination 1 <->EDouble-Arrow Introduction 1,2 <->I |

There are six primitive rules of proof for the predicate system | |

Universal Elimination1 @EUniversal Introduction 1 @IExistential Elimination 1,3 $E (2) |
Existential Introduction1 $IIdentity Elimination 1,2 =EIdentity Introduction =I |

DN MTT v-> DM HS FA TC |
IA Neg-> vAssoc &Assoc vComm &Trans Dist Imp/Exp |
BP BT Neg<-> Bitrans SimDil SpecDil ComDil |

The rule QE introduced in chapter 3 is also accepted by the program.