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

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

<p>This is equivalent to standard textbook FD definition:</p>

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

CC BY-SA 3.0
2018-04-04T01:51:54.237Z
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?
AntC
CC BY-SA 4.0
2018-10-20T20:37:26.127Z
Here is a better answer: https://pdfs.semanticscholar.org/056b/9c2633693426196c43000b73726cb2be7c76.pdf
jackb
CC BY-SA 2.5
2011-02-04T23:16:52.420Z
2011-02-05T00:11:40.770Z
2011-02-05T00:11:40.770Z
Tegiri Nenashi
<blockquote>
  <p>[in the article] there seems to be a confusion between dependency and functional dependency.</p>
</blockquote>

<p>The article is using "dependency" in the sense of 'Dependence Logic' <a href="https://plato.stanford.edu/entries/logic-dependence/" rel="nofollow noreferrer">here</a> or <a href="https://en.m.wikipedia.org/wiki/Dependence_logic" rel="nofollow noreferrer">here</a>. As @Mark R points out. Specifically it's talking about the <a href="https://en.m.wikipedia.org/wiki/Branching_quantifier" rel="nofollow noreferrer">'branching or Henkin quantifier'</a>. 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.)</p>

<blockquote>
  <p>The expression $∀x∃y:S(x,y).$ ...</p>
</blockquote>

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

<p>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).</p>

<p>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.</p>

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

<p>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.</p>

<p>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</p>

<p>$$
(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:</p>

<p>$$\begin{align}
\forall x, a, y, b, x', a', y', b' &amp; [S(x, a, y, b) \wedge S(x', a', y', b')\\ &amp; \Longrightarrow S(x, a, y', b') \wedge S(x', a', y, b)]
\end{align}$$</p>

<p>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.</p>

CC BY-SA 3.0
2018-04-06T06:48:19.430Z
2018-04-06T06:48:19.430Z
AntC
<p>I'm puzzled with functional dependency formula in first order logic. It is triggered by</p>

<p><a href="http://rjlipton.wordpress.com/2010/01/17/a-limit-of-first-order-logic/" rel="nofollow">http://rjlipton.wordpress.com/2010/01/17/a-limit-of-first-order-logic/</a></p>

<p>where there seems to be a confusion between <em>dependency</em> and <em>functional dependency</em>. The expression </p>

<p>$\displaystyle \forall x \exists y : S(x, y) .$</p>

<p>is anything but functional dependency. The formula for functional dependency is</p>

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

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

CC BY-SA 2.5
2011-02-04T18:00:32.980Z
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?
Tsuyoshi Ito
CC BY-SA 2.5
2011-02-04T18:25:11.183Z
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.
Mark Reitblatt
CC BY-SA 2.5
2011-02-04T19:08:34.033Z
The predicate $\displaystyle x^2=a \wedge y^2=b .$ that Lipton uses as an example contains two functional dependencies.
Tegiri Nenashi
CC BY-SA 2.5
2011-02-04T19:48:46.990Z
I am not sure if the last paragraph really solved what you had asked.  Sounds like something different.  Anyway this question does not seem relevant any longer.  What should we do?  I do not want to keep irrelevant questions dangling around (because non-closed questions with no accepted answers are automatically bumped once in a while).
Tsuyoshi Ito
CC BY-SA 2.5
2011-02-04T21:40:24.063Z
DB people were quickly to point out that I should have consulted textbook for FD definition (rather than wikipedia). Anyway, replying to Mark, DB theory provides some insight into the nature of dependencies. Lipton (and Terry Tao) failed to clarify what kind of dependency are they looking for: is it functional dependency or join dependency? DB theory also emphasizes importance of domain dependence: the expression forany x exists y : S(x,y) is domain dependent; it never occurs in pure form. Its domain independent reincarnation is forany x exists y : R(x) -> S(x,y)
Tegiri Nenashi
CC BY-SA 2.5
2011-02-04T22:01:45.037Z
@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.
Mark Reitblatt
CC BY-SA 2.5
2011-02-04T22:08:17.437Z
@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.
Suresh Venkat
CC BY-SA 2.5
2011-02-04T22:49:43.883Z
@Tegiri, I agree with Mark, you are missing the context in his post. Please fix that part of your question. Thanks.
Kaveh
CC BY-SA 2.5
2011-02-05T00:25:46.863Z
Mark, perhaps I went too far suggesting that for their purpose Lipton (and Terry) might have considered "exists unique" quantifier, instead of just "exists". Then, the required proposition is expressible in first order logic!
Tegiri Nenashi
<lo.logic><db.databases>
First order expression for functional dependency
Tegiri Nenashi
# First order expression for functional dependency

(Asked by: username_0 on 2011-02-04)

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)?

**Tags:** lo.logic, db.databases
> **Comments:**
> **username_1**: 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?  
> **username_2**: 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.  
> **username_0**: The predicate $\displaystyle x^2=a \wedge y^2=b .$ that Lipton uses as an example contains two functional dependencies.  
> **username_1**: I am not sure if the last paragraph really solved what you had asked.  Sounds like something different.  Anyway this question does not seem relevant any longer.  What should we do?  I do not want to keep irrelevant questions dangling around (because non-closed questions with no accepted answers are automatically bumped once in a while).  
> **username_0**: DB people were quickly to point out that I should have consulted textbook for FD definition (rather than wikipedia). Anyway, replying to Mark, DB theory provides some insight into the nature of dependencies. Lipton (and Terry Tao) failed to clarify what kind of dependency are they looking for: is it functional dependency or join dependency? DB theory also emphasizes importance of domain dependence: the expression forany x exists y : S(x,y) is domain dependent; it never occurs in pure form. Its domain independent reincarnation is forany x exists y : R(x) -> S(x,y)  
> **username_2**: @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.  
> **username_3**: @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.  
> **username_4**: @Tegiri, I agree with Mark, you are missing the context in his post. Please fix that part of your question. Thanks.  
> **username_0**: Mark, perhaps I went too far suggesting that for their purpose Lipton (and Terry) might have considered "exists unique" quantifier, instead of just "exists". Then, the required proposition is expressible in first order logic!  

---

## 2 answers

### Answer by username_0 on 2011-02-04. Score: 2 | Accepted answer

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.

> **Comments:**
> **username_5**: 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?  
> **username_6**: Here is a better answer: https://pdfs.semanticscholar.org/056b/9c2633693426196c43000b73726cb2be7c76.pdf  

---

### Answer by username_5 on 2018-04-06. Score: 2

> [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](https://plato.stanford.edu/entries/logic-dependence/) or [here](https://en.m.wikipedia.org/wiki/Dependence_logic). As @Mark R points out. Specifically it's talking about the ['branching or Henkin quantifier'](https://en.m.wikipedia.org/wiki/Branching_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.


---

