[FOM] The rule of generalization in FOL

[Arnon Avron]

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