Re: deductive databases
From: Jan Hidders <jan.hidders_at_REMOVETHIS.pandora.be>
Date: Thu, 26 May 2005 20:18:39 GMT
Message-ID: <zaqle.102192$D24.5938321_at_phobos.telenet-ops.be>
>
> If memory serves, the usual proof goes like this:
>
> Let's take a directed graph encoded as a binary relation R. Let's
> assume that TC(a,b) expresses the transitive closure of R and define
> an infinite set of propositions P0(a,b), P1(a,b), ..., where Pn says
> that there is *no* path of length 'n' from a to b. Now, consider an
> infinite set of propositions
>
> {TC(a,b)} U {P0(a,b), P1(a,b),...}
>
> Each finite subset of these propositions has a model and, by
> compactness, the whole set has a model too, But although TC(a,b) is
> true, in this model there is no path from a to b which means that
> TC(a,b) does not express transitive closure of the relation R.
>
> The EF game shows that transitive closure cannot be expressed in a
> first-order language even on *finite models* ( where the compactness
> theorem fails).
Date: Thu, 26 May 2005 20:18:39 GMT
Message-ID: <zaqle.102192$D24.5938321_at_phobos.telenet-ops.be>
VC wrote:
> "Jan Hidders" <jan.hidders_at_REMOVETHIS.pandora.be> wrote in message
> news:WC7le.101230$Pg5.6146163_at_phobos.telenet-ops.be...
>
>> Ok. I had to go back and do some reading and I think I understand >> now. What I still not understand is how compactness shows in this >> case (or even in the normal case) proves that you cannot express >> the transitive closure.
>
> If memory serves, the usual proof goes like this:
>
> Let's take a directed graph encoded as a binary relation R. Let's
> assume that TC(a,b) expresses the transitive closure of R and define
> an infinite set of propositions P0(a,b), P1(a,b), ..., where Pn says
> that there is *no* path of length 'n' from a to b. Now, consider an
> infinite set of propositions
>
> {TC(a,b)} U {P0(a,b), P1(a,b),...}
>
> Each finite subset of these propositions has a model and, by
> compactness, the whole set has a model too, But although TC(a,b) is
> true, in this model there is no path from a to b which means that
> TC(a,b) does not express transitive closure of the relation R.
Well explained. Thank you for that. Let me check if I really got it. The formula TC(a,b) is assumed to express that there is in R a path from a to b, right? And the reason that there is a model for each finite subset of the infinite set is that if n is the largest number for which Pn(a,b) is in the set, then we let R consist of a path from a to b with length n+1. Correct?
>> The proof for inexpressibility of TC I know works with >> Ehrenfeucht-Fraisse games, so I'm surprised that there is >> apparently a much simpeler way to prove it.
>
> The EF game shows that transitive closure cannot be expressed in a
> first-order language even on *finite models* ( where the compactness
> theorem fails).
Right! I learned my logic mainly in the context of database theory so I sometimes forget that this restriction is not the default.
Thank you again, very helpful.
- Jan Hidders