Beginner natural deduction, proof verification

Question

I would like to prove the following proofs using the system of natural deduction and I am having a little difficulty:

1) $\exists x \space \text{slimy}(x)$, $\forall x \space (\text{slimy}(x) \rightarrow (\text{big}(x) \vee \text{toad}(x)))$, $\forall x \space (\text{big}(x) \rightarrow \text{mighty}(x)) \space \vdash \exists x \space \text{mighty}(x)$

My attempt:

 1: ∃x slimy(x)                                               premise
 2: ∀x (slimy(x) → (big(x) ∨ toad(x)))                        premise
 3: ∀x (big(x) → mighty(x))                                   premise
   ----------------------------------------------------------
 4: slimy(c)                                                  assumption
 5: slimy(c) → (big(c) ∨ toad(c))                             ∀-elim 2
 6: big(c) ∨ toad(c)                                          →-elim 5,4
 7: big(c)                                                    ∨-elim 6
 8: big(c) → mighty(c)                                        ∀-elim 3
 9: mighty(c)                                                 →-elim 8,7
10: ∃x mighty(x)                                              ∃-intro 9
   ----------------------------------------------------------
11: ∃x mighty(x)                                              ∃-elim 1,4–10

2) $\exists x \space \text{slimy}(x) \wedge \exists x \space \text{toad}(x)$, $\forall x \space(\text{slimy}(x) \wedge \text{toad}(x) \rightarrow \text{mighty}(x))$, $\forall x \space (\text{mighty}(x) \rightarrow \text{big}(x)) \space \vdash \space \exists x \space \text{big}(x)$

My attempt:

 1: ∃x slimy(x) ∧ ∃x toad(x)                                  premise
 2: ∀x (slimy(x) ∧ toad(x) → mighty(x))                       premise
 3: ∀x (mighty(x) → big(x))                                   premise
 4: slimy(c) ∧ toad(c)                                        assumption
   ----------------------------------------------------------
 5: slimy(c) ∧ toad(c) → mighty(c)                            ∀-elim 2
 6: mighty(c)                                                 →-elim 5,4
 7: mighty(c) → big(c)                                        ∀-elim 3
 8: big(c)                                                    →-elim 7,6
 9: ∃x big(x)                                                 ∃-intro 8
   ----------------------------------------------------------
10: ∃x big(x)                                                 ∃-elim 1,4-9

Could someone please explain which lines are incorrect, and why they are incorrect?

Answer 1

1)

 1: ∃x slimy(x)                                               premise
 2: ∀x (slimy(x) → (big(x) ∨ toad(x)))                        premise
 3: ∀x (big(x) → mighty(x))                                   premise
 ----------------------------------------------------------
 4: slimy(c)                                                  assumption

This is not an assumption. This is existential elimination from Premise 1.

4': slimy(c)                                                  ∃-elim 1
 5: slimy(c) → (big(c) ∨ toad(c))                             ∀-elim 2
 6: big(c) ∨ toad(c)                                          →-elim 5,4
 7: big(c)                                                    ∨-elim 6

That is not how disjunction elimination works.   If you know $\sf P\vee R$, you are assured that at least one of $\sf P$ or $\sf R$ is true, but you cannot be certain that either in particular will be true.

Only if the conclusion $\sf Q$ is an consequence of $\sf P$ and also a consequence of $\sf R$ can the disjunction be eliminated to imply the conclusion.

The rule of disjunction elimination is: $\sf P\vee R, P\to Q, R\to Q\vdash Q$

You won't be able to use this rule. Rather you have to prepare for a constructive dilemma.

7': toad(c) → toad(x)                                         tautology 
 8: big(c) → mighty(c)                                        ∀-elim 3
 9: mighty(c)                                                 →-elim 8,7

As stated we can't use the old statement 7, rather we use the rule of constructive dilemma $\sf P\vee R, P\to Q, R\to S\vdash Q\vee S$

9': mighty(c) ∨ toad(c)                                       ∨-dilemma 6,7',8
10: ∃x mighty(x)                                              ∃-intro 9

Using the new 9 you can only conclude

10: ∃x (mighty(x) ∨ toad(x))                                  ∃-intro 9', 4

That is as strong as the three premises infer.

---

2)

1: ∃x slimy(x) ∧ ∃x toad(x)                                  premise
2: ∀x ((slimy(x) ∧ toad(x)) → mighty(x))                     premise
3: ∀x (mighty(x) → big(x))                                   premise
4: slimy(c) ∧ toad(c)                                        assumption

You can't make an assumption unless you intend to discharge it; all assumptions must be discharged.   Further, you cannot reach this line from existential elimination either, because premise 1 asserts that there are things which are slimy and things which are toads, but does not guarantee the existence of any thing that is both slimy and toad.

You can't go any further. All this line of reasoning will conclude is that :

∀x ((slimy(x) ∧ toad(x)) → big(x))

Answer 2

I can see why you would be 'having a little difficulty' since both arguments are invalid, so can not be proven!

For 1, a counterexample is: You have a small, slimy, and un-mighty toad, and nothing else. That would make all premises true, but the conclusion false.

For 2, a counterexample is: You have a small, slimy, un-mighty snail, as well as a small, un-slimy, un-mighty, toad.

As far as your attempts of the proofs go ...

'Proof' 1

As GrahamKemp already pointed out, you make a big mistake when doing the v Elim in line 7 of the proof attempt for 1: you can not infer:

 6: big(c) ∨ toad(c)                                         
 7: big(c)                 ∨-elim 6

If you go back to the counterexample I provided: if all you have is a small, slimy, and un-mighty toad, then 6 is true (since the only thing that exists, c, is a toad), but 7 is false (since this thing c is not big). As another example: it is true that every natural number is either even or odd (so we have (Odd(n) v Even(n)), but obviously we can't conclude Odd(n) by itself from that!

GrahamKemp also said that your line 4 is incorrect, but actually that was just fine. You use the same proof system that I am used to, in which you perform an $\exists$ Elim through the use of a subproof, exactly as you did: so actually you did a good job on the set-up (or 'proof plan' or 'proof skeleton') which is often the most important part of getting these formal proofs done!

'Proof' 2

In proof 2, though, you make a mistake in the set-up. Given the premise:

 1: ∃x slimy(x) ∧ ∃x toad(x)                   premise

you can not set up an existential elimination on both existentials at once. In fact, since this statement is a conjunction, you can't start the process of $\exists$ Elim at all. What you can do is the perform $\land$ Elim to get

n: ∃x slimy(x)           ∧ Elim 1

n+1: ∃x toad(x)            ∧ Elim 1

And now you can a subproof to eliminate either one, but that will take a subproof for each, rather than one subproof for both at once.