Symbolic Logic Proof: Removing Quantifiers

533 Views Asked by At

I'm going through an intro symbolic logic class (basic stuff predicate, syllogicistic) and and having trouble doing this proof I'm working on from a study sheet. And help would be appreciated

In this context, all lowercase letters less or equal to "t" are consider individal constants and all letters greater than "t" individual variables. Capital letters are properly constants.

My premises are:

$(\exists x)Fx \rightarrow (\forall x)[Px \rightarrow (\exists y)Qxy]$ (premise 1)

$(\forall x)(\forall y)(Qxy \rightarrow Gx)$ (premise 2)

And I seek to conclude:

$(\forall x) [(Fx\land Px)\rightarrow (\exists y)Gy]$.

I haven't got far.

1 - $Qxb\rightarrow Gx$ - from 2, Universal Instantian

2 - $Fx \rightarrow (\forall x)[Px\rightarrow (\exists y)Qxy]$ - 1, Existential instantiation

3 - $Fx \rightarrow (Px \rightarrow (\exists y)Qxy)$ - 2, Universal instantiton

4 - $Fx\rightarrow (Px \rightarrow Qxy)$ - 3, existential istantiona

5 - $(Fx \land Px)\rightarrow Qxy $ - 4, exportation

I'm almost there (seemingly just a modus ponens away), but can't figure out how to get the quantifiers right? I can't just put a "for all" in front of 5 because the x attached to Fx is special right?

Any help is appreciated.

1

There are 1 best solutions below

0
On BEST ANSWER

I'll prove it with Natural Deduction :

1) $Fz ∧ Pz$ --- assumed [a]

2) $Fz$ --- from 1) by $\land$-elim

3) $Pz$ --- from 1) by $\land$-elim

4) $(∃x)Fx$ --- from 2) by $∃$-intro

5) $(∀x)[Px→(∃y)Qxy]$ --- from premise 1 and 4) by $\to$-elim

6) $Pz → (∃y)Qzy$ --- from 5) by $∀$-elim

7) $(∃y)Qzy$ --- from 3) and 6) by $\to$-elim

8) $Qzy→Gz$ --- from premise 2 by $∀$-elim twice

9) $Qzy$ --- assumed [b] from 7) for $∃$-elim

10) $Gz$ --- from 8) and 9) by $\to$-elim

11) $(∃y)Gy$ --- from 10) by $∃$-intro

12) $(∃y)Gy$ --- from 7), 9) and 11) by $∃$-elim, discharging [b] : $y$ in not free in 11)

13) $(Fz ∧ Pz) \to (∃y)Gy$ --- from 1) and 12) by $\to$-intro. discharging [a]

14) $(∀x)[(Fx ∧ Px) \to (∃y)Gy]$ --- from 13) by $∀$-intro : $x$ is not free in any open assumptions (there are none).