Conditional Proof with Negated Disjunctions (Biconditional Premise)

Question

I'm a beginner in logic, so forgive me for the inevitable incompetence!

I am trying to do a conditional proof with the sequence below, and had hoped to equivocate $\lnot(P \lor Q)$ with $\ (\lnot P \land \lnot Q)$. Do I need an additional subproof to do this?

$Q\leftrightarrow R \vdash \lnot(P \lor Q) \to \lnot (P \lor R)$

I'm also unsure whether I can apply $\land E$ to $(Q\iff\ R)$ and extract $(Q\to R)$ in a single operation, or if it requires multiple steps.

Thanks for any time taken to read my question.

Answer 1

If you want to use $\neg Q$, you can't pull it straight out of $\neg (P\vee Q)$. If you want it, you can infer $\neg P\wedge \neg Q$ by the De Morgan law (DeM).

I'm not a huge fan of pulling apart biconditionals in natural deduction. You can just use $\leftrightarrow E$ to replace one side with the other in a proof. This example is harder, because you want to replace $\neg Q$ with $\neg R$ and those sentences aren't part of the biconditional. The easiest way around it is to assume $R$, derive $\bot$ from it, then infer $\neg R$ by $\neg I$.

Here's my entire proof, when you're ready for it.

Answer 2

It depends on what rules you have available in your formal proof system. If you have DeMorgan as an inference rule, then you can obviously do this in one step.

If not, you'll need to do two subproofs: one to infer $\neg P $ and one to infer $\neg Q$

To get $\neg Q$: Assume $Q$, infer $P \lor Q$ using $\lor \ Intro$, and now you have a contradiction with $\neg (P \lor Q)$, and so by closing the subproof and applying $\neg \ Intro$ you can get $\neg Q$.

Same for $\neg P$

However ... since your goal is $\neg (P \lor r)$, I would recommend to do a proof by contradiction directly. That is: assume $P \lor R$, and then show that (using two subproofs) both $P$ and $R$ lead to a contradiction. So then yu can use proof by cases (formalized by $\lor \ Elim$) to get a contraidction, and then use $\neg \ Intro$ to get $\neg (P \lor R)$

Finally: can you infer $Q \to R$ directly from $Q \leftrightarrow R$? Again, it all dends on what formal rules the system has. Some systems allow you to do this, sure, others not.

Answer 3

You want to introduce a conditional with an assumed negation that somehow derives another negation. Clearly that derivation will be to introduce a negation with an assumed position that derives a contradiction...of the first assumption.

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{q\leftrightarrow r}{\fitch{\neg(p\vee q)}{\fitch{p\vee r}{~~\vdots\\p\vee q\\\bot}\\\neg(p\vee r)}\\\neg(p\vee q)\to\neg(p\vee r)}$

Now, you have assumed a disjunction with the aim of deriving a disjunction. So...

Answer 4

$\newcommand\tot\leftrightarrow$

Here is a proof using only introduction and elimination rules, without the derived De Morgan rules:

---

The genreal strategy of getting from $\neg (P \lor Q)$ to $\neg Q$ is as follows:
1. Assume $Q$.
2. If $Q$ holds, then so does $P \lor Q$. (This is disjunction introduction.)
3. But this is a direct contradiction to the assumption that $\neg (P \lor Q)$.
4. Conclude that the assumption $Q$ must have been wrong, i.e. derive $\neg Q$ by negation introduction on the subproof from $Q$ to $\bot$.

---

If we do the analogous for $P$, we can derive the De Morgan rule $\neg (P \lor Q) \vdash \neg P \land \neg Q$ by simply doing a conjunction introduction on the two conclusions:

---

The other direction of the De Morgan rule, $\neg P \land \neg Q \vdash \neg (P \lor Q)$, works as follows:

1. Assume that $P \lor Q$ does hold.
2. Consider the case $P$, i.e. assume $P$.
3. From $\neg P \land \neg Q$, by conjunction elimination we know $\neg P$.
4. This is a contradiction to $P$.
5. Steps 2-4 analogously for $Q$.
6. Since both cases, $P$ and $Q$, leads to a contradiction, and since we assumed that at least one out of $P$ and $Q$ holds, we can conclude $\bot$ for sure. This is disjunction elimination on $P \lor Q$ and the two subproofs $P \vdash \bot$, $Q \vdash \bot$.
7. Since we derived a contradiction from the assumption $P \lor Q$, the assumption must have been wrong, and we can conclude $\neg(P \lor Q)$ by negation introduction on the whole subproof $P \lor Q \vdash \bot$.

This is what it looks like formally:

And so we avoided the De Morgan rule, which is only a derived rule and often not assumed to be part of natural deduction, by using introduction and elimination rules only.

---

I'm also unsure whether I can apply ∧E to (Q⟺ R) and extract (Q→R) in a single operation, or if it requires multiple steps.

That depends on your rule system. If you have an introduction-elimination rule pair for $\tot$, something like

m. | P
   ----
n. | Q
i. | Q
   ----
j. | P
k.  P <-> Q   (<->I, m-n, i-j)


m. P <-> Q
n. P
   Q          (<->E, m, n)


m. P <-> Q
n. Q
   P          (<-> E, m, n)

then you can derive $Q$ from $Q \tot R$, $R$ with the dedicated $\tot E$ directly, as I did on line 8 above.

If you don't have such a rule in your system, then $Q \tot R$ will be defined as $(Q \to R) \land (R \to Q)$ -- these will simply be treated as the same formula -- and you can do the desired subderivation via $\land E$ to get $R \to Q$ and $\to E$ on the on-way implication togehther with $R$ to get $Q$: