## 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.