Lemmon Language Help

(this text by Steven DeHaven, Calgary, and Christian Gottschall, Vienna)

This help neither explains the deductive system nor the Lemmon proof builder applet itself. If you need help with either of them go to Help with Rules or Help with Applet. The sole purpose of this text is to explain the formal language understood by the Lemmon Proof Builder applet.

Propositional variables are upper-case letters, i.e. "A"..."Z". If twenty-six propositional variables do not suffice, you may use them in combination with an arbitrary natural number as an index, e.g. "P1", "Z24" or "A12".
The negation may be expressed by one of the strings "~", "-", "not", leading to propositions like "~P1", "-Z24" or "not A12".
The conjunction may be expressed by one of the strings "&", "^", "and", leading to propositions like "~P1 & Z10", "-(~P1 & Z10) ^ -A" or "-~-A and B".
The disjunction may be expressed by one of the strings "v" (the lower-case letter V), "|", "or", leading to propositions like "~P1 v Z10", "-(~P1 & Z10) | -A" or "-~-A or B".
The conditional may be expressed by one of the strings "->", "=>", leading to propositions like "~P1 -> Z10" or "-(~P1 & Z10) => -A".
The biconditional may be expressed by one of the strings "<->", "<=>", "iff", leading to propositions like "~P1 <-> Z10", "-(~P1 & Z10) <=> -A" or "-~-A iff B".
Brackets may be used as needed. Both "(", ")" and "[", "]" are valid, although every open bracket must be matched by a closed bracket of the same type. Examples: "(P v Q) & R", "P & [Q v R]", "(P v Q) & [Q v R]".
You may omit brackets in which case the applet evaluates (from left to right) negations, conjunctions, disjunctions, conditionals and biconditionals. If you are unsure what this means or if you want to be in total control of everything, you should try to use brackets.