[FOM] The rule of generalization in FOL, and pseudo-theorems

[Sandy Hodges]

If we wanted to say what a logical theory is, we might use this
definition, taken from Wikipedia:

[A] logical theory, ... consists of

1) ...
2) a set of axioms, ....
3) a set of inference rules which allow one to prove theorems from
axioms or earlier proven theorems.

This is a good definition; however the first-order calculus, as
presented in this same article, and in most textbooks, does not conform
to it, at least not unless you are willing to accept a stretched
definition of 'theorem'.   The problem is the 'rule of
generalization.'   This says that if we have proved some formula:
  Z(a)
where 'a' represents an arbitrary variable, and "Z(a)" represents any
formula containing that variable, then we may conclude:
   (Forall x) Z(x)

This rule only conforms to the above definition of a logical theory, if
   Z(a)
is a theorem.   But the claim that "Z(a)" is a theorem causes
difficulties for the philosophy of logic.  We might say of a logical
theory, that if it's axioms are true, and its rules preserve truth, then
its theorems must be true.   But "Z(a)" is not the sort of thing that
can be either true or false.   "Z(a)" does not say anything, because "a"
does not name anything.   Whereas a theorem, for example:
   (Forall x) ( 0 < x => (Exists y) x < y )
says something about numbers, a formula such as
    0 < a => (Exists y) a < y
does not say anything because "a" is not defined.   I would say that "0
< a => (Exists y) a < y" is not a theorem - but even if we called it a
theorem, the problem would not go away - we then have to deal with
"theorems" which don't say anything, which are neither true nor false.

Here's the way the rule of generalization is used; usually we have a
formula of the form:
   (Forall x) K(x)
and we infer
    K(a)
by the appropriate rule.   "a" should be a variable not previously used
in the proof.   Then after some steps we arrive at
    Z(a)
and then we use generalization to conclude
    (Forall y) Z(y)
If we want to convert this "proof", into a proof in which only theorems
occur, then the strategy is to prefix every step in which an unbound "a"
occurs, with "(Forall a)".  We then need to convert every step in the
proof: For example, if a step in the original "proof" uses modus ponens,
we need to prove:
   (Forall a) ( R(a) => Q(a) )
   (Forall a) R(a)
   -------------
   (Forall a) Q(q)
Additional rules of inference or axioms will be needed to make possible
all the needed proofs.    These rules take the place of the rule of
generalization.

What I am hoping for is a source to cite, in which first-order logic is
presented in a way that does not require such psuedo-theorems as "0 < a
=> (Exists y) a < y".  If anyone knows of a textbook or article that has
a system for first-order logic that avoids such "theorems", I would
appreciate knowing where it is.   I do want a system that is of the
'natural deduction' sort - one that conforms to the definition given
above: that a logical theory is a list of axioms and a list of rules.

Thanks for any references or other comments:

Sandy Hodges

Here is the Wikipedia citation:
http://en.wikipedia.org/wiki/First-order_predicate_calculus
------- -- ---- - --- -- --------- -----
Sandy Hodges / Alameda,  California,   USA