From: FGD <presbeis@my-deja.com>
Subject: Re: Confused with skolemization
Date: Sat, 10 Feb 2001 08:13:04 GMT
Newsgroups: sci.math
Summary: Skolemization; comparative consistency of sets of sentences in languages

In article <962gu4$be6$1@nnrp1.deja.com>,
  plofap@my-deja.com wrote:
> [Stuff about how skolemization can make you fly... ;-)]

So you've seen a theorem which paraphrases:

   Given a language L0 and a set of sentences A of that
   language. If L1 is obtained from L0 by adding a term
   g(x1,...,xn) and  Phi(y,x1,...,xn) is a formula of L
   with all free variables shown, then the sets of
   sentences

      A0 = A U {(Ax1)...(Axn)(Ey)Phi(y,x1,...,xn)}

      A1 = A U {(Ax1)...(Axn)Phi(g(x1,...,xn),x1,...,xn)}

   of L0 and L1 respectively are equiconsitent.

And the proof consisted of constructing a model of A0 from a model of A1
and convesely. There is no problem in constructing a model of A0 from a
model of A1. But the converse is a bit troubling: the good g seems to
drop from the sky somewhere.

Well, you will be glad to know that this is not the only way to prove
this, you will stop being glad once you know what the other proof is
like. I will only biefly outline the proof, since the details would most
likely need much more time than I can give. The proof is completely
syntactical and constructive---all sweat, no miracles.

The first step is to give a faithful reduction of L1 to L0. That is you
construct a map which translates each L1 formula into an equivalent L0
formula. The idea for this map is to replace every L1 formula of the
form

   Psi(g(x1,...,xn),x1,...,xn,xn+1,...,xm)

by a formula of the form

   (Ey)(Phi(y,x1,...,xn) & Psi(y,x1,...,xm))

But things are not quite as simple, you must be careful about your
choice of replacement variables y. You want to make sure that clashes
never occur with "old" variables and you must make sure that your
choices of variables is consistent so that if g(x1,...,xn) occurs twice
in a formula then the two occurnces are replaced by the same variable.
All of this should be done by induction on formula complexity. You may
find it easier to work with an intermediate language L2 which is L1
extended with extra variable symbols (and nothing else) The extra
variables could even be given an idexing scheme which emulates the
functionality of g, that is you define a map which associates with each
term sequence x1,...,xn a variable index i = i(x1,...,xn) the new
variable symbol yi. Such a scheme would guarantee consistency, but there
are other troubles you will have to deal with... No one ever said being
a logician was easy!

Now for the second step, you suppose that A1 is inconsistent. You take a
sample proof of say ~(x = x) from the axioms A1. (See note) Then you
translate this proof into a L0 (or L2) proof of ~(x = x) from A0 which
shows that A0 is inconsistent too. The hard part of this step is to
prove that the translated proof will be a valid proof. How "easy" this
step is depends on how good the translating scheme is. Whenever I have
to do this kind of thing, I use the "back and forth" technique. I write
a preliminary or even incompelete step 1, I then try to do step 2, when
it becomes too hard or even impossible, I go back to step 1 and modify
it to make step 2 work, I retry step 2, and so on until step 2 works.
Finally, I clean up the mess. You may want to use your instructor's
experience to speed up the process, you will have to go back and forth a
few times, don't be afraid to change stuff, I can't count how many times
I've redefined FOL while doing this.

I forgot something really important in the first step, well honestly I
just remebered while writing stuff for step 2. The consistency
requirement for transaltion is not only necessary whithin formulas, but
also within proofs. And it is essential at some point to worry about
provable identities between terms. All of this should be implicit if the
translation is done right. (The emulation of g through an indexing
scheme as mentioned above is a _very_ good idea...)

There you go! At this point, I imagine you're wondering where I got this
proof from, hoping that I could point to a complete proof of the result
somewhere in the literature. Well, I can't! I've been thinking about
this and looking around for a while now, but I can't remember. This is
why I gave so much advice. I promise that if I do remember at some point
in the near future, I'll gladly post a reference, and keep it safely for
the future.

By the way, this was a very good question, not all logic students worry
about these things and they should. The shortest proof is not always the
best (except maybe for instructors and textbook writers). Keep going!

-- Frank


Sent via Deja.com
http://www.deja.com/