I'm having trouble understanding writing out a proof. The proof I'm trying to work with is :
How do I reach this goal? Which rules do I use and with which support steps to each rule (proofs to prove each step?) Using only inference rules, reit, quantifier rules. What have I missed writing out?
-
My calculation was completely wrong so look directly at grahams comment and what he has put up for correct explanations!– user39869Jun 6, 2019 at 3:26
-
This is the third context-less question you've asked about Fitch-style proofs.– Noah SchweberJun 6, 2019 at 3:52
2 Answers
On line 9 referencing conjunction elimination from line 8 should derive either B(a) or K(a), but not R(a).
You might start this with the assumption on line 8 which is made to hopefully eliminate the existential in line 2.
Then use conjunction elimination to derive B(a) from that assumption. Use universal elimination from line 1 to derive B(a) → R(a). Those two lines allow one to derive R(a). Use conjunction elimination to get K(a) and then conjunction introduction to combine R(a) ∧ K(a). Use existential introduction to turn that into ∃x(R(x) ∧ K(x)).
That will allow you to discharge the assumption using existential elimination to complete the proof.
Here's the skeleton for the proof. You begin by assuming a witness to the existential in the premises, aiming to derive a witness for the existential in the conclusion.
| Ɐx (Bx → Rx) Premise
|_ Ǝx (Bx ˄ Kx) Premise
| |_ [c] Bc ˄ Kc Assumption
| | : ˄E
| | : ˄E
| | : ⱯE
| | : →E
| | Kc ˄ Rc ˄I
| | Ǝx (Kx ˄ Rx) ƎI
| Ǝx (Kx ˄ Rx) ƎE
-
thank you so much graham! Could you please tell me the : steps as well and which steps I should higlight to each step?– user39869Jun 6, 2019 at 0:20
-
-
I did, and the way I tried it turned out like the one above, so I'm completely lost and not sure what to do? Unfortunately, I'm not gifted in this at all.– user39869Jun 6, 2019 at 0:51
-
@maxpax The first two suggestions are ˄E, conjunction elimination. So what conditional(s) are there to be eliminated? What two derivations could result? Jun 6, 2019 at 1:32
-
Thank you graham! It's all figured out!– user39869Jun 6, 2019 at 2:06