3

If asked “Prove in Fitch: From no premises, derive $A \lor (A \to B)$. Without using Taut Con?"

These are the are the Fitch rules, and this is what I have so far.

Should I aim to use V Elim to isolate both sides and then derive with the method I'm currently trying? I'm unsure how to piece that part together.

Martin Sleziak
  • 53,687
Xavier Alexander
  • 63
  • Look at your rules and see which allow you to make some assumptions and then eliminate them. – Hungry May 23 '16 at 18:14
  • I've tried to do so but I don't know where to go from what is listed above, original version I forgot to post progress – Xavier Alexander May 23 '16 at 20:27
  • @Lord_Farin The Fitch proof system is commonly called $F$. OP it would help if you specified this. – Hungry May 23 '16 at 22:50
  • @XavierAlexander Why do you start by assuming $A \rightarrow B$? You need to eliminate all of your assumptions by the end—what rule would allow you to eliminate that? – Hungry May 23 '16 at 22:58
  • @Hungry Should I aim to use V Elim to isolate both sides and then derive with the method I'm currently trying. I'm unsure how to piece that part together. – Xavier Alexander May 23 '16 at 23:24
  • @XavierAlexander I tried to add the standard Fitch rules to your post in hopes of getting it taken off hold so I can give you a full answer... Do you have any additional rules? – Hungry May 23 '16 at 23:58
  • 1
    No additional rules – Xavier Alexander May 24 '16 at 01:41
  • 1
    Sorry I'm trying to improve this but I'm a new user and I'm trying to get the hang of this – Xavier Alexander May 24 '16 at 01:42
  • Assume $\neg A$. Then, disyunction introduction, $\neg A \vee B$. By definition of the material implication, $A\Rightarrow B$. Conclude from hypothesis by contidional proof: $\neg A\Rightarrow(A\Rightarrow B)$. Finally, by definition of the disyunction, $A\vee(A\Rightarrow B)$. – Fernando Cano May 24 '16 at 02:32
  • 1
    OP, I would start by assuming $\neg(A \vee (A \rightarrow B))$. Do you see what to do next? @FernandoCano you can't normally use the definition of the material implication or disjunction in a Fitch system. – Hungry May 24 '16 at 04:34
  • I don’t really see what to do next if I’m honest, just shots in the dark right now – Xavier Alexander May 24 '16 at 07:44
  • @Hungry of course you can use it. You first have to prove it. The proof goes by contradiction. You can always use proved theorems in your new proofs. Besides, material implication is standard in most natural deduction rule systems. – Fernando Cano May 24 '16 at 11:13
  • @FernandoCano Proving it is no easier than proving this directly, and since OP doesn't see how to do this, he won't see how to do that either. OP has already said that he cannot use any rules other than the ones in the post, which do not include material implication. – Hungry May 24 '16 at 17:16

3 Answers3

1

In order to:

prove something without premises

we have to take care to discharge all the "temporary" assumptions we made in the derivation.

We can prove your formula using LEM, that in turn is derivable from Double Negation.

1) $A$ --- assumed [a]

2) $A \lor \lnot A$ --- from 1) by $\lor$-intro

3) $\lnot (A \lor \lnot A)$ --- assumed [b]

4) $\bot$ --- $\bot$-intro: from 2) and 3)

5) $\lnot A$ --- by $\lnot$-intro from 1) and 5), discharging [a]

6) $A \lor \lnot A$ --- from 5) by $\lor$-intro

7) $\bot$ --- $\bot$-intro: from 3) and 6)

8) $A \lor \lnot A$ --- from 3) and 7) by DN, discharging [b]

Note: up to now we have proved $\vdash A \lor \lnot A$; this is an example of how to derive a valid formula, i.e. how to prove something without assumptions.

9) $A$ --- assumed [c] from 8) by $\lor$-elim

10) $A \lor (A \to B)$ --- from 9) by $\lor$-intro

11) $\lnot A$ --- assumed [d] from 8) by $\lor$-elim

12) $A$ --- assumed [e]

13) $\bot$ --- $\bot$-intro: from 11) and 12)

14) $B$ --- $\bot$-elim: from 13)

15) $A \to B$ --- from 12) and 14), discharging [e]

16) $A \lor (A \to B)$ --- from 15) by $\lor$-intro

17) $A \lor (A \to B)$ --- from 9)-10) and 11)-16) and 8) by $\lor$-elim, discharging [c] and [d].

