[FOM] The rule of generalization in FOL

[Arnon Avron]

This is a good opportunity to mention an important fact that almost
all textbooks I know hide or ignore. In my paper "Simple Consequence
Relations" (Information and Computation 92, 105-139, 1991), as well
as in my contribution to the Volume "What is a Logical System (edited
by D. Gabbay) I emphasized (though I dont claim any priority here,
of course) that there is no single "First Order Logic",
but there are TWO different ones. They share the same class of languages,
and have the same set of logically valid formulas, but they differ
in their consequence relations. According to one (which I have called
the "truth consequence relation"), a formula A follows from a theory T
if every pair <M,v> (where M is a structure for the corresponding
language, and v is an assignment in the domain of M) which satisfies all
the formulas in T  satisfies also A. According to the other
(which I have called the "validity consequence relation"), 
a formula A follows from a theory T if A is valid in every structure M
(i.e.: satisfied in M by every assignment v) in which all formulas
of T are valid. 

  Every textbook I know uses exactly one of these two consequence relations
as the official definition of consequence in FOL (the only one I know
In which soundness and completeness are practically stated
and  proved for both is Peter Andrews' book, and even he does not
refer to them as two different consequence relations). To take four classical
textbooks as examples:  The books of Mendelson and of Shoenfeld 
use the "validity" consequence relation, while those of Enderton 
and of van Dalen uses the "truth" consequence relation (Usually books
which employ a Natural deduction systems, like van Dalen's book,
use the "truth" consequence relation, while those who employ
Hilbert-type systems, like the books of Mendelson and Shoenfeld,
use the "validity" consequence relation.  However, Enderton's book
is a counterexample here).

Now the main deductive differences between the two consequence relations
are the following:

1) The deduction theorem obtains for the "truth" consequence relation
but not for the "validity" consequence relation (this is why 
natural deduction systems are mainly suitable for the "truth" 
consequence relation)

2) The direct rules of Generalization and of Substitution (of terms for free
variables) obtain for the "validity" consequence relation, but not
for the "truth" consequence relation. By "direct" I mean 
pure Hilbert-type rules that take any  formula and return another 
formula (We have of course a 
counterpart of these rules in natural deduction system, but in such systems
rules are really applied to sequents, and return a sequent. Thus  the 
generalization rule of ND allows the inference of \Gamma=>\forall x A
from \Gamma=> A if x is not free in any formula of \Gamma, while
the substitution rule,  usually not taken as a primitive rule,
allows to infer \Gamma'=> A' from \Gamma=> A if the former is obtained
from the latter by a simultaneous substitution in all formulas).

  It is worth noting that these two consequence relations are
not peculiar to FOL, and the difference is not
due to the presence of quantifierss, but to the use 
of variables inside the formal language. The two
consequence relations are  known in fact to every
pupil in high school who learns the difference between identities
and equations. The "validity" consequence relation
is used while dealing with identities. Hence the substitution rule is 
available, and one may infer sin x = 2sin(x/2)cos(x/2) from 
the identity sin(2x)=2sin x cos x. In contrast, the 
"truth" consequence relation is used in solving equation, and substituting
x/2 for x everywhere in an equation is an error (but one can still 
replace equals by equals, since this rule obtains for "truth"). 
Birkhoff'd famous completeness theorem for equality reasoning
applies to the "validity" consequence relation, of course.

   Given these facts, I cant understand Hodges's problem:

> 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.   

"Z(a)" for itself is just something we write. What it says (if it says)
depends on the meaning *we* attach to it. Even a close formula
"says" nothing until we decide what structure we are talking about.
Similarly, the meaning of an open formula might depend on a
structure *and* an assignment in it. In other 
contexts or for other applications we might take its meaning to be
identical with its universal closure, depending on the structure
alone (like in the "validity" consequence relation). After all,
all the algebraic and trigonometric identities proved, used, and
manipulated in high school are open, and it would be foolish to use
a first-order system for this task rather than pure equality
reasoning. Should we tell the pupils that everything they write
while deriving such identities from other identities is meaningless??
Of course not, since their meaning in this context is very clear.


Arnon Avron