Use natural deduction to prove ((¬P ∧ ¬Q) → ¬(P ∨ Q)) using primitive rules only

Question

Here is my attempt which is obviously full of errors. I saw another post that has quite a similar question but I could not understand it still..

Answer 1

Line 9 $\neg (P \lor Q)$ should be the last line of the subproof, i.e. that line should occur inside the subproof. So with that subproof, you show that if you assume $\neg P \land \neg Q$, then you can eventually get to $\neg (P \lor Q)$. And so then you can use $\to$ Intro to conclude the whole statement at the end after/outside the subproof.

Also, given that the goal of the subproof is $\neg (P \lor Q)$, which is a negation, you should set this up as a proof by Contradiction, i.e. start a second subproof inside the first one, assume $P \lor Q$, show how that leads to a contradiction, and conclude $\neg (P \lor Q)$ using $\neg$ Intro. That's the basic set-up/proof plan/strategy/skeleton. I'll leave it to you to fill in the rest.

Answer 2

I think it's easier than what it seems. Take a look at that:

$(\lnot P \wedge \lnot Q) \to \lnot(P \lor Q) \equiv \lnot(P \lor Q) \to \lnot(P \lor Q) \equiv \lnot(P \lor Q) \lor \lnot\lnot(P \lor Q) \equiv \lnot(P \lor Q) \lor (P \lor Q) \equiv 1$

All the equivalences are elementary, if you need help, tell me. Just take a look at the last step, maybe is the least automatical. Just remember that:

$P \lor \lnot P \equiv 1$

because either $P=0,1$, the equivalence equals $1$.

Answer 3

Line 8 cites an unavailable line (4)

Line 4 is the assumption of a closed subproof. You cannot access this assumption for the $\vee\sf I$ rule outside of its scope.

Line 9 cites too few ranges for the $\vee\sf E$ rule.

The rule requires you to cite a disjunction and two subproofs which begin assuming the disjuncts and reach the same conclusion. This is the "proof by cases" format.

Line 9 cites an unavailable line (8)

Line 10 cites a range of lines which do not make up a subproof $(1{-}9)$

The $\vee\sf E$ rule is to deduce that the conclusion holds in the same scope as the disjunction and two subproofs. It will thus not produce $\lnot(P\vee Q)$, but rather $\bot$.

The ${\to}\sf I$ rule requires a subproof which assumes the antecedant and concludes with the consequent. In short, you want $\lnot(P\vee Q)$ to be inside the subproof.

You need a $\lnot\sf I$ rule to introduce a negation; which requires deriving a contradiction from the assumption you wish to negate.

---

Thus you just need to rearrange you proof slightly. Raise an assumption of $P\vee Q$ before the two subproofs, so you can conclude the contradiction with $\vee\sf E$, and therefore discharge the second assumption to deduce its negation with $\lnot\sf I$. Finally discharge the first assumption to deduce the conditional with ${\to}\sf I$.

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{}{\fitch{~~1.~~\lnot P\land\lnot Q}{~~2.~~\lnot P\\~~3.~~\lnot Q\\\fitch{~~4.~~(P\vee Q)}{\fitch{~~5.~~P}{~~6.~~\bot}\\\fitch{~~7.~~Q}{~~8.~~\bot}\\~~9.~~\bot\hspace{20ex}{\lor}\mathsf E~4,5{-}6,7{-}8}\\10.~~\lnot(P\vee Q)\hspace{15ex}\lnot\mathsf I~4{-}9}\\11.~~(\lnot P\land\lnot Q)\to\lnot(P\vee Q)\hspace{4ex}{\to}\mathsf I~1{-}10}$

Answer 4

$\def\fitch#1#2{\begin{array}{|l}\>#1\\\hline\>#2\end{array}}$ I'll try to explain why the checker says the lines were invalid. Just comment if I got something wrong.

---

• For line 8, you said that it uses disjunction introduction. Recall that the inference rule is
  
  $\fitch{A.}{A \lor B.}\qquad\fitch{A.}{B \lor A.}$
  
  The problem, is that you cited an assumption that is not yet justified in the current context. Note that disjunction introduction is neither
  
  $\fitch{\fitch{P}{\vdots}}{P \lor Q.}$ nor $\quad\fitch{\fitch{P}{\vdots}}{Q \lor P.}$
  
  but the ones shown before.

• For line 9, you said that it uses disjunction elimination. Recall that it is
  
  $\fitch{A \lor B. \\ \fitch{A}{\,\vdots\\C.} \\ \fitch{B}{\,\vdots\\C.}}{C.}$
  
  However, you didn't have a disjunction nor the subproofs for each disjunct. You can't eliminate a disjunction symbol if you didn't have one. As you can see, at least three statements are needed to apply disjunction elimination. You only cited one, and so the checker says that you didn't provide enough ranges of lines. Also, you cited a statement that's inside a subproof, which is not in the same level as line 9.

• For line 10, you said that it uses implication introduction, which is
  
  $\fitch{\fitch{A}{\,\vdots \\ B.}}{A \Rightarrow B.}$
  
  However, the lines you cited doesn't match the implication introduction rule. Line 9 is not inside the subproof assuming $A$, so it is invalid.

This is the explanation for the errors, and you can check Bram28's answer for the outline of the proof.