Pushing in negation in first order logic

Question

Assume you have a formula $$\neg (\forall_y \exists_x p(x,y))$$

Can this formula be rewritten using the $\delta$ rule: $\neg \forall_x A(x)$ rewritten to $\neg A(a)$

Thereby, $\neg (\forall_y \exists_x p(x,y))$ rewrites to $\neg \exists_x p(x,y)$?

I am a little unsure of how to apply this $\delta$ rule properly?

Answer 1

The rules for negating quantifiers are :

$\lnot \forall x \equiv \exists x \lnot$

and :

$\lnot \exists x \equiv \forall x \lnot$.

Thus, the formula :

$¬(∀y \ ∃x \ p(x,y))$ is equivalent to :

$∃y \ ¬ (∃x \ p(x,y))$

that, in turn is equivalent to :

$∃y \ ∀x \ ¬p(x,y).$

---

If you are working with Tableau method, this means that the formula $¬(∀y \ ∃x \ p(x,y))$ will produce a new node $¬ (∃x \ p(a,y))$, with $a$ new.

The intuition is : if we know that $¬(∀y \ ∃x \ p(x,y))$ holds, this means that $∃x \ p(x,y)$ does not hold for every object in the domain. Thus, for some unspecified object $a$, we have that $∃x \ p(x,a)$ does not hold, i.e. that $¬ (∃x \ p(x,a))$ hold.

Answer 2

First, please understand that the $\delta$ rule is not a 'rewrite' rule. Rewriting rules are rules of equivalence, but that is not what you are dealing with here. Rather: in a tableaux/tree method, you are figure out how you can satisfy the truth of statements by assigning truths to some 'component' statement. As such, the rules are seen as 'decomposition' rules, rather than 'rewrite' rules.

Specifically, when the $\delta$ rule says:

$$\neg \forall_x \ \varphi(x)$$

$$\neg \varphi(a)$$

It says that you can satisfy the truth of $\neg \forall_x \ \varphi(x)$ by satisfying the truth of $\neg \varphi(a)$. Simply put: if $\neg \varphi(a)$ is true, then $\neg \forall_x \ \varphi(x)$ will be true as well. Please note that $x$ can be any variable, and $a$ has to be a new/fresh constant: a constant that does not already occur in the branch where the $\neg \forall_x \ \varphi(x)$ occurs. Also, $\varphi(x)$ is any formula containing $x$ as zero or more free variables, and $\varphi(a)$ the result that is obtained by substituting all free variables $x$ with $a$.

So, when in your case we have $\neg \forall_y \exists_x p(x,y)$, then the variable you are working with is $y$, and the formula $\varphi(y)$ is $\exists_x p(x,y)$. So, assuming $a$ is indeed a fresh constant, $\varphi(a)$ is $\exists_x p(x,a)$, and thus in the tree you get:

$$\neg \forall_y \exists_x p(x,y)$$

$$\neg \exists_x p(x,a)$$

So, when you write:

Thereby, $\neg (\forall_y \exists_x p(x,y))$ rewrites to $\neg \exists_x p(x,y)$?

Close! The variable $y$ needs to be replaced with a fresh constant.