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)
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
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.