Pandora was originally written by Dan Ehrlich as a 4th-year project in 1998 and has been developed over the past decade by a number of DoC students. While using Pandora to do proofs, there are a few conventions differing from the Logic course.

Logic Syntax

Please see the Logic Syntax used in Pandora.

Lemma and Excluded Middle

In the Logic lecture notes:

"A Lemma is something you prove that helps in proving something else better."

In Pandora, this is called Law of Excluded Middle, which is a theorem that can be introduced anywhere in your proof.

Nevertheless, there is something called "Lemma" which is different from the Law of Excluded Middle in Pandora.

The Lemma in Pandora is a formula that can be introduced into the proof to help in proving the conclusion.

In some cases a large proof can best be tackled by breaking it down into smaller steps. For example, if you are trying to show Data |- Conclusion then maybe you could show Data |- Lemma and then make use of Lemma to show Conclusion -- (Data and Lemma) |- Conclusion.

Rules for IFF(If And Only If)

Both Pandora and the Logic lecture notes agree with that one of the ways to use the IFF Introduction rule is:

In Pandora, this is used as the IFF Introduction(Forwards) Rule.

In the Logic lecture notes, the other two ways of using the IFF Introduction are:

However, they are not implemented in Pandora. In stead, you can use the IFF Introduction(Backwards) Rule in Pandora like this:

Or with the "Expert Mode" in Pandora, you can use the IFF Introduction Derived Rule like this:

Both Pandora and the Logic lecture notes agree with that the way of using the IFF Elimination rule is:

With the "Expert Mode" in Pandora, you can also use the IFF Elimination Derived Rule like this:

If you want some more information please refer to the Logic lecture notes and the help pages for IFF Introduction, IFF Elimination, IFF Introduction (Derived) and IFF Elimination (Derived).