[FOM] The rule of generalization in FOL, and pseudo-theorems
kai.bruennler at gmx.net
Tue Aug 31 08:16:59 EDT 2004
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?
> 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
More information about the FOM