Prove $\exists x p(x) \implies ¬ \forall x q(x)$ from premise $\forall x (p(x) \implies ¬ q(x))$

Solution 1:

Adding to Mauro ALLEGRANZA comment I am going to use a modified version of the Fitch system I was taught.

First I am going to look at our conclusion: $\exists x(p(x)) \to \lnot \forall x(q(x))$ which is equivalent to $\exists x(p(x)) \to \exists x(\lnot q(x))$ because of DeMorgan's law and going further we know that $\lnot p \lor q \equiv p \to q$, so we will apply this to what we have in question making: $\lnot \exists x(p(x)) \lor \exists x(\lnot q(x))$ and using DeMorgan's again we get: $\forall x(\lnot p(x)) \lor \exists x(\lnot q(x))$.

What Mauro is saying is that we should assume the opposite of this so we can draw a contradiction and this will say everything we stated is false, therefore we negate what we stated and we get what we want.

$$1.\space \forall x(p(x) \to \lnot q(x)) \qquad \text{Premise.}\\ \boxed{2.\space \exists x(p(x)) \land \forall x(q(x)) \qquad \text{Assumption} \\ 3.\forall x(q(x)) \qquad \text{$\land$-elim (2)} \\ 4.\space \exists x(p(x)) \qquad \text{$\land$-elim(2)} \\ \boxed{5.\space a \space p(a) \qquad \text{assumption} \\ 6.\space p(a) \to \lnot q(a) \qquad \text{$\forall$-elim (1)} \\ 7.\space \lnot q(a) \qquad \text{$\to$-elim(5,6)} \\ 8.\space \exists x(\lnot q(x)) \qquad \text{$\exists$-intro(7)}} \\ 9.\space \exists x(\lnot q(x)) \qquad \text{$\exists$-elim(4,5-8)} \\ 10. \space \exists x(\lnot q(x)) \lor \forall x(\lnot p(x)) \space \space \text{$\lor$ -intro (9)} \\ 11.F \qquad \text{$\lnot$-elim (2,10)} } \\ 12. \lnot(\exists x(p(x)) \land \forall x(q(x))) $$

We end with what we want! If we take more of DeMorgan's laws and logical equivalences: $$\begin{align} \lnot(\exists x(p(x)) \land \forall x(q(x))) \\ \equiv \forall x(\lnot p(x)) \lor \exists x(\lnot q(x)) \\ \equiv \lnot(\forall x(\lnot p(x))) \to \exists x(\lnot q(x)) \\ \boxed{\equiv \exists x(p(x)) \to \exists x (\lnot q(x)).} \end{align}$$

I wanted to note some of the operations and logic I did with this system. We assume the opposite of what we want on line $2$. With the $\land$ elimination we can get both sides as true because in order for a $\land$ to be true both premises must be true. Line $5$ we assume there is a variable named $a$ that makes $p(a)$ true meaning there is only one variable which let's us apply the $\forall$ elimination. On line $8$, we introduce that there does indeed exist a variable that makes $\lnot q(a)$ true. Line $10$ we can introduce $\lor$ anything we want since we know that at least one premise is true.

Hope this helps, and maybe you can apply this to your Fitch system.

Solution 2:

Due to "x" being a free variable, I believe utilizing some witty placeholder substitution via universal elimination may be a step I need to explore. - qxzsilver

Yes. That is the correct process.

You will first need to raise a witness variable, somehow. Well, you appear to be using Stanford Logica's proof checker which implements Existential Elimination by: checking a line with an existential statement, clicking 'Existential Elimination', to instantiate the predicate with a new witness variable: eg q([c1]) or such.

Once that is done, then you may use 'Universal Elimination' to instantiate a universal statement's predicate to the same term.

The skeleton of the proof is to take AX:(p(X) => ~q(X)) as a premise, and use a conditional proof to derive EX:q(X) => ~AX:q(X).

That requires raising EX:q(X) as an assumption, then derive ~AX:q(X) so you may then use Introduction Introduction. Existential Elimination will be involved inside this sub-proof.

You thus need to derive ~AX:q(X) using negation introduction; the implementation of which in Stanford Logica requires two implications each with AX:q(X) as their antecedents, and having contradictory consequents. For this, AX:q(X) => p([c1]) and AX:q(X) => ~p([c1]) will do nicely, because these can readily be derived.

Well, that will get you started, so I'll leave the rest to you.

1. AX:(p(X) => ~q(X))            Premise
    2. EX:p(X)                   Assumption
    3. p([c1])                   Existential Elimination: 2
    :
    10. AX:q(X) => ~p([c1])      Implication Introduction: 4, 9
    :
    13. AX:q(X) => p([c1])       Implication Introduction: 11, 12
    14. ~AX:q(X)                 Negation Introduction: 13, 10
15. EX:p(X) => ~AX:q(X)          Implication Introduction: 2, 14