Consider (adapted from this article)

$$ S(x, a, y, b) \text{ means } a \text{ is a factor of } x \wedge b \text{ is a substring of } y $$ where $x, a$ Naturals; $y, b$ strings. Note those are both infinite domains. $S( )$ is true for all Naturals $x$ (for each we have a limited set of choices for $a$); and is true for all strings $y$ (for each we have a limited set of choices for $b$). IOW $a$ depends on $x$; $b$ depends on $y$; but $a$ doesn't depend on $y$ neither does $b$ depend on $x$.

The article tries to express those dependencies as

$$ ∀ x, y ∃ a ∃ b S(x, y, a, b) $$ The pattern $∀ x ... ∃ a ...$ (existential quant inside scope of some other quantification) expresses that $a$ depends on $x$. Then we have a problem: the $∃ b$ is inside scope of $∀ y$ OK; but also inside scope of $x$ and of $a$. So this is saying $b$ depends on $x$ and $a$ which is not what we want to say. (We could re-order the quantifications; we'll get the same problem.) The article claims what we want to say cannot be expressed in FOL; we must introduce a new form of quantification beyond FOL Dependence Logic with a Branching aka Henkin quantifier.

I propose staying within FOL:

$$\begin{align} & \hspace{12pt}( ∀ x ∃ a [ ∀ x', y', a', b'\\ & & [ S(x', y', a', b') \Longrightarrow S(x, y', a, b') ]] )\\ & \wedge ( ∀ y ∃ b [ ∀ x', y', a', b'\\ & & [ S(x', y', a', b') \Longrightarrow S(x', y, a', b) ]] ) \\ & \wedge ( ∀ x, y, a, b, x', y', a', b'\\ & & [ S(x, y, a, b) \wedge S(x', y', a', b')\\ & & \Longrightarrow S(x, y', a, b') \wedge S(x', y, a', b) ] )\\ \end{align} $$ There the only existential quantifiers are within (dependent on) just the variables on which they genuinely depend. All other variables are universally quantified. The third conjunct (all universally quantified) affirms the choice of $x, a$ is indeed independent of the choice of $y, b$.

Did I do something wrong? Or does the example actually not demonstrate the need for Branching quantification?

This question is boiled down from here, for more background.


Convert the proposed formula to Prenex Normal Form. (There's lots of same-named variables, so first consistently rename each to something unique, to avoid inadvertent bindings. After that it's plain sailing, because there's no quantification under negation or implication.)

Moving all the quantification to a prefix will force putting $∀ y ∃ b$ under $∀ x ∃ a$ or vice versa. We're back to the original problem. It might make it worse: depending on the order of moving quantifiers, there might be far more $∀$s in front of the $∃$s.

A PNF is supposed to be logically equivalent.

Objection 1: If the PNF is equivalent, then that third conjunct affirming the independence of $x, a$ vs $y, b$ must still hold. Also there continues to be no predicate application mentioning both $∃\text{-quantified}$ variables. There still isn't an explanation why that doesn't resolve the problem.

Perhaps the syntactic characterisation of dependence as the form $∀ x ... ∃ a$ is an over-simplification? To make $a$ dependent on $x$ requires also that they appear together in a function application or predicate application or equality? Or rather the transitive closure of appearances: $x$ appears under a predicate with $z$; and $z$ appears with $a$; etc.

Objection 2: PNF is only logically equivalent in Classical Logic but not for example in Intuitionist Logic.

Specifically this rule fails

$$ ¬∀ x ϕ \text{ implies } ∃ x ¬ϕ $$ Converting the proposed formula doesn't need that rule (because no quantifiers under negations nor implications); but the effect of the rule (assuming this wff appears nested inside some other quantifier) is for $x$ to become dependent. So yes the syntactic characterisation of dependence must be over-simplifying.

Then is it that PNF preserves logical equivalence; but not dependencies. And/or does Dependence Logic assume a non-Classical logic?

  • 1
    $\begingroup$ This is not an answer to any question as far as I can seel. Please do not use the answer box for things other that, well, answering questions. $\endgroup$ – Mariano Suárez-Álvarez Mar 27 '18 at 17:17
  • $\begingroup$ Is there something wrong with the reasoning here? Please explain so that I can learn and improve the answer. $\endgroup$ – AntC Mar 28 '18 at 4:57
  • 1
    $\begingroup$ Was I not sufficiently clear?! This is not an answer to a question. The answer box is not a good place to write a blog $\endgroup$ – Mariano Suárez-Álvarez Mar 28 '18 at 5:05
  • 1
    $\begingroup$ By now I am pretty sure you have managed to annoy most of the users of this site who know logic, so probably it is a good plan not to hold your breath waiting for someone to actually answer. $\endgroup$ – Mariano Suárez-Álvarez Mar 28 '18 at 5:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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