Predicate Logic Modifying Quantifiers Withing Conditionals

Question

I'm working on a predicate logic derivation problem, and I've ran into a couple of issues. Firstly, I am a bit new to derivations in predicate logic, and don't have a full understanding of all the rules. Anyway, the problem I'm working on is:

$\forall x(Fx \iff \forall yG(xy)) \therefore \exists x \forall y(Fy \Rightarrow G(xy))$

I can first do $UI$ on the only premise to get: $Fx \iff \forall yG(xy)$, and then go from a bi-conditional to a conditional to get: $Fx \Rightarrow \forall yG(xy)$, but I'm stuck here as I don't know how to proceed. Could there be a rule to get rid of the $\forall y$ in the consequence and keeping the general form of the conditional? If so, how would I go by deriving the conclusion from there?

Anyway, thanks.

Answer 1

to get: $Fx_*⇒∀yG(x_*y)$ , but I'm stuck here as I don't know how to proceed. Could

Because the witness $x_*$ is a constant, you basically have $A\to \forall y~P(y)$.

Assuming $A$, gives $\forall y~P(y)$ by implication elimination, then $P(y_*)$ by universal elimination, and discharging the assumption gives $A\to P(y_*)$.   Since $y_\ast$ is arbitrary, we have $\forall y~(A\to P(y))$ by universal reintroduction.

Thus $Fx_\ast \to\forall y~G(x_\ast y)$ infers $\forall y~(Fx_\ast \to G(x_\ast y))$

---

$$\begin{array}{l|l:l} X.0& Fx_\ast \to\forall y~G(x_\ast y) & \text{Given Premise}\\ \quad X.0.1 & Fx_\ast & \text{Assume} \\ \quad X.0.2 & \forall y~G(x_\ast,y) & X.0, X.0.1,\to\mathsf{E} \\ \quad X.0.3 & G(x_\ast, y_\ast) & X.0.2,\forall\mathsf E\vert^y_{y_\ast} \\ \quad X.0.4 & Fx_\ast\to G(x_\ast, y_\ast) & X.0.1,X.0.3, \to\mathsf I \\ X.1 & \forall y~\big(Fx_\ast\to G(x_\ast, y)) & X.0.4, \forall \mathsf I\vert^{y_\ast}_y \end{array}$$

Answer 2

Consider $\exists x(Fx)$. Either $\exists x(Fx)\wedge \forall x(\neg Fx)$

1.) By your given statement: $\exists x(Fx) \iff\exists x \forall y(G(xy))$

2.) And since the latter predicate ($Fy$) is never true: $\forall x(\neg Fx) \Rightarrow \forall x \forall y(Fy \Rightarrow G(xy))$

The latter statements from both 1.) and 2.) are stronger versions of $\exists x \forall y(Fy \Rightarrow G(xy))$

To gain some intuition: Let $Fx=$ "$x$ is a perfect guest", $G(xy)=$ "$x$ compliments $y$", and $x, y$ be from the space of party guests.

Then $\forall x(Fx\iff \forall yG(xy))=$ "$x$ is a perfect guest if and only if he compliments everyone at the party"

The conclusion $\exists x \forall y(Fy \Rightarrow G(xy))=$ "There exists a guest who has complimented all perfect guests". If there are no perfect guests, then every guest qualifies since there are no perfect guests to compliment. If there is at least one perfect guest, then he qualifies since he has complimented everyone and therefore, all other perfect guests (including himself!) as well.

Answer 3

$$\forall x ~ (Fx \Rightarrow \forall y~ Gxy)$$

is equivalent to

$$\forall x ~ \forall y ~ (Fx \Rightarrow Gxy)$$

which implies (standard non empty universe caveat)

$$\exists x ~ \forall y ~ (Fx \Rightarrow Gxy)$$

An outline of a proof would be like:

$$\begin{array} {l} \forall x ~ (Fx \Leftrightarrow \forall y~ Gxy) \\ \vdots \\ Fx \Rightarrow \forall y~ Gxy \\ \vdots \\ Fx \Rightarrow Gxy \\ \vdots \\ \exists x ~ \forall y ~ (Fx \Rightarrow \forall y~ Gxy) \\ \end{array}$$

In detail:

$$\begin{array} {rll} (1) & \forall x ~ (Fx \Leftrightarrow \forall y~ Gxy) & \text{Premise} \\ (2) & Fx \Leftrightarrow \forall y~ Gxy & \forall~\text{Elim of 1} \\ (3) & Fx \Rightarrow \forall y~ Gxy & \iff~\text{Elim of 2} \\ (4) & \quad\quad Fx & \text{Premise} \\ (5) & \quad\quad \forall y~ Gxy & \Rightarrow~\text{Elim of 4} \\ (6) & \quad\quad Gxy & \forall~\text{Elim of 5} \\ (7) & Fx \Rightarrow Gxy & \Rightarrow~\text{Intro of 4 through 6} \\ (8) & \forall y ~ (Fx \Rightarrow Gxy) & \forall~\text{Intro of 7} \\ (9) & \exists x ~ \forall y ~ (Fx \Rightarrow \forall y~ Gxy) & \exists~\text{Intro of 8} \\ \end{array}$$