# Help with proof ¬∀x:X.¬(P⇒Q)⊣⊢∃x:X.(¬P∨Q)

I am working on a propositional calculus proof and I would like to confirm that my proof is correct as I am not familiar with these yet.

EDIT: we are using Mathematics of Discrete Structures for Computer Science by Gordon Pace.

These are the Equivalence Laws that we were given: http://www.filedropper.com/laws

According to Peter Smith's comment on his answer below:

From what's available by way of online excerpts, Pace seems to be using a standard Natural Deduction system, with subproofs

¬∀x:X.¬(P⇒Q)⊣⊢∃x:X.(¬P∨Q)


My main reason for worrying is that these proofs seem to be the opposites of each other.

1   ¬∀x:X.¬(P⇒Q)    hypothesis
2   ∃x:X.¬¬(P⇒Q)    ∃x:X.P ≡ ¬∀x:X.¬P
3   ¬¬(P⇒Q)[x\x]    ∃ elimination
4   ¬¬(P⇒Q)         P ≡ P[x\x]
5   P⇒Q             double negation
6   ¬P∨Q            P⇒Q ≡ ¬P∨Q
7   (¬P∨Q)[x\x]     P ≡ P[x\x]
8   ∃x:X.(¬P∨Q)     ∃ introduction

o//o proven for LHS

9   ∃x:X.(¬P∨Q)     hypothesis
10  (¬P∨Q)[x\x]     ∃ elimination
11  ¬P∨Q            P ≡ P[x\x]
12  P⇒Q             P⇒Q ≡ ¬P∨Q
13  (P⇒Q)[x\x]      P ≡ P[x\x]
14  ∃x:X.(P⇒Q)      ∃ introduction
15  ¬∀x:X.¬(P⇒Q)    ∃x:X.P ≡ ¬∀x:X.¬P

o//o proven for RHS


UPDATE:

I have a "model answer" for a similar problem.

∀x:X.¬(P^Q)⊣⊢∃x:X.¬(¬P∨¬Q)

1   ∀x:X.¬(P^Q)                 hypothesis
2   ¬(P^Q)[x\x]                 ∀ elimination
3   ¬(P^Q)                      P ≡ P[x\x]
4   ∃x:X.¬(¬P∨¬Q)           assume
5   ¬(P^Q)                  copy 3
6   ∃x:X.¬(¬P∨¬Q)           assume
7   ¬(¬P∨¬Q)            sub-hypothesis
8   ¬(P^Q)              De Morgan's law
9   ¬(¬P∨¬Q)⇒(P^Q)          ⇒ introduction on 7-8
10  (¬(¬P∨¬Q)⇒(P^Q))[x\x]   P ≡ P[x\x]
11  ∀x:X.((¬(P^Q))⇒(P^Q))   ∀ introduction
12  P^Q                     ∃ elimination using 6
13  ∃x:X.¬(¬P∨¬Q)               ¬ introduction by contradiction using 4-5, 6-12

o//o proven for LHS

14  ∃x:X.¬(¬P∨¬Q)               hypothesis
15  ∀x:X.(¬P∨¬Q)                ∃x:X.P ≡ ¬∀x:X.¬P
16  (¬P∨¬Q)[x\x]                ∀ elimination
17  ¬P∨¬Q                       P ≡ P[x\x]
18  ¬P                      assume
19 P^Q                  sub-hypothesis
20 P                    ^ elimination type 1 on 19
21 P^Q                  sub-hypothesis
22 ¬P                   copy 18
23  ¬(P∨Q)                  ¬ introduction by contradiction using 19-20, 21-22
24  ¬Q                      assume
25  P^Q                 sub-hypothesis
26  Q                   ^ elimination type 1 on 25
27  P^Q                 sub-hypothesis
28  ¬Q                  copy 24
29  ¬(P∨Q)                  ¬ introduction by contradiction using 25-26,27-28
30  ¬(P^Q)                      V elimination using 18-23, 24-29
31  ¬(P^Q)[x\x]                 P ≡ P[x\x]
32  ∀x:X.¬(P^Q)                 ∀ introduction

o//o proven for LHS


In an alternate method, steps 18 - 29 could be avoided by using De Morgan's law where

¬(P^Q) ≡ (¬P∨¬Q)


Thanks in advance for looking into this.

Final update: I have managed to avoid doing this question, but thanks to all the people who tried to help me. I'll look at the answers right now and mark the best one for future reference.

