Please note that the following is not a duplicate:
Why negating universal quantifier gives existential quantifier?
I am asking for a particular type of formal proof. I have added the alternative-proof tag because I can prove it one way, but I would like another way.
I have recently had the pleasure of finding Proof Checker. I want to brush up on my logic – in which I am entirely self-taught – and in doing so, I found that I am stuck trying to prove
$$(\lnot\forall xPx)\to(\exists y(\lnot Py)).\tag{1}$$
Well, when I say "prove", I mean using the following rules:
- modus ponens ->E
- modus tollens MT
- modus tollendo ponens DS
- double negation DNE
- addition vI
- adjunction ^I
- simplification ^E
- bicondition <->I
- equivalence <->E
- repeat Rep
- conditional derivation ->I
- reductio ad absurdum RAA
- universal instantiation AE
- universal derivation AI
- existential instantiation EE
- existential generalization EI
- identity introduction =I
- substitution of identicals =E
. . . in a "Fitch-style" proof.
These rules can be found on the Proof Checker site.
I know the following.
Suppose the opposite. Then $$\lnot((\lnot\forall xPx)\to(\exists y(\lnot Py))).$$ The only way for an implication to be false is for its assumption to be true, $\lnot\forall xPx$, while its conclusion is false, $\lnot(\exists y(\lnot Py))$. From the former, we have $\lnot Pa$ for some $a$. From the latter, we have $\lnot\lnot Pa$, from which we have $Pa$, a contradiction.
This is the written form of the method of analytic tableaux applied to $(1)$; namely:
$$\begin{array}{ccc}
1. & \lnot(\lnot\forall xPx\to\exists y\lnot Py) & \,\\
2. & \lnot\forall xPx & (1)\\
3. & \lnot \exists y\lnot Py & (1)\\
4. & \lnot Pa & (2)\\
5. & \lnot\lnot Pa & (3)\\
6. & Pa & (5)
\end{array}$$
It seems to assume (at least in the metalogic) what I set out to prove. I don't know how to convert this to a formal proof.
For what it's worth (and I think it's worth very little), I suppose the proof starts out like (or contains) this:
$$\frac{|1. \lnot \forall xPx}{\vdots}.$$
That is, I can start (a subproof) by assuming $\lnot\forall xPx$. My problem is that, as far as I can see, none of the given rules allows me to go from $\lnot\forall xPx$ to $\lnot Pa$, which is what I am guessing is the next line, especially if the tableaux method is anything to go by.
Please help 🙂
Best Answer
No, start exactly as the tableau suggests, by first assuming the antecedent is true and the consequent is false, then assuming $\neg Pa$ holds for an arbitrary variable ($a$). Â Everything else derives from discharging those assumptions.
So, as the third assumption contradicts the second assumption (via Existential Generalisation), we may discharge the third assumption with RAA to deduce $Pa$.
Next, since $a$ is arbitrary, that now contradicts the first assumption (via Universal Derivation), so we may discharge the second assumption with RAA to deduce the desired conclusion.
Finally, we may discharge the first assumption with Conditional Derivation, wrap it all up and put a bow on top.
$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \qquad{\fitch{}{\fitch{~~1.~\neg\forall x~Px}{\fitch{~~2.~\neg\exists y~\neg Py}{\!\begin{array}{|l}\!\fitch{~~3.~\neg Pa}{~~4.~\exists y~\neg Py\hspace{7ex}\textrm{Existential generalisation}~3\\~~5.~\neg\exists y~\neg Py\hspace{5.5ex}\textrm{Repetition}~2}\\\!~~6.~Pa\hspace{15.5ex}\textrm{Reductio Ad Absurdum}~3{-}5\end{array}\\~~7.~\forall x~Px\hspace{12.25ex}\textrm{Universal derivation}~6\\~~8.~\neg\forall x~Px\hspace{10.5ex}\textrm{Repetition}~1}\\~~9.~\exists y~\neg Py\hspace{14ex}\textrm{Reductio Ad Absurdum}~2{-}8}\\10.~\neg\forall x~Px \to \exists y~\neg Py\hspace{6ex}\text{Conditional derivarion}~1{-}9}\\\blacksquare}$
Or simply: If it is not true that everthing satisfies the predicate, then there must be something that does not satisfy the predicate.