Listed below are the technical
definitions of many of the terms that are used in the investigation
of deductive reasoning.
Denumerable  A set is denumerable if it can be
put into a onetoone correspondence with the positive integers.
Countable  A set is countable if it is either
finite or denumerable.
A formal theory T consists of:
(1) A countable set of symbols.
(A finite sequence of symbols of T is called an expression
of T.)
(2) A subset of the expressions,
called the wellformed formulas (abbreviated wffs) of
T. The wffs are the legal sentences of the theory.
(3) A subset of the wffs called
the axioms of T.
(4) A finite set of relations
R1, ..., Rn on wffs, called rules of inference. For each
Ri there is a unique positive integer j such that for every j
wffs and each wff A one can effectively decide whether the given
j wffs are in the relation Ri to A; if so, A is called a direct
consequence of the given wffs by virtue of Ri. For example,
the rule modus ponens is a relation on three wffs, A, A >
B, and B, by which B is a direct consequence of A and A >
B.
Since the set of axioms is often
infinite, this set is often specified by providing a finite set
of axiom schemata. A schema is a statement form; it provides
a template showing the form of a wff while leaving some pieces
unspecified through the use of metavariables. In the above example
A and B are metavariables which stand for wffs of the theory.
An instance of a schema is a wff obtained from the statement
form by substitution.
Deducible from S in T  Let S be a set of wffs, and let P
be a wff in the formal theory T. We say that P is deducible from
S in T (denoted by S T P) if there exists a finite sequence
of wffs P1, ..., Pn such that Pn = P and for 1 < i < n
Pi is either an axiom, a formula in S (called a hypothesis),
or a direct consequence of previous Pi's by virtue of one of
the rules of inference.
Proof or Derivation  The sequence of Pi's is called a derivation
of P from S, or a proof of P from S.
Theorem
 If P is deducible from the empty set, we write T P , and
say that P is a theorem or P is provable in T.
The following properties of deducibility
are consequences of the definition of deducible from:
Let S1 and S2 be sets of wffs,
and A a wff, then
1. If S1 is a subset of S2 and
S1  A, then S2  A. This property is called monotonicity.
2. S1  A if and only if there
is a finite subset S2 of S1 such that S2  A. This property
is called compactness. (Since
a derivation must be finite, it must require only a finite number
of hypotheses)
3. If S2  A, and for each wff
B in S2, S1  B, then S1  A. (If
every wff in S2 can be derived from the set of wffs S1, then
anything that can be derived from S2 can also be derived from
S1.)
Interpretation  An interpretation supplies a meaning
for each of the symbols of a formal theory such that any wff
can be understood as a statement that is either true or false
in the interpretation.
Model
 An interpretation is a model for a set of wffs S if every wff
in S is true in the interpretation.
Completeness  A theory is complete if every sentence
that is true in all interpretations is provable in the theory.
Soundness  A theory is sound if every provable
sentence is true in all interpretations.
If a theory is sound and complete
then truth and deduction are equivalent.
A computation method is complete
if for every sentence S, the algorithm will terminate on input
S in a finite amount of time, indicating whether or not S is
true in all interpretations.
Decidable  A formal theory is decidable if there
exists an effective procedure that will determine, for any sentence
of the theory, whether or not that sentence is provable in the
theory.
(Any property is said
to be decidable if there exists an effective procedure (i.e.,
terminating algorithm) that will determine whether or not the
property holds.)
Consistent  A theory is consistent if it contains
no wff such that both the wff and its negation are provable.
First Order Predicate Calculus is sound, complete, and consistent,
but not decidable.
