Predicate logic and material equivalence.

Question

Predicate logic and material equivalence.

- --- Hey all,

I have a question about predicate logic and material equivalences. When using the rule of material equivalence on a biconditional - 'if and only if' statement - do the quantifiers apply to the whole statement or to a part? I don't know if I'm writing this super clearly so I'll give an example.

Statement and Attempts

Statement: ∃xFx ↔ ∀y(Fy ∨ Gy → Hy)
Material equivalence attempts:

(1) (∃xFx → ∀y(Fy ∨ Gy → Hy)) & (∀y(Fy ∨ Gy → Hy) → ∃xFx)
(2) ∃x∀y{[Fx → (Fy ∨ Gy → Hy)] & [(Fy ∨ Gy → Hy) → Fx]}

My Thoughts

Intuitively, it looks like the second option is correct because, in the 'if and only if statement' of (1), we wouldn't be allowed to perform an existential proof such that the same constant, by rules of existential proof, would be allowed to satisfy the same predicate - although, now that I'm thinking about this, I can probably just instantiate both variables within the 'if and only if' statement to check which way is correct, oops what a digression - option (1) looks like it doesn't make sense to me, especially given the fact that

∃xFx ↔ ∀y(Fy ∨ Gy → Hy)

is a biconditional that says "There may exist x - such that Fx - only if for all y - such that if Fy or Gy then Hy." In the case of this statement, it looks like ∃xFx implies ∀y(Fy ∨ Gy → Hy) and vice versa - I feel like the same variables need to be used to translate this to the conjunction of two conditionals. However, I also know that quantifier order matters; is (2) the right way of doing things?

I might have solved my own problem by thinking about this. So, if we instantiate the variables I think we could end up with something like this:

1 (1) ∃xFx ↔ ∀y(Fy ∨ Gy → Hy)                                        A
2 (2) Fa ↔ ∀y(Fy ∨ Gy → Hy)                                          A for existential proof (1)
2 (3) Fa ↔ (Fb ∨ Gb → Hb)                                            2 ∀ instantiation
2 (4) (Fa → (Fb ∨ Gb → Hb)) & ((Fb ∨ Gb → Hb) →  Fa)                 3 material equivalence
2 (5) ∀y{[Fa → (Fy ∨ Gy → Hy)] & [(Fy ∨ Gy → Hy) →  Fa]}             4 ∀ generalization
2 (6) ∃x∀y{[Fx → (Fy ∨ Gy → Hy)] & [(Fy ∨ Gy → Hy) →  Fx]}           5 exists
1 (7) ∃x∀y{[Fx → (Fy ∨ Gy → Hy)] & [(Fy ∨ Gy → Hy) →  Fx]}           1,6 exists proof discharge 2

Would this be the right quantifier order?

Thanks,

Kyle (Heifenhoomer)