Complex Natural Deduction proof

Question

How do I provide a Natural Deduction proof for (¬A ∨ ¬B) → (C → A ∧ B)→ ¬C?

I know I can work backwards and i managed to get rid of the implications:

¬C

(C → A ∧ B)→ ¬C

(¬A ∨ ¬B) → (C → A ∧ B)→ ¬C

However i'm unsure where to go from here and what Hypotheses to choose, I've recently started Natural Deduction and I'm finding it pretty tricky

It's hard to give a good answer without knowing what system of natural deduction you are using. The idea will be to assume $\lnot A\lor \lnot B$ and $C\to A\land B$ and then prove $\lnot C.$ The presence of the disjunctive assumption $\lnot A\lor \lnot B$ suggests that you will need to do a case analysis, but how this is formalized precisely will depend on the details of the system you are using. — spaceisdarkgreen, Oct 28 '21 at 03:06

cinch · Answer 1 · 2021-10-28T03:24:46.800

In most logics connectives with same precedence are associated to the right by default (see a recent post), so we need to prove $(¬A ∨ ¬B) → ((C → A ∧ B)→ ¬C)$. I'll sketch a proof below using the most common ND rules, and you should fill in your specific rules for your ND system:

Apparently we can try prove by cases:

 1 ¬A ∨ ¬B                        premise 
   2 ¬A                         
     3 C → A ∧ B                  assumption
       4 C                        assumption
       5 A ∧ B                    → E 3-4 (MP)
       6 A                        ∧ E
       7 ⊥                        ¬ E 2, 6
     8 (C → A ∧ B) → ¬C           ¬ I 4, 7
9 ¬B

     10 C → A ∧ B                  assumption
       11 C                        assumption
       12 A ∧ B                    → E 10-11 
       13 B                        ∧ E
       14 ⊥                        ¬ E 9, 12
     15 (C → A ∧ B) → ¬C           ¬ I 11, 14
16 (¬A ∨ ¬B) → ((C → A ∧ B)→ ¬C)  ∨ E

Finally please be aware that $((¬A ∨ ¬B) → (C → A ∧ B)) → ¬C$ is not valid which has an obvious counterexample when $A=B=C=True$.

score 0 · Answer 2 · answered Oct 28 '21 at 03:09

Those are indeed your targets. So you need raise appropriate assumptions in subproofs aiming for them. The skeleton should look something like this (in Fitch style), but will depend somewhat on the rules implemented in your proof system.

$$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{}{\fitch{\neg A\vee\neg B}{\fitch{C\to A\wedge B}{\fitch{C}{\vdots\\\bot}\\\neg C}\\(C\to(A\wedge B)\to\neg C}\\(\neg A\vee\neg B)\to((C\to(A\wedge B)\to\neg C)}$$

At the very least, you'll need a 'proof by cases' to eliminate that disjunction.

score 0 · Answer 3 · answered Oct 29 '21 at 17:00

Here's one way to do it, $$\begin{align} \neg A, C \to (A \wedge B), C &\vdash C &&\text{($\in$)}\\ \neg A, C \to (A \wedge B), C &\vdash C \to (A \wedge B) &&\text{($\in$)}\\ \neg A, C \to (A \wedge B), C &\vdash A \wedge B &&\text{($\to -$)}\\ \neg A, C \to (A \wedge B), C &\vdash A &&\text{($\wedge -$)}\\ \neg A, C \to (A \wedge B), C &\vdash \neg A &&\text{($\in$)}\\ \neg A, C \to (A \wedge B) &\vdash \neg C &&\text{($\neg +$), (4), (5)}\\ \neg A &\vdash (C \to (A \wedge B)) \to \neg C &&\text{($\to +$)}\\ \neg B, C \to (A \wedge B), C &\vdash C &&\text{($\in$)}\\ \neg B, C \to (A \wedge B), C &\vdash C \to (A \wedge B) &&\text{($\in$)}\\ \neg B, C \to (A \wedge B), C &\vdash A \wedge B &&\text{($\to -$)}\\ \neg B, C \to (A \wedge B), C &\vdash B &&\text{($\wedge -$)}\\ \neg B, C \to (A \wedge B), C &\vdash \neg B &&\text{($\in$)}\\ \neg B, C \to (A \wedge B) &\vdash \neg C &&\text{($\neg +$), (11), (12)}\\ \neg B &\vdash (C \to (A \wedge B)) \to \neg C &&\text{($\to +$)}\\ \neg A \vee \neg B &\vdash (C \to (A \wedge B)) \to \neg C &&\text{($\vee -$), (7), (14)}\\ \emptyset &\vdash (\neg A \vee \neg B) \to ((C \to (A \wedge B)) \to \neg C) &&\text{($\to +$)} \end{align}$$

Complex Natural Deduction proof

3 Answers3