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

[Kai Brünnler]

Dear Sandy,

1. There is indeed a system on p. 26 of my thesis which has the 
properties you're looking for. In a nutshell, the inference rules deal 
with the universal quantifier not by dropping it when going up, but by 
moving it out of the way. In the strict technical (but not moral!) sense 
this requires to drop the subformula property. It also means that 
inference rules are sound in the strong sense that the premise implies 
the conclusion and not only in the weaker sense that the validity of the 
premise implies the validity of the conclusion.

2. The system by Craig ("Linear Reasoning. A new form of the 
Herbrand-Gentzen Theorem" JSL, 1957) also avoids having to call formulas 
with free variables "theorems". I'm not sure whether you will consider 
it to be of "natural deduction sort", though.

3. After checking with some of my collegues here in Bern it seems to me 
that "working logicians" do not share your concern about calling 
formulas with free variables "theorems". Are you aware of any technical 
(as opposed to philosophical) problems arising from that?

Best wishes,

-Kai
http://www.iam.unibe.ch/~kai/


> At 13:29 -0700 30.8.04, Sandy Hodges wrote:
>> 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