0. Introduction
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.
Rules of thumb
- Use upper-case propositional variables (e.g. P, Q, R instead of p, q, r).
- Use the connectives ~, &, v, (i.e. the lower-case letter), -> and <-> (negation, conjunction, disjunction, conditional, biconditional) or the English words not, and, or, then and iff.
- Always place at least one space character between a connective
consisting of letters and a propositional variable or another
connective (e.g. enter P and Q instead of
PandQ
and p v q instead of pvq).
For your convenience there is one exception to this rule: If you use propositional variables consisting of exactly one upper-case letter, you need not separate them from the connective v (and only from this connective) with a blank (i.e., you can write PvQ instead of P v Q).
1. Propositional variables
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".
2. Connectives
The strings "~", "&", "v", "->", "<->", and only these strings, are connectives. They are used for composing new propositions out of (usually two) existing ones.
2.1. The string "~", also known as negation
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".
2.2. The string "&", also known as conjunction
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.
2.3. The string "v", also known as disjunction
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".
2.4. The string "->", also known as conditional or implication
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.
2.5. The string "<->", also known as biconditional
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.
3. More about brackets
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.
4. Hints for users with broken keyboards
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.
- Instead of "~", you can use the dash "-" or the English word "not".
- Instead of "&", you can enter "^" or the English word "and".
- Instead of "v", you can enter "|" (not to be confused with the Sheffer stroke, which this "|" isn't), or the English word "or".
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".
5. Predicates
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)".
6. Individual constants
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.
7. Individual variables
Invidual variables consist of one lowercase letter, followed by zero or more letters or digits. Individual variables signify nothing.
8. Quantifiers
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) )".
9. Proof syntax
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:
- &E (elimination of a conjunction) allows you to move either to p or to q given that p & q is a line of the proof.
- &I (introduction of a conjunction) allows you to move from p, q as lines to p & q or to q & p.
- ->E (elimination of a conditional) allows you to move from p, p -> q to q. Often this is called 'modus ponens' or 'affirming the antecedent'.
- ~~E (elimination of double negation) allows you to move from ~~p to p.
- vI (introduction of a disjunction) allows you to move from p to p v q or to q v p where q is an arbitrary disjunct. Note that you must specify this disjunct in R1 when you are using the proof-builder. This rule is often called addition.
- vE (elimination of a disjunction) allows you to move from p v q, p |- r, q |- r to r.
- ->I (introduction of a conditional) is used to complete a conditional proof.
- ~I (introduction of a negation) is used to complete an indirect proof. The last line must be an explicit contradiction.