The Proof Builder uses a logical system that closely resembles the calculus used by E. J. Lemmon in his book Beginning Logic (London: Chapman & Hall) and by Colin Allen in his book Logic Primer (Cambridge: MIT Press 1992). Some familiarity with either system or with natural deduction calculi will be required when using the Proof Builder. If you feel not sufficiently familiar with any of these systems, you might consider having a look at the other functions of the Gateway to Logic.
Propositional expressions consist of propositional variables, connectives and brackets.
A propositional variable (or, shorter, just "variable") is an uppercase letter, followed by zero or more digits or letters. Thus, the strings "P", "Q", "P1", "Q42", as well as "Proposition" or "IamAniceProposition" are (different) propositional variables. Note that most tasks accept propositions which start with a lowercase letter, too. Since the proof checker does not, you should probably always use capitalized propositional variables.
Semantically, as their name indicates, propositional variables signify a proposition (you can treat them as an abbreviation of an English proposition). For example, you can decide to use the propositional variable "P" as an abbreviation of the English proposition "It is raining", or the variable "Q42" as an abbreviation of "All pigs are pink".
The strings "~", "&", "v", "->", "<->", and only these strings, are connectives. They are used for composing new propositions out of (usually two) existing ones.
The string "~" is the first and only exception to the rule that connectives compose two propositions into a new one: It needs only one existing proposition. In general, if foo is a proposition, by placing "~" in front of it you form a new proposition.
As indicated by the preceding chapter, "P" is a proposition. Thus, we can form a new proposition out of "P" by placing a "~" in front of it: "~P". Of course, we can repeat that step: Now knowing that "~P" is a proposition, we can create another proposition by just writing a "~" in front of it: "~~P".
As its name implies, the string "~" is used to deny the truth of a proposition. Hence, if we use "P" as an abbreviation for "It is raining", "~P" means (more or less) "It is not raining".
The string "&" is used to combine two existing propositions into another one by writing the "&" between them, but we have to enclose the expression formed so far in brackets.
So, if we use "~~P" and "Q42" (we already know that both are propositions), we easily form the new proposition "(~~P & Q42)".
The "&" is used to express confidence that both the sentence to its left as well as the sentence to its right are true.
The string "v" (the lowercase letter "v"), analogous to "&", combines two propositions. If foo and bar are propositions, the string "(foo v bar)" is a proposition, too.
Please note that if there is a propositional variable right before or after "v", the gateway requires you to separate the "v" from the variables by at least one space character. Although this might seem strange at the first glance, especially since in the case of the other connectives there is no such requirement, there is a simple reason. It is easiest demonstrated by a simple example: In the case of the proposition "PvQ v R", the gateway could not decide whether "PvQ" is one variable, namely "PvQ", or if "PvQ" is the disjunction of the two variables "P" and "Q".
The meaning of "v" is quite the same as the meaning of the English phrase "...or..., or both". Thus, "P" abbreviating "It is raining" and "Q" abbreviating "The sun is shining", "P v Q" signifies "It is raining, or the sun is shining, or both".
As in the case of "&" and "v", "->" combines two existing propositions into a new one. As usual, if foo and bar are two propositions, the expression "(foo -> bar)" is a proposition, too.
The connective "->" usually is translated by the phrase "if... then...". Although this is not wrong, it is sometimes misleading.
If foo and bar are two propositions, the expression "(foo <-> bar)" is a proposition, too.
The translation of "<->" is "...if and only if...", which often is abbreviated as "iff". "(foo <-> bar)" signifies that either both foo and bar are true or that both are false.
Although a strict formal language usually requires brackets, the gateway allows you to leave them out. In this case, it evaluates negations, then conjunctions, followed by disjunctions, conditionals and finally biconditionals. Two or more occurrances of the same connective are evaluated from left to right. Hint: If you don't understand this paragraph, use brackets.
If some of the keys of your keyboard are broken or you can't find a certain key you would need to enter a connective, you need not despair. There are alternatives.
Remark: In fact it is desirable to use "|" instead of "v", since that makes the lexicographic analysis of your input deterministic. If you don't understand this remark, you should either use "|" instead of "v" or always place a space character before and after the "v".
Like propositional variables, predicates start with an uppercase letter, followed by zero or more letters or digits. The arguments of the predicate are enclosed by brackets and separated by commas. Examples are "Philosopher(Sokrates)" or "Loves(Foo,Bar)".
Individual constants look exactly like propositional variables, i.e. they consist of one uppercase letter, followed by zero or more letters or digits. Individual constants are "Sokrates", "Platon" or "Frege". Individual constants denotate exactly one individual, each - hence the name.
Invidual variables consist of one lowercase letter, followed by zero or more letters or digits. Individual variables signify nothing.
The strings "exist" and "all" represent existential and universal quantification. The bound variable and the quantified expression, enclosed in brackets and separated by a comma, follow the quantifier.
"All pigs are pink" could be translated as "all( x, Pig(x)->Pink(x) )". "Some pigs are not pink" would be "exist( x, Pig(x) & ~Pink(x) )".
The syntax of proofs, too, resembles Lemmon's notation. The following example shows a proof which the gateway accepts without modifications.
1 (1) P->Q A 2 (2) ~Q A 3 (3) P A 1,3 (4) Q 1,3MPP 1,2,3 (5) Q & ~Q 2,4&I 1,2 (6) ~P 3,5RAA 1 (7) ~Q -> ~P 2,6CP
Explaining the deduction rules in detail would lead us a bit too far into detail. All I can provide here is an overview: