# Language Proof & Logic 8.31 Fitch Proof

Been working on this one question for the past hours and I can't ever seem to get the last step working. Any help would be appreciated!  • What is the question ? What is the step you are concerned with ? You can use LEM : Mythical(c) or not-Mythical(c). Nov 12, 2019 at 7:49

Note that the first premise is a conjunction. So, you can just get the two conjuncts using Conjunction Elimination. You have the two conjuncts as the respective assumptions of the two subproofs you have, which would make sense if the conjunction was a disjunction ... but it is not. So again, you can get the two conjuncts at 'ground' level ... and hence you can get the Mythical(a)->Magical(a) and the ~Mythical(a)->Magical(a) sentences at ground level as well. And from there, you should be able to prove Magical(a) without too much effort.

This is as close as I got: I think I'm stuck on the last step. Please update if you end up finding out how to do it.

Cheers!

• Lines 6 and 7 should not be assumptions. They should be derived from Premise 1 by conjunction elimination; and thus do not raise contexts. Nov 28, 2019 at 23:05
• The disjunction you should be eliminating is `~Mythical(c) v Mythical(c)`, derived by LEM. Nov 28, 2019 at 23:12
• How do I derive ~Mythical(c) v Mythical(c)? I am not allowed to use tout con.
– spam
Nov 29, 2019 at 5:56
• Then nest two proofs by contradiction. Assume '~Magical(c)' then assume 'Mythical(c)', which derives 'Magical(c)' as above. Use this contradiction to discharge the second assumption with *negation introduction to deduce '~Mythical(c)', and derive 'Magical(c)' again. Discharging the first assumption will deduce '~~Magical(c)' and you are almost done. Nov 29, 2019 at 9:21

Lines 6 and 7 should not be assumptions. They should be derived from Premise 1 by conjunction elimination; and thus do not raise contexts. The disjunction you should be eliminating is `~Mythical(c) v Mythical(c)`, derived by LEM.

If you cannot use a TautCon to derive `~Mythical(c) v Mythical(c)` you can use nested proof by contradiction.

``````   |_ :
|  |_ ~Magical(c)       Assumption
|  |  |_ Mythical(c)    Assumption
|  |  |  :
|  |  |  :
|  |  |  Magical(c)
|  |  |  _|_            Negation Elimination
|  |  ~Mythical(c)      Negation Introduction
|  |  :
|  |  :
|  |  Magical(c)
|  |  _|_               Negation Elimination
|  ~~Magical(c)         Negation Introduction
|  Magical(c)           Double Negation Elimination
``````

I know it’s a formal logic question with a mechanical proof, but maybe taking a semantic approach might help you see what’s going on.

Firstly, we’re talking about a constant object C. (In practice C might be a parameter for any object, but let’s think of it in specific terms first)