Re: free variables in FOL



Pierre Asselin wrote:
> 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 ?

Not necessarily valid, but at least symmetric, but only if
(to me) the rules can be rewritten:

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

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

because the scope of the universal quantification is different
otherwise. In the first it's local to the F, in the second over
both. Of course G has no free occurrences of x. Does that mean
you can either universalize just the formula in which it is free
or the entire statement, as you prefer?

Sorry I'm late, my Mac went on the fritz Fri. nite. I must need to
get a life because I was completely at loose ends.

Thanks.

Ken
>
>
> > 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: Attempts to Refute Cantors Uncountability Proof?
    ... unable to prove true statements about objects defined in the system. ... Both universal quantification and existential ... Just because the theory is incomplete doesn't mean it ... And even if you removed universal quantification from ZF, ...
    (sci.math)
  • Re: how to define Thm in PRA
    ... I WAS aware that the object language didn't contain variables ... your schematic variables have THIS ... language is because it requires universal quantification ...
    (sci.logic)
  • Re: Ramification Schema.
    ... What do you intend 'F' to mean? ... allowed to be free variables in 'F' other than 'y' and 'z', ... 'u' might be free in 'F' and within the scope of a quantification ...
    (sci.math)
  • Re: Looking for true (and/or provable) statements of the ZF theory
    ... > formula with the right free variables ... (Does there exist a subset of naturals S with no predicate Phi ... The first order theory ZF does not permit quantification over ... false when Phi is a tautology, regardless of what variables are free in ...
    (sci.math)
  • Re: Ramification Schema.
    ... What do you intend 'F' to mean? ... free variables in 'F' other than 'y' and 'z'? ... 'u' might be free in 'F' and within the scope of a quantification ...
    (sci.math)