[FOM] The rule of generalization in FOL
Neil Tennant
neilt at mercutio.cohums.ohio-state.edu
Thu Sep 9 16:40:06 EDT 2004
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
More information about the FOM
mailing list