Re: free variables in FOL

Ken Quirici <kquirici@xxxxxxxxx> wrote:
> MathWorld has the following two rules of inference in FOL:

> if G=>F(x)
> then G=>AxF(x)

> if F(x)=>G
> then ExF(x)=>G

> where in both cases x is unbound/free in F and doesn't occur free in G.

> Why in one case does 'free' lead to universal quantification and in
> the other to existential quantification?

If you rewrite the formulas in prenex form, the second conclusion
becomes Ax(F(x) => G) . Does that seem more symmetric to you ?


> How can free variables pop up at all in any sentential formulae? What
> do they mean?

One of the books I have makes the distinction between *variables* and
*names*. The inference rules above are given as

If (G => F(c)) is valid,
then (G => AxF(x)) is valid.

and

If (F(c) => G) is valid,
then (ExF(x) => G) is valid.

The "c" is not a variable but a name, a non-logical symbol of the
language just like F() and G. When the language is interpreted,
the c has to be assigned an individual in the domain of model, just
like the F() is assigned a subset of the domain and G is assigned
a truth value (except that F() and G may have more internal structure
than shown and if so it is their constituents that must be
interpreted).

If you read "valid" as "true in every interpretation" you can
convince yourself that the two inference rules preserve validity.

If you don't want to bother with the variable/name distinction you
can probably just read formulas with free variables as universally
quantified implicitly. But it is the *entire formula*, not just
a fragment of it, that is so quantified. Therefore,

F(x) => G

is shorthand for

Ax ( F(x) => G )

and not for

(Ax F(x)) => G


--
pa at panix dot com
.

Relevant Pages

  • Re: Godels comments about the "true reason" for incompleteness
    ... arbitrary Q. Obviously there is an implied quantification over Q, ... letters of the object language). ... we want to convey that "all" propositions follow from a contradiction. ... refutable in PA and as confirmed by the supposed undecidability of S. ...
    (sci.logic)
  • Re: Godels comments about the "true reason" for incompleteness
    ... why not formally admit propositions ... arbitrary Q. Obviously there is an implied quantification over Q, ... letters of the object language). ... refutable in PA and as confirmed by the supposed undecidability of S. ...
    (sci.logic)
  • Re: Godels comments about the "true reason" for incompleteness
    ... arbitrary Q. Obviously there is an implied quantification over Q, ... letters of the object language). ... quantified over in the meta-language (if the meta-language is first ... propostion, which must be specified by construction) or else it is ...
    (sci.logic)
  • Re: Rules of deduction.
    ... derived from words in spoken language, eg. if, not, all, some. ... The rules of inference in symbolic logic are derived from methods ... it is very interesting to see how quantification differs ... modern logics. ...
    (talk.origins)
Loading