- Clever(a) ∧ ¬Happy(a)
- ∀x (Clever(x) → Happy(x))
So far I have something like this
Thanks to Bram28 I got the correct proof.
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.Sign up to join this community
Don't use subproofs!
Just eliminate the universal and after a few more lines you are done.
Here's a tip: Do not start any subproofs unless you know exactly what you are going to use those subproofs for. In Fitch, there are only 6 reasons for starting a subproof:
You are setting up a Proof by Contradiction (i.e $\neg$ Intro)
You are setting up a Proof by Cases (i.e $\lor$ Elim)
You are setting up a Conditional Proof (i.e $\rightarrow$ Intro)
You are setting up a BiConditional Proof (i.e $\leftrightarrow$ Intro)
You are setting up a Universal Proof (i.e $\forall$ Intro)
You are eliminating an existential (i.e $\exists$ Elim)
Note that in your case none of these rules make sense: you are not trying to prove a negation, conditional, biconditional, or universal, and you are not eliminating a disjunction or an existential.
Also, to force you to think about what you are using any subproof for, make it a habit to follow the following steps if you ever do start a subproof:
Start a (the) subproof(s) and write down the assumption(s)
Write down what you what at the end of (each of) the subproof(s)
Close the subproof(s) and apply the rule for which the subproof(s) was meant
Finally, go back inside the subproof and think: how can I get to the last line of my subproof given what I have?
So note that step 4 is the last thing you do, but note that in your partial proof you have been opening up a whole bunch of subproofs without indicating how you intend to use them. That's a really bad habit, and it's exactly what gets you stuck! Here's a post where I describe the 'correct' thought process for doing a specific Fitch proof.