Provide a proof for the following using FOL in forallx
Use the natural deduction system and proof strategies in forallx to provide a formal proof for the following . Please provide a picture of your proof.
∃xFx ∧ ∀yGy ∴ ∃x(Fx ∧ Gx)
-
3What have you tried? What rules you think to be used?– Mauro ALLEGRANZANov 11, 2021 at 11:22
-
I'm not an expert of forallx proof system, but within "standard" Natural Deduction, the proof is a very straightforward" exercise in application of quantifiers rules.– Mauro ALLEGRANZANov 11, 2021 at 11:24
-
I’m not sure whether to work forwards or backwards to derive the conclusion.– AlexisNov 11, 2021 at 12:36
-
You can start with simplification of the Premise.– DasemNov 11, 2021 at 20:16
-
Welcome to SE Philosophy! Thanks for your contribution. Please take a quick moment to take the tour or find help. You can perform searches here or seek additional clarification at the meta site. Don't forget, when someone has answered your question, you can click on the arrow to reward the contributor and the checkmark to select what you feel is the best answer.– J DNov 13, 2021 at 15:41
|
Show 1 more comment
2 Answers
I’m not sure whether to work forwards or backwards to derive the conclusion.
Why not both? You know what you have to start with, and where you wish to go.
Your premise is a conjunction of an existential and an universal. Look to the rules of Conjunction Elimination, Universal Elimination, and Existential Elimination. See what that start gives you to work with.
Your conclusion is an existential of a conjunction. Look to the Rules of Conjunction Introduction and Existential Introduction. Find what you need to reach the final target.
Bridge them together.
Assume ∃xFx ∧ ∀yGy then prove ∃x(Fx ∧ Gx) based on this assumption.
Use conjunction elimination to derive ∃xFx from your assumption. Then instantiate the variable x to a constant, say, a.* The result is Fa.
Use conjunction elimination to derive ∀yGy from your initial assumption. From this, you can instantiate the variable y to any constant, say a.** The result is Ga.
Use conjunction introduction to combine Fa and Ga, the result being Fa ∧ Ga.
Use existential generalization, with the variable x replacing every occurrence of a. The result is ∃x(Fx ∧ Gx).
*The constant cannot already be used in the proof. This is because ∃ applies to something in the domain, but we don't know exactly what. **Universals apply to everything in the domain, not just something. That means we can choose to instantiate y to the constant a.
