MHB How to Prove the Negation of Nested Quantifiers After Instantiation?

[agapito]

Consider the expression:

~ Ex Ay Ez P(x,y,z), where

~ is negation symbol, E existential quantifier, A universal quantifier.

We are asked to prove formally that, after instantiation of x to a, we obtain:

~ Ay Ez P(a,y,z)

How might we go about this? I appreciate all help,

agapito

 

[Evgeny.Makarov]

Consider the following problem: "Suppose we have an expression 1 + 2. Prove that after replacing 2 with (1 + 1), we get 1 + (1 + 1)". It's hard to argue against it: this is just a question of replacing a substring with another substring. So it may not be exactly clear what we are asked to prove.

Note, however, that after replacing we don't get an arbitrary new expression; the numerical value of the new expression is equal to that of the old one: 1 + 2 = 1 + (1 + 1). One could consider a similar problem: "Suppose we have an expression 1 + 2. Prove that after replacing 2 with (1 + 3), we get 1 + (1 + 3)". This is equally true, but it is somewhat strange that we replaced 2 with 1 + 3 = 4, so the value of the new expression is not equal to the value of the old one. Unlike the first problem, replacing 2 with 1 + 3 seems unjustified.

In the same way, logic is about rules manipulating strings of symbols. We define certain rules because they have some meaning: for example, they preserve the truth value of logical formulas. (Formally the choice of rules is justified by the so-called soundness theorem.) But once the rules are chosen, the only question is, "Can we get from this string to that string by following these rules?". You could always replace some substring by any other substring (e.g., instantiate $x$ with $a$), and nobody will doubt that you did that. But the question is whether this is done in accordance with the rules, or whether the new formula has some expected relationship with the old one.

In your problem it seems that what one needs to prove is that $\neg\forall y\exists z\,P(a,y,z)$ logically follows from (or is in some other sense implied by) $\neg\exists x\forall y\exists z\,P(x,y,z)$. This is indeed so, but to approach it you need to clarify the problem statement. Is it about logical (semantic) consequence or about syntactic consequence (derivability)? In the second case you need to provide the logical calculus that is used in your course or book: axioms and rules of inference. But the idea is that $\neg\exists x\ldots$ is equivalent to $\forall x\neg\ldots$, and one can instantiate a universally quantified variable and get a consequence of the formula.

 

[agapito]

Thank you very much for your explanation. I'm actually looking for a proof of the material equivalence

¬∃x∀y∃z P(x,y,z) <---> ∀x ¬∀y∃z P(x,y,z)

in terms of syntactic consequence. My text, Copi's Symbolic Logic shows it as a rule. Does it make sense to inquire if there is some basic principle supporting the rule?

Thanks again for helping me out with this,

agapito

 

[Evgeny.Makarov]

I'm actually looking for a proof of the material equivalence

¬∃x∀y∃z P(x,y,z) <---> ∀x ¬∀y∃z P(x,y,z)

in terms of syntactic consequence. My text, Copi's Symbolic Logic shows it as a rule. Does it make sense to inquire if there is some basic principle supporting the rule?

This is a special case of
\[
\neg\exists x\,A\longleftrightarrow\forall x\,\neg A.\qquad(*)
\]
That this formula is always true is clear: an object satisfying $A$ does not exists iff all objects don't satisfy $A$. As for a syntactic proof, one needs to specify axioms and rules of inference. There is no way around it. There are dozens of logical calculi, just like dozens of programming language, and asking for a formal proof of a formula without specifying a calculus makes as much sense as asking to write an actual program without specifying a language. Wikipedia, for example, lists around 20 calculi only of a certain style and only for propositional logic.

But the equivalence (*) is indeed quite fundamental, and a lot can be said about it.

 

[agapito]

OK, many thanks for your help.