- argument a set of propositions where one (the "corollary")
is claimed to follow from the others (the "premises").
- valid argument one whose corollary is true whenever all the
premises are true;
- validation the process of ascertaining the validity of an argument;
cf proof of theorem.
axiom a statement (usually a fully quantfied predicate)
that is assumed to be true for the purposes of proving other statements.
axiomatic theory a noncontradictory (i.e. not giving
rise to a contradiction) set of axioms intended as a basis for proving
calculus a set of strings of symbols (i.e. fomulae)
with a set of formal rules that define how a formula can be rewritten without
changing its value ("calculated"). The meaning of the formulae
and the justification of the rules are not part of the calculus and may
not be relied upon in calculations.
(logical) connectives words, such as "and"
,"or", "if...then..", etc., that are used to connect
atomic propositions in a compound one.
contradiction a compound proposition whose truth
value is "false" irrespective of the truth values of the atomic
propositions it consists of.
- (partial) correctness a program is partially correct if its
postcondition is satisfied whenever it terminates. In determining partial
correctness it is assumed that the precondition is satisfied. Partial correctness
does not imply that the program will necessarily terminate.
(full) correctness a program is correct if it is
partially correct and terminates whenever the precondition is satisfied.
equivalence the logical connective that yields
true only when both propositions are either true or false simultaneously.
It is represented as "p if and only if q" and can
be understood as mutual implication: "(p if q) and (q
implication the logical connective represented
as "if...then..." or by an arrow ->. The truth vale of "if
p then q" is true unless p is true and q
- inference rules for programs are logical arguments that infer
partial correctness of a command (in a programming language) from the partial
correctness of its constituent parts.
instantiation the process of replacing a variable
proposition occurring in a tautology by any particular propositional statement.
The result of instantiation is guaranteed to be another tautology.
laws of logic equivalence-based tautologies which
can be used for simplification of logical formulae. Examples are: de Morgan's
laws, associativity of "or", etc.
- Modus Ponens also known as the "rule of detachment"
and "method of affirming". An inference rule which states that
if p implies q and p is true then so is q.
- Modus Tollens also known as the "method of denying".
An inference rule which states that if p implies q and q
is false, then so is p.
- operator "not" the operator which, when applied to
a propositon, inverts its truth value, i.e. makes a true proposition a
false one and vice versa.
- predicate a proposition whose truth value depends on a variable.
The variable may range over any class of objects (the "universe of
discourse") as long as the truth value of the proposition is certain.
- principle of mathematical induction (week form) states that
for a predicate P(n) with the universe of discours being
all natural numbers, the fact that both P(1) is true and for all
n>0 P(n) implies P(n+1) constitutes
a proof of the truth of P(n) for all n>0.
- principle of mathematical induction (strong form) states that
for a predicate P(n) with the universe of discours being
all natural numbers, the fact that both P(1) is true and the conjunction
of all P(k), k=1..n implies P(n+1)
constitutes a proof of the truth of P(n) for all n>0.
- principle of well ordering states that every set of natural
numbers has the least element.
- program verification the process of proving the correctness
argument for a given program with respect to a particular set of pre- and
- proof of a theorem the process of validating the logical argument
contained in the theorem possibly using its axioamatic
theory as additional premises.
- direct proof a proof technique which assumes the truth of the
theorem's premises for some unknown instance of the variables and then attempts to
derive the truth of the corollary for the same instance of the variables.
- contrapositive proof a proof technique which assumes the falsehood
of the theorem's corollary on some unkonwn instance of the variables and then attempts
to demonstrate that at least one premise of the theorm is false on the same instance
of the variables.
- proof by contradiction also known as "reductio ad absurdum",
a proof technique that assumes that there exists an instance of the variables
for which all the premises are true and at the same time the corollary
is false. It then goes on to show that this assumption leads to a contradiction.
proposition a statement with a definite truth value.
- atomic proposition, one that does not have internal structure,
i.e. no smaller propositions can be identified as its parts.
- compound proposition, one that consists of one or more propositions
held together by logical connectives and the operator "not".
- quantifier an operator applicable to a predicate and its parameter:
- universal quantifier, pronounced "for all" and
denoted by the letter A written upside
down. When applied to a predicate, it yields
"true" if the predocate is true everywhere in the universe
- existential quantifier, pronounced "there
exists" and denoted by the letter E reflected about
a vertical line (we have no font for this either)
When applied to a predicate, it yields "true" if the
predicate is true anywhere in the universe of discourse.
- rules of inference small valid arguments that involve only variable
propositions. With respect to their variables, the rules of inference are tautologies.
When appropriately instantiated, they are useful in proving other arguments
- substitution the process of replacing a proposition that occurs
in a given compound proposition by its equivalent. The result of substitution
is guaranteed to be equivalent to the original compound proposition.
- (Hypothetical) Syllogism an inference rule which states that
if p implies q and q implies r then p implies
- tautology a compound proposition that is true irrespective of
the truth values of the atomic propositions that it consists of.
- theorem a statement claimed to be true given the truth of an
axiomatic theory. A theorem is said to be stated in the axiomatic
theory on whose truth it is dependent. All theorems should either refer
to or assume the axiomatic theory they are stated in.
- universe of discourse see predicate
- universal generalisation the rule in the predicate calculus
that states that if a predicate P(x) is true for any x
then it is true for all x. It is assumed that x ranges
over the universe of discourse.
- universal specification the rule in the predicate calculus that
state that if a predicate P(x) is true for all x then
it is true for any given x. It is assumed that x ranges over
the universe of discourse.