Starting a Proof
Proofs are entered or continued in the box provided. In most of the
online exercises, the proof is already started above the box. You
should enter the next line number in sequence and continue from there.
Otherwise start by entering the first line of the proof in the box,
beginning with line number 1.
Premises are entered on numbered lines, with the conclusion appearing
to the right of the final premise. For example:
1. P → Q
2. P ∴ Q
(See below for instructions on how to type the logical symbols.)
To prove a theorem, start an unnumbered line, with the symbol for
therefore followed by the theorem that will be the
conclusion of the proof. E.g.:
∴ (((P → Q) → P) → P)
Continuing a Proof
Following the line containing the conclusion, each continuation line
should consist of a line number, a well-formed formula, and the
justification. Except for assumptions, for which the justification is
written "Assume", justifications consist of one or more line numbers
and the name of a rule, all separated by commas, e.g. "1,2,MP". (The
quotation marks are not part of the justification.)
When an assumption is made, you must also indent the proof until the
assumption is discharged by an appropriate rule. Indentation is marked
using the vertical bar character "|". For example:
1. (P ∙ Q) → R ∴ P → (Q → R)
| 2. P Assume
|| 3. Q Assume
Symbols
Keyboard characters are entered using standard keys that will be converted to the logical symbols as follows:
| ∴ |
therefore |
":." or ".:" (colon and period, in either order) |
| → |
arrow |
"->" (dash + greater than),
or simply ">" |
| ↔ |
double arrow |
"<->" (less than + dash + greater than),
or simply "<" |
| ∙ |
conjunction (dot) |
"." (a period) |
| ∨ |
disjunction (wedge) |
"v" (lower case letter vee) |
| ∃ |
existential quantifier |
"$" -- think $ome! |
| | |
subproof indentation |
type a vertical bar "|" for each level of indentation that a line should have,
e.g. "|3. P → ~Q Assume" |
Checking Proofs
Proofs may be checked at any time, even before they are complete. The
proof checker will assess each line in sequence until an error or the
end of the proof is reached. If an error is found or the proof is
incomplete, a diagnostic message will be produced and the attempted
proof will be redisplayed for you to edit and resubmit.
|
