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

Question

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

Thank you in advance for your suggestions.

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.

Answer 1

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

Answer 2

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