Rules

Pandora is a natural deduction proof tool that uses a set of rules to prove a conclusion from a set of given formulas. Before you can apply any rules in pandora you must first specify your given formulas, and the conclusion you are attempting to prove. After these have been entered you can then apply Pandora's rules to your proof lines to reach the conclusion.

In Pandora, some rules can be applied in both a forwards direction (on an empty line using lines that appear before it) and also in a backwards direction (on the uppermost conclusion line using lines that appear before it). There are also rules that can only be applied backwards. (See here for more information about applying a rule forwards/backwards)

Here is a table of all the Natural Deduction rules in Pandora:

Rule Name Forwards Backwards

And Elimination Yes

And Introduction Yes Yes

Arrow Elimination Yes Yes

Arrow Introduction Yes

Bottom Elimination Yes Yes

Equality Substitution Yes Yes

Exists Elimination Yes

Exists Introduction Yes Yes

For All Arrow Elimination Yes Yes

For All Arrow Introduction Yes

For All Elimination Yes

For All Introduction Yes

If and Only If Elimination (derived) Yes Yes

If and Only If Elimination Yes Yes

If and Only If Introduction (Derived) Yes Yes

If and Only If Introduction Yes Yes

Law of Excluded Middle Yes Yes

Lemma Yes

Not Elimination Yes Yes

Not Introduction Yes

Not Not Elimination Yes Yes

Or Elimination Yes

Or Introduction Yes Yes

Proof by Contradiction (PC) Yes

Reflex (x=x) Yes Yes

Tick Yes Yes

Top Introduction Yes Yes

Trust Me Yes Yes