<
logic> A set of rules expressing how valid
proofs may be constructed in
predicate logic.
In the traditional notation, a horizontal line separates
premises (above) from
conclusions (below). Vertical ellipsis (dots) stand for a series of applications of the rules. "T" is the constant "true" and "F" is the constant "false" (sometimes written with a
LaTeX \perp).
"^" is the AND (
conjunction) operator, "v" is the inclusive OR (
disjunction) operator and "/" is NOT (negation or
complement, normally written with a
LaTeX \neg).
P, Q, P1, P2, etc. stand for
propositions such as "Socrates was a man". P[x] is a proposition possibly containing instances of the variable x, e.g. "x can fly".
A proof (a sequence of applications of the rules) may be enclosed in a box. A boxed proof produces conclusions that are only valid given the assumptions made inside the box, however, the proof demonstrates certain relationships which are valid outside the box. For example, the box below labelled "Implication introduction" starts by assuming P, which need not be a true
proposition Q ---------- Q
(If P and P implies Q then Q).
NOT elimination, contradiction:
P /P ------ F
(If P is true and P is not true then false is true).
(1995-01-16)
Free Download Now!
