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

[Richard Zach]

Dear Sandy et al.,

You raise an interesting question.  I don't know of a recent textbook
calculus of first-order logic in which all theorems are sentences.
However, I also don't think that it raises a particularly pressing
question for the philosophy of logic.  It is true that there is a
disconnect between the definition of validity in most textbooks
(preservation of truth) and the requirement of soundness on systems of
derivation (preservation of validity).  But that's just that: a
disconnect.  All it means is that validity is not all that must be
required of inference rules in a logical calculus.  Even when no free
(object) variables are involved, you can see this disconnect in
derivation systems for modal logic:  the inference from A to Necessarily
A is invalid (on the preservation of truth definition) but is sound for
systems of normal modal logic (in the sense of preservation of
validity).

There is precedent for your concern about the status of open formulas in
derivations, though.  In an interview late in his life, Paul Bernays
said this about his involvement in the working out of the first-order
calculus in Hilbert's 1917/18 lectures on the "Principles of
mathematics":

"My knowledge [of logic] was very incomplete at the time, in 1917.
Before Hilbert took up the [investigation of the foundations of
mathematics] directly again, which he had started much earlier, he did
not immediately lecture on that, but he gave a course on mathematical
logic.  And I was in charge of writing up [ausarbeiten] that lecture
course, and I did this in such a way that I avoided free variables.  I
had looked at Russell a little bit, and first I found it too broad and
did not like it in all respects, but in particular I did not understand
what it means to say ``for all $x$, $F(x)$, then $F(y)$ follows.''  In
fact, the application of free variables is something technical.  These
are two ways to represent generality.  One has generality on the one
hand through bound variables and on the other through free variables.
There is no such difference in natural language.  So I avoided free
variables at first.  This is a possible way of approach, and later
others have also done it this way."

(cited in my "Completeness before Post: Bernays, Hilbert, and the
development of propositional logic," Bulletin of Symbolic Logic 5 (1999)
331–366. http://www.ucalgary.ca/~rzach/papers/bernays.html)

The system Bernays worked out, which I believe to be the first deduction
system for first-order logic (presented as such--i.e., not a fragment of
a higher-order system such as Frege's or Russell's) avoids, as Bernays
says, the use of free object variables.  Very soon thereafter, at least
by the time Grundzuege came out (1928), Hilbert (and presumably Bernays)
didn't think twice about having open formulas in derivations.

Yours,
Richard
-- 
Richard Zach ...... http://www.ucalgary.ca/~rzach/
Associate  Professor,   Department  of  Philosophy
University of Calgary, Calgary, AB T2N 1N4, Canada