2
$\begingroup$

I'm puzzled with functional dependency formula in first order logic. It is triggered by

http://rjlipton.wordpress.com/2010/01/17/a-limit-of-first-order-logic/

where there seems to be a confusion between dependency and functional dependency. The expression

$\displaystyle \forall x \exists y : S(x, y) .$

is anything but functional dependency. The formula for functional dependency is

$\displaystyle \forall y_{1} \forall y_{2} \forall x : S(x, y_{1}) \wedge S(x, y_{2}) \implies y_{1} = y_{2} .$

Now, suppose we have ternary predicate Q(x,y,z). How does one express functional dependency y=f(x)?

Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ I do not understand which property of ternary predicate Q you want to express. I know that in the case with binary relation, what you are doing is simply to represent a function by a (binary) relation; or more precisely, you want a first-order expression on the relation S which is satisfied if and only if S represents some function. What is the connection which the function f and the ternary relation Q are supposed to have? $\endgroup$
    – Tsuyoshi Ito
    Feb 4, 2011 at 18:00
  • 1
    $\begingroup$ Lipton isn't talking about databases, he's talking about logic. In $\forall x \exists y: S(x,y)$, you can view the existential quantifier as a function $f$ that takes in the $x$ and gives you the (of possibly many) appropriate $y$. IOW, this is equivalent to $\forall x: S(x,f(x))$. This is called skolemization. $\endgroup$
    – Mark Reitblatt
    Feb 4, 2011 at 18:25
  • $\begingroup$ The predicate $\displaystyle x^2=a \wedge y^2=b .$ that Lipton uses as an example contains two functional dependencies. $\endgroup$
    – Tegiri Nenashi
    Feb 4, 2011 at 19:08
  • 1
    $\begingroup$ @Tegiri The dependency intended was clear from the context, as least to a logician. The desired notion of dependency is precisely the one I described in my comment. Lipton wanted to express that one $\exists$ depended on one $\forall$, and another $\exists$ depended upon another $\forall$. That may not exist in "pure form" in databases, but it certainly does in logic: $\forall x\exists y : x = y$ is a perfectly reasonable expression. $\endgroup$
    – Mark Reitblatt
    Feb 4, 2011 at 22:01
  • 1
    $\begingroup$ @Tegiri, if you answered your own question, you should post the update as an answer and accept it, else as Tsuyoshi points out, it'll keep coming back to haunt us. If you don't do this, we will have to close the question. $\endgroup$
    – Suresh Venkat
    Feb 4, 2011 at 22:08

2 Answers 2

Reset to default
2
$\begingroup$

Apparently, we must project away variable z from ternary relation Q, which is done via existential quantifier:

∀y1∀y2∀x:(∃z:Q(x1,y,z))∧(∃z:Q(x2,y,z))⟹x1=x2.

This is equivalent to standard textbook FD definition:

∀y1∀y2∀x∀z1∀z2:Q(x1,y,z1)∧Q(x2,y,z2)⟹x1=x2.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Your 'standard textbook' definition is good but I think missing an $\Longrightarrow$. The form with $\exists$ also has that missing, and I think the variable names are mixed up(?) Yes it is equivalent (after allowing for that): you can see by converting to Prenex Normal Form.$\hspace{160pt}$ Yes I know this is an old post. I'm interested in the topic and can't find much about it in the wiki-/stack-osphere. Is anybody still listening here? $\endgroup$
    – AntC
    Apr 4, 2018 at 1:51
  • $\begingroup$ Here is a better answer: pdfs.semanticscholar.org/056b/… $\endgroup$
    – jackb
    Oct 20, 2018 at 20:37
2
$\begingroup$

[in the article] there seems to be a confusion between dependency and functional dependency.

The article is using "dependency" in the sense of 'Dependence Logic' here or here. As @Mark R points out. Specifically it's talking about the 'branching or Henkin quantifier'. Yes those are nothing to do with database theory Functional Dependencies. (They might be a little to do with other forms of database Dependencies, see below.)

The expression $∀x∃y:S(x,y).$ ...

is not logically equivalent to $∃y∀x:S(x,y).$ (quantifiers permuted).

The first says (to stick with Lipton's example) 'every number has at least one square root' (True). The second says 'there's a number which is a square root of every number' (False).

But note that for the first formula to be true, requires you pick different numbers for $y$, for each different $x$. That's the sense in which $y$ is dependent.

The predicate $x^2 = a \wedge y^2 = b$ that Lipton uses as an example contains two functional dependencies.

You and I can see that (with our data analyst hats on). Lipton is ignoring it and looking at the (logical) dependency the other way round: having chosen $x$, there's always at least one choice for $a$. Database Dependency Theory has a name for that: it's a MultiValued Dependency.

Futhermore what he's really concentrating on is that $a$ depends on $x$ but not at all on $y$; $b$ depends on $y$ but not at all on $x$. Database Dependency Theory has a name for that, too: Join Dependency. A MultiValued Dependency is a special case. We can write this case as

$$ (JD) S: \bowtie(\{x, a\}, \{y, b\}) $$ That is, the relation representing predicate S can be vertically partitioned into two by projecting on those two pairs of attributes; and when we join them back together ($\bowtie$ symbol), we must get back the original relation value. There's a FOL equivalent for that, similar to your formula for an FD:

$$\begin{align} \forall x, a, y, b, x', a', y', b' & [S(x, a, y, b) \wedge S(x', a', y', b')\\ & \Longrightarrow S(x, a, y', b') \wedge S(x', a', y, b)] \end{align}$$

It seems to me we can use that to give the semantics of Lipton's example. without needing to escape into Second-Order logic. OTOH I think this is such a poorly chosen example, that might not be telling us much about the Branching/Henkin quantifier in general.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.