Proving ${\sim}(p \mathbin\& q)$ implies ${\sim p}\mid{\sim q}$ using Fitch

I am struggling with proving something in Fitch. How can I prove from the premise ~(p & q), that ~p | ~q . Any ideas on how I should proceed; I have no idea...?

• Presumably you're the same user that asked this question; you can request for your accounts to be merged on this page (select the appropriate option from the dropdown menu). – Lord_Farin Oct 19 '13 at 21:28
• What's Fitch? ~~ You can use a truth table, but I don't know what Fitch is, so I don't know if that answers your question. – Stefan Smith Oct 19 '13 at 22:10
• @StefanSmith It doesn't answer it. – Git Gud Oct 19 '13 at 22:26
• @StefanSmith Fitch is one of the three little programs that accompany this popular logic textbook. It's a proof system; the other two programs are Boole (incidentally, for constructing truth tables), and Tarski's world (for evaluating first-order sentences within a block world of a certain kind). – Hunan Rostomyan Oct 20 '13 at 0:21

Here are two different Fitch-style proofs. In the one immediately below I've used the propositional tautology (P v ~P) and proved the desired conclusion by cases. In the second one, I've used the definition of '$\rightarrow$' and proved it directly (i.e., by conditional introduction).

$\fbox{Proof by Cases}$ $\fbox{Direct Proof }$ • If (as in step 2 of the first proof) you can use something just because it's a tautology, then why not collapse it all into "$\neg(P\land Q)\to(\neg P\lor \neg Q)$ is a tautology, thus done"? – Henning Makholm Oct 20 '13 at 20:34
• You're right, of course. Not knowing what exactly the allowed rules are, I figured it might still be of some small use. Unlike the formula immediately above, $(P \lor \lnot P)$ is an axiom of all classical logics I've come across; so its use might be more justified than that of its longer equivalent. Anyway, thank you very much for the comment. – Hunan Rostomyan Oct 20 '13 at 22:23
• @Human: I can think of lots of classical logics where $P\lor\neg P$ is not an axiom but merely a theorem -- such as ones that become classical by adding $((P\to Q)\to P)\to P$ or $\neg\neg P\to P$ to an intuitionistic substratum. Or classical sequent calculus which has no specific axioms responsible for classicality. – Henning Makholm Oct 20 '13 at 22:45
• @HunanRostomyan Here's an axiom set for classical logic which also works well enough for natural deduction, but ApNp is not an axiom: 1. CpCqp. 2. CCpCqrCCpqCpr. 3. CpApq. 4. CpAqp. 5. CCpqCCrqCAprq. 6. CpCqKpq. 7. CKpqp. 8. CKpqq. 9. CCpqCCqpEpq. 10. CEpqCpq. 11. CEpqCqp. 12. CCNpKqNqp. – Doug Spoonwood Oct 22 '13 at 16:06
• Thanks Doug. I have to admit that I prefer @Henning's $(\lnot\lnot P \rightarrow P)$ + $\sf IPC$ because it has only 9 axioms (plus, of course, modus ponens and closure under uniform substitution). – Hunan Rostomyan Oct 22 '13 at 21:28

I use Polish notation. Instead of writing $\land$, $\lor$, $\lnot$, and ->, I write K, A, N, and C respectively. Connectives also appear before lower case letters instead of in the middle of them. Thus, for (p->q) I write Cpq. So, we want to show that

NKpq $\vdash$ ANpNq.

The rules I use probably vary a little from Fitch, but not so much that you can't figure out how to write a proof in Fitch after reading this one. The basic plan of this proof goes to assume the negation of the desired conclusion. Then, we'll show that Kpq will hold, by showing that p and q will hold. We'll show that p and q hold respectively by showing that if we assume Np and Nq respectively, then we'll get a contradiction. Then since we have p and q, we'll infer Kpq, and since we have NKpq upfront, this gives us a contradiction. Since NANpNq was the last hypothesis in effect, this means we can eventually infer ANpNq.

The rules I'll use can get written as follows.

C-in: {$\alpha$, ..., $\beta$} $\vdash$ C$\alpha$$\beta, where \alpha and \beta have the same scope. A-in left: \alpha \vdash A\alpha$$\beta$.

A-in right: $\alpha$ $\vdash$ A$\beta$$\alpha. K-in: {\alpha, \beta} \vdash K\alpha$$\beta$.

N-out: CN$\alpha$K$\beta$N$\beta$ $\vdash$ $\alpha$.

1 assumption         NKpq
2 hypothesis      !  NANpNq
3 hypothesis      !@ Np
4 3 A-in left     !@ ANpNq
5 2, 4 K-in       !@ KANpNqNANpNq
6 2-5 C-in        !  C Np KANpNqNANpNq
7 6 N-out         !  p
8 hypothesis      !# Nq
9 8 A-in right    !# ANpNq
10 9, 2 K-in      !@ KANpNqNANpNq
11 8-10 C-in      !  C Nq KANpNqNANpNq
12 11 N-out       !  q
13 7, 12 K-in     !  Kpq
14 1, 13 K-in     !  KKpqNKpq
15 2-14 C-in         C NANpNq KKpqNKpq
16 15 N-out          ANpNq.