Predicate calculus-is there a way to prove that a false term can implicate anything and is therefore true?

Question

I'm currently trying to solve the following:

(∃x(¬A(x))) → [∀x (A(x)) → B(z) ]

using only the rules of predicate and propositional calculus. I've had a few stabs at the problem. My chief idea has to do with the A(x) statements. I understand that if there exists at least one false A(x), then A(x) is not all true. I understand that falsities can imply anything. How do I join these two ideas together with the proper formal logical notation?

For example, I first assume:

(∃x(¬A(x)))

which means:

    [∀x    (A(x)) → B(z)   ]           (=> E)
        [∀x    (A(x))]              (assume)
        A(a)                        (∀E)
        F

So I have proved it's false. Now what?

I realise that there is a very good chance I am barking up the wrong tree but I cannot see any other way to prove this. B(z) is totally unrelated to A(z) and while existential elimination will let me arrive at a "q" statement, I do not see how I can get "q" from the other two terms.

Answer 1

You're being a bit inconsistent with parenthesis in the statement you're trying to prove, and maybe your notation is a bit unclear. But the idea is correct.

What you're basically relying on is the DeMorgan theorem for quantifiers, that is the fact that $\exists x(\neg\phi(x)) \leftrightarrow \neg\forall x(\phi(x))$. The proof may be a bit difficult to word in a natural way since we're doing a conditional proof twice and also in doing that we're throwing in an assumption that we're using in RAA.

In addition it might seem a bit odd too that we assume something that directly contradicts what we're already have assumed, but that's perfectly allowed.

If we write it using symbols instead it may be a bit more "clear":

$$\begin{align} \tag{1}\exists x(\neg A(x)), \forall x(A(x))&\vdash \exists x(\neg A(x)) &\text{ Assumption}\\ \tag{2}\exists x(\neg A(x)), \forall x(A(x))&\vdash \neg\forall x(A(x)) &\text{ Assumption}\\ \tag{3}\exists x(\neg A(x)), \forall x(A(x))&\vdash \forall x(A(x)) &\text{ DeMorgan(1)}\\ \tag{4}\exists x(\neg A(x)), \forall x(A(x))&\vdash B(z) &\text{ RAA(2,3)}\\ \tag{5}\exists x(\neg A(x))&\vdash\forall x(A(x)) \rightarrow B(z) &\text{ Cond(4)}\\ \tag{6}&\vdash \exists x(\neg A(x)) \rightarrow (\forall x(A(x) \rightarrow B(z)) &\text{ Cond(5)} \end{align}$$

To be clear here, in formal logic we're not concerned with statements being true or false, we're concerned with statements being proved (possibly under a set of conditions to the left of $\vdash$ symbol). What RAA then is about is that if we have proven $\phi$ and $\neg\phi$ we can conclude $\psi$.

Answer 2

Here is a natural deduction proof (somehow informally stated). The details of the proof may vary according to how exactly your proof system is stated, but the following derivation should offer a good blueprint for adapting it to various proof systems.

The goal is to prove: $(\,\exists x\ \lnot A(x)\,)\ \to\ [ \,(\forall x\ A(x))\to B(z) \,]$.

1) Assume $\exists x\ \lnot A(x)$.

Now the goal is to prove: $(\forall x\ A(x))\to B(z)$ from assumption 1).

2) Assume $\forall x\ A(x)$.

Now the goal is to prove: $B(z)$ from assumptions 1) and 2).

3) From 1), by instantiation of a existentially quantified formula, you get: $\lnot A(t)$, where $t$ is a term not appearing in the proof so far.

4) From 2), by instantiation of a universally quantified formula, you get $A(t)$.

5) From 4), by inserting a disjunction, you get $A(t)\lor B(z)$.

6) From 3) and 5), by "disjunctive syllogism", you get $B(z)$.

Now you discharge the assumption and you get the desired result, i.e.

7) By discharging assumption 2), you get: $(\forall x\ A(x))\to B(z)$.

8) By discharging assumption 1), you get: $(\,\exists x\ \lnot A(x)\,)\ \to\ [ \,(\forall x\ A(x))\to B(z) \,]$.