Mauro ALLEGRANZA
  • 94,169
  • Okay, this is an old post, but, anyway. Your "proof" of LEM is this?$$\dfrac{\dfrac{~~~A\to(\neg(A\vee\neg A)\to\bot)\\neg A\to(\neg(A\vee\neg A)\to\bot)}{\neg\neg(A\vee\neg A)}{\small(\vee\mathsf E)^\star}}{A\vee\neg A}{\small(\neg\neg\mathsf E)}$$Uh,... that disjunctive elimination uses the LEM (since it is implicitly the disjunction being eliminated). – Graham Kemp Mar 15 '18 at 02:08
  • Oh, nevermind, it's $$\def\fitch#1#2{~\begin{array}{|l}#1\\hline#2\end{array}}\fitch{(\neg\neg\mathsf{E}\text{ is an accepted rule})}{\fitch{\neg(A\vee\neg A)}{\fitch{A}{A\vee\neg A\\bot}\\neg A\ A\vee\neg A\\bot}\\neg\neg(A\vee\neg A)\A\vee\neg A}$$Indenting will help readability and stuff. – Graham Kemp Mar 15 '18 at 02:33
1

The most direct way to do this is to start by assuming $\neg (A\: \vee \: (A\: \rightarrow \: B))$, eventually discharging it via negation introduction. The only other rules we have that allow us to discharge premises are conditional rules, but we want to end up with a disjunction, and the system itself doesn't give us a way of translating between them.

$ \begin{array} \\1. & \mid \: \neg (A\: \vee \: (A\: \to \: B) & \text{ass} \\2. & \mid \: \mid \: \neg A & \text{ass} \\3. & \mid \: \mid \: \mid \: A & \text{ass} \\4. & \mid \: \mid \: \mid \: \mid \: \neg B & \text{ass} \\5. & \mid \: \mid \: \mid \: \mid \: A\: \wedge \: \neg A & \text{2, 3 $\wedge$intro} \\6. & \mid \: \mid \: \mid \: \neg \neg B & \text{4-5 $\neg$intro} \\7. & \mid \: \mid \: \mid \: B & \text{6, $\neg$elim} \\8. & \mid \: \mid \: A\: \to \: B & \text{3-7 $\to$intro} \\9. & \mid \: \mid \: A\: \vee \: (A\: \to \: B) & \text{8, $\vee$intro} \\10. & \mid \: \mid \: \neg (A\: \vee \: (A\: \rightarrow \: B)\: \wedge \: (A\: \vee \: (A\: \rightarrow \: B))\quad & \text{1, 9 $\wedge$intro} \\11. & \mid \: \neg \neg A & \text{2-10 $\neg$intro} \\12. & \mid \: A & \text{11, $\neg$elim} \\13. & \mid \: A\: \vee \: (A\: \rightarrow \: B) & \text{12, $\vee$intro} \\14. & \mid \: \neg (A\: \vee \: (A\: \rightarrow \: B)\: \wedge \: (A\: \vee \: (A\: \rightarrow \: B)) & \text{1, 13 $\vee$intro} \\15. & \neg \neg (A\: \vee \: (A\: \rightarrow \: B)) & \text{1-14 $\neg$intro} \\16. & A\: \vee \: (A \ \rightarrow \ B) & \text{15, $\neg$elim} \end{array} $

In 2-9, I show $\neg A\:\vdash \: A \vee(A\rightarrow B)$, and 12-13 show $A\:\vdash \: A \vee(A\rightarrow B)$. If you already had $A \vee \neg A$, you could use these pieces with disjunction elimination, as you suggested.

Make sure to note the derivation of $\neg A\:\vdash \: A\rightarrow B$ in 2-8.

Hungry
  • 421
0

Yuck! It looks like somebody is trying to give you a headache.

To solve this there are a couple of general tricks you'll need to implement.

  1. derive $\neg (C\lor D)\vdash \neg C$.
  2. derive $\neg(C\to D)\vdash C$.

Combining yields a derivation of $\neg(A\lor (A\to B))\vdash A\land\neg A$.

Toward 1, after assuming $\neg (C\lor D)$ you'll want temporarily to assume $C$. An application of $\lor$-intro gives you a contradiction.

Toward 2, you'll first want to have achieved

  1. derive $C,\neg C\vdash D$.

With 3 in hand, let's return to 2. Assume $\neg (C\to D)$. Temporarily assume $\neg C$. Further temporarily assume $C$. After reaching $D$ by trick 3, conditional proof gives $C\to D$. You now have a contradiction, returning $\neg\neg C$.

Finally toward 3, the strategy is to 'convict the innocent': after assuming $C$ and $\neg C$, further temporarily assume $D$. Here you can can assert $C\land \neg C$. Using this proof of a contradiction which begins from an assumption of $D$ you can infer $\neg D$.

mmw
  • 953
  • 4
  • 11