-
I removed the "propositional calculus" - as you are working with predicate calculus (given your reference in a comment. Unfortunately, there is no tag for predicate-calculus. –  amWhy Jan 4 '13 at 16:14
Heavens! Who on earth produced that "model answer"? Complain to your instructor as it really is simply awful -- it really is a straight "fail" answer, I'm afraid. –  Peter Smith Jan 5 '13 at 14:27
I'd love to, believe me. But for now this is all I have. However, 1) why is it a "fail" answer? Is it wrong or just badly formed? 2) given that model answer, do you think mine is good? –  4th guy Jan 5 '13 at 14:32
The model answer is so far from right that you need to start from scratch. I can only suggest reading a good book on Natural Deduction. The excerpts I can see from Pace's book look OK. But I''d recommend Paul Teller's Modern Formal Logic Primer as reliable, lucid, and now free: you can download chapters from tellerprimer.ucdavis.edu –  Peter Smith Jan 5 '13 at 15:12

1. Whatever else this is, this isn't propositional calculus -- as the propositional calculus lacks individual quantifiers.
2. You don't say what/whose system of predicate calculus you are using (textbook reference? the notation is unfamiliar to me), but I know no system which allows existential quantifier elimination in the form you seem to be using it.

A normal deduction of this sort of thing, using "introduction" and "elimination" rules, would look more like this:

1 $\quad\neg\forall x \neg (\varphi(x) \to \psi(x))$

2 $\quad\exists x (\varphi(x) \to \psi(x))$

3 $\quad|\quad (\varphi(a) \to \psi(a))\quad$ Assumption

4 $\quad|\quad (\neg\varphi(a) \lor \psi(a))\quad$ $\to/\lor$

5 $\quad|\quad \exists x(\neg\varphi(x) \lor \psi(x))\quad$ $\exists$-introduction

6 $\quad \exists x(\neg\varphi(x) \lor \psi(x))\quad$ $\exists$-elimination, from 2 and subproof 3 -- 5

-
1. Sorry, I think I should have written Predicate calculus encyclopediaofmath.org/index.php/Predicate_calculus 2. We weren't told what this is in class yet, so I can't provide information on that. Sorry. –  4th guy Jan 4 '13 at 16:11
The notation and the proof-system in that link are quite different from what is displayed in the proofs in the question. The link is to a standard Hilbert system: but it is natural deduction systems that have introduction and elimination rules for quantifiers. –  Peter Smith Jan 4 '13 at 16:15
Well, this is the book that we have been referred to: Mathematics of Discrete Structures for Computer Science by Gordon Pace. –  4th guy Jan 4 '13 at 17:03
@4thguy Thanks I'll check it out ... –  Peter Smith Jan 4 '13 at 17:21
From what's available by way of online excerpts, Pace seems to be using a standard Natural Deduction system, with subproofs (the sort of thing involved in my schematic proof above and conspicuously missing from your suggested proofs). –  Peter Smith Jan 4 '13 at 17:35
show 1 more comment

Your proof looks like a good start, to me, and it is very thorough! Usually, quantifiers are used with predicates, e.g. $$\lnot \forall x.\lnot(P(x)\rightarrow Q(x)),$$ and then, $$\exists x. \lnot\lnot(P(x)\rightarrow Q(x)),$$ etc., so your notation is a bit unconventional.

But I understood well enough that your notation is to be taken as predicates about a quantified $x\in X$, which you (existentially) instantiate some "a" to stand in for "some x", then proceed, until you eliminate the instantiated "a" back to an existentially quantified $x$.

Also, when instantiating an existential quantifier, one usually does so with a "subproof": indented, to help delineate the scope in which it is instantiated.

That said, the logic of your proof follows clearly enough.

Regarding your worries: When you have an equivalence (to prove), the steps for the first implication are sort of (for lack of a better term) "reversed" ("opposite") when proving the second implication. That's partly due to the nature of double implication / equivalence, and the fact that the logical manipulation in your proof (apart from quantifier elimination/introduction) involved only equivalencies (identities).

Nice job of showing your work. And kudos for making the effort to justify all your steps in your proof!

Regarding your Edit: you really ought to include subproofs in your proof: as you are introducing an assumption when you eliminate/instantiate the existentially quantified statement, and need to indicate the scope of that instantiation by indentation, and then end the subproof by reintroducing the existential quantifier (citing the subproof in you justification). Perhaps you can follow the logic here (Note, however, as in Peter Smith's answer, predicates are typically written with an argument (variable or constant):

¬∀x:X.¬(P⇒Q)⊣⊢∃x:X.(¬P∨Q)

1   ¬∀x:X.¬(P⇒Q)    hypothesis
2   ∃x:X.¬¬(P⇒Q)    ∃x:X.P ≡ ¬∀x:X.¬P (1)
|3 ¬¬(P⇒Q) assumption (P ≡ P[x\x])
|4  P⇒Q    double negation (3)
|5  ¬P∨Q   P⇒Q ≡ ¬P∨Q (4)
|6 ∃x(¬P∨Q)    ∃ introduction  (P ≡ P[x\x])
7   ∃x:X.(¬P∨Q) ∃ elimination (2) & (3 - 6)

o//o proven for LHS

9   ∃x:X.(¬P∨Q) hypothesis
|10 (¬P∨Q) assumption ((P ≡ P[x\x]))
|11  P⇒Q   P⇒Q ≡ ¬P∨Q (2)
|12 ∃x(P⇒Q)    ∃ introduction  (P ≡ P[x\x])
13  ∃x:X.(P⇒Q)  ∃ elimination (9) & (10-12)
14  ¬∀x:X.¬(P⇒Q)    ∃x:X.P ≡ ¬∀x:X.¬P

o//o proven for RHS

-
In what system from what textbook are these well-formed proofs? No standard one known to me -- though I'm always ready to hear of new ones! –  Peter Smith Jan 4 '13 at 16:18
4th guy: If you have any more questions, feel free to comment/ask! –  amWhy Jan 5 '13 at 13:48
I don't think there are sub-proofs, unless I'm not understanding correctly. –  4th guy Jan 5 '13 at 14:35
What I mean is "indented" to show scope of the instantiation: but you can do fine without, it just helps clarify the part of the proof in which you are manipulating an instantiated existential quantifier. –  amWhy Jan 5 '13 at 14:43
Unless the solution is wrong, I'd rather not mess with indentation. My head is already hurting by going through all these possible answers. –  4th guy Jan 5 '13 at 15:00