3
$\begingroup$

Why is it not possible to represent transitive closure in First Order Logic?

I am learning about translating from Description logic to FOL. In description logic, it is possible to have transitive closure but i am wondering how it is possible in FOL. I found that it is not possible with FOL. The reason I found is " as a consequence of compactness theorem, it is not possible". I couldn't understand its meaning.

$\endgroup$
1
  • $\begingroup$ Because you would need an infinite formula listing all the possible cases of transitivity of all possible variables. $\endgroup$
    – Demosthene
    May 17, 2015 at 11:11

1 Answer 1

Reset to default
4
$\begingroup$

The context is as follows:

Given relation symbols $R, \overline R$, suppose there were a formula $\phi(R,\overline R)$ expressing that $\overline R$ is the transitive closure of $R$. Consider furthermore the constant symbols $c_1, c_2$ and construct the theory comprising $\phi(R,\overline R), c_1 \mathrel{\overline R} c_2$, and for each $n \in \Bbb N = \Bbb Z_{\ge 0}$: $$\neg (\exists x_1\ldots x_n : c_1 \mathrel R x_1 \mathrel R \cdots \mathrel R x_n \mathrel R c_2)$$ where I abused some notation for brevity's sake. This is manifestly inconsistent.

By the Compactness Theorem, a finite set of these is already inconsistent. It does not require a lot of thought, however, to see that any finite set is consistent.

Thus $\phi$ cannot exist.

$\endgroup$
2
  • $\begingroup$ why do you need negation? are you trying to check does it entail any given theory? $\endgroup$
    – Proton Boss
    May 17, 2015 at 13:23
  • $\begingroup$ $\phi$ says that one of infinitely many possibilities has to be true. Subsequently I add the negation of all these possibilities to the theory under consideration, so that it becomes inconsistent. Here, theory is used in its model-theoretic sense: just a set of formulas whose models we want to study. $\endgroup$
    – Lord_Farin
    May 17, 2015 at 13:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .