Section 2.4: A Deductive Calculus
Read this section until enlightenment (at least twice if you had no prior knowledge).
Suppose that . What methods of proof might be required to demonstrate that fact? Is there necessarily a proof at all?
What is a proof? Main characteristics:
 Finiteness. This is potentially possible due to the Compactness Theorem for FirstOrder Logic (to be proved in Section 2.5) implying that only a finite subset of is needed to prove .
 Decidability. Each step of the proof should be able to be verified, implying the set of proofs from the empty set of hypotheses ( ) should be decidable. This would, in particular, imply that the set of all validities is effectively enumerable. This is potentially possible due to the Enumerability Theorem (to be proved in Section 2.5) implying that, under reasonable assumptions, the validities are effectively enumerable.
Vice versa, the compactness and enumerability theorems imply that for every
there exists a finite proof which can be found in a finite number of steps.
Deductions
Given a wff
, a generalization of
is a formula
for some
and variables
.
Logical Axioms: they are all possible generalizations of the following axioms.

Tautologies.A prime formula is either an atomic formula or one of the form . A nonprime formula is any other formula (built up from prime formulas using and ).Given any wff, it is build up from prime formulas by using and , hence, can be considered as a wff of sentential logic where all prime formulas are considered as sentence symbols. A wff is called a tautology iff it is a tautology of sentential logic. Similarly, tautological implications are defined.
 If tautologically implies , then logically implies , but not necessarily vice versa.

where
is substitutable for
in
.is defined as follows: a) if is atomic, replaces each , b) , c) , d) , and e) , .is substitutable for in iff: a) if is atomic, b) if and is substitutable for in , c) and is substitutable for in and , or d) if and [ does not occur free in ] or [ does not occur in and is substitutable for in ].Note: is always substitutable for , and not containing any variables that occur in is always substitutable for any in .For any , and there is always “equivalent” to such that is substitutable for in (see the Existence of Alphabetic Variants Theorem below; the idea is that the only substitutability problem we may encounter is in the case of some where , is free in , is substitutable for in , but occurs in , in which case we rewrite it as ).
 .
 where does not occur free in .
 (if the language has ) .
 (if the language has ) where is atomic and is obtained from by replacing in zero or more but not necessary all places by .
Rule of Inference:
 Modus ponens: From , we infer .
Given a set of formulas
(and the set of logical axioms
),
is a theorem of
(
is deducible from
),
, if
can be obtained from
by use (finite number of times) of the rule of inference. A deduction of
from
describes how
can be obtained this way form
(and
), i.e. it is a finite sequence
of formulas such that a)
, and b) for
,
is in
or obtained by modus ponens from some
and
,
.
 iff tautologically implies .
 If tautologically implies , then logically implies .
Additional Rules of Inference
(Generalization Theorem) If
and
does not occur free in any wff in
, then
.

(Generalization on Constants) If
and a constant symbol
does not occur in any wffs in
, then there is a variable
that does not occur in
such that
(and a deduction of
from
that does not use
).
 If where the constant symbol does not occur in any wffs in or , then (and there is a deduction of from that does not not use ).
 (Rule EI  Existential Instantiation) If where the constant symbol does not occur in any wffs in , or , then (and there is a deduction of from that does not use ).
(Rule T) If
,
, and
tautologically implies
, then
.
(Deduction Theorem) If
then
.
(Contraposition) If
then
.
A set of wffs
is inconsistent iff for some wff
,
.
 For every consistent there is a consistent such that for every wff , either or .
(Reductio ad Absurdum) If
is inconsistent, then
.
(ReReplacement Lemma) If
does not occur in
at all, then
is substitutable for
in
and
.
(Existence of Alphabetic Variants) For a wff
, term
and variable
, there is a wff
such that a)
differs from
in the choice of quantified variables only, b)
can be proved from
and vice versa, and c)
is substitutable for
in
.
 The formulas as described in the theorem are called alphabetic variants of .
Rules for equation:
Eq1 (p. 127)
(reflexivity).
Eq2 (p. 127)
(symmetry).
Eq3 (p. 128)
(transitivity).
Eq4 (p. 128)
(similarly for
place predicate symbols).
Eq5 (p. 128)
(similarly for
place function symbols).
Strategy
Suppose we want to deduce
. Working backward:
 If , it is sufficient (and always possible) to show .

If
,
 If does not occur free in , it is sufficient (and always possible) to show .
 If does occur free in , it is sufficient (and always possible) to show using the ReReplacement Lemma.

If
,
 If , it is sufficient (and always possible) to show .
 If , it is sufficient (and always possible) to show .

If
, it is sufficient to show
where
is substitutable for
in
, but it is not always possible.
 One can try, iff , or if .
 Reductio ad absurdum.