[FOM] The rule of generalization in FOL

[Neil Tennant]

On Tue, 7 Sep 2004, Arnon Avron wrote:

> Neil, I dont understand something. You write:
> 
> > My book Natural Logic (Edinburgh U. Press, 1978; 2nd, revd. edn 1990)
> > follows Prawitz's monograph Natural Deduction (Almqvist & Wiksell,
> > Stockholm, 1965) in allowing only sentences to occur in proofs. Hence only
> > sentences can be premises or conclusions of proofs. In particular, only
> > sentences can be theorems.
> > 
> > If one proves a theorem of the form F(a), then of course one extra step of
> > universal introduction would produce the explicitly general theorem
> > (x)F(x).
> 
> Now I take it that one cannot infer in your system "(x)(y)x=<y"
> from "(y)0=<y". On the other hand one can infer "(x)(y)x=<y"
> from "(y)a=<y", where a is (I guess) an "arbitrary constant". So
> obviously constants like 0 treated differently in your system from 
> "arbitrary constants" like a. So what is the difference between your
> constant a and a variable, and in what sense is "F(a)" a sentence
> while "F(x)" is an open formula? Or maybe you dont have open formulas
> at all in your system, and every formula is a "sentence"?

Arnon,
 
If from premises X not involving the name 0 you have proved F(0), then you
may infer (x)F(x), in which 0 no longer occurs.

Indeed, for any name a:

If from premises X not involving the name a you have proved F(a), then you
may infer (x)F(x), in which a no longer occurs.

Typographically, 0 has no special status; it is a name like any other.

The difference between a name and a variable is that the latter, but not
the former, can occur in a sentence only if bound by a quantifier. One has
the usual inductive definition of "phi is a formula with such-and-such
occurrences of variables free"; and a sentence is a formula with no free
occurrences of variables.

The *proof system*, however, allows only sentences to occur in proofs.

Best,
Neil