Section 2.4: Problem 1 Solution »

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 First-Order 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.
  1. 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.
  2. 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 ).
  3. .
  4. where does not occur free in .
  5. (if the language has ) .
  6. (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:
  1. 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 .
(Re-Replacement 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:
  1. If , it is sufficient (and always possible) to show .
  2. If ,
    1. If does not occur free in , it is sufficient (and always possible) to show .
    2. If does occur free in , it is sufficient (and always possible) to show using the Re-Replacement Lemma.
  3. If ,
    1. If , it is sufficient (and always possible) to show .
    2. If , it is sufficient (and always possible) to show .
    3. If , it is sufficient to show where is substitutable for in , but it is not always possible.
      1. One can try, iff , or if .
      2. Reductio ad absurdum.