Need Help Proving First Order Logic Equivalence

Hello,

I have the following First order Logic statement:

*If F(x) is not true then no H(y,x) satisfies **G(x)*

(∀x ¬F(x)) ⇒¬∃y G(y) ˄ H(y,x)

I have to change this to get:

(∃y G(y) ˄ H(y,x))) ⇒ ((∀x F(x))

Is this possible? I can possibly modify the first statement so as to prove the latter. What would be a way to do this while staying within the domain of the Logic Statement given above.

Re: Need Help Proving First Order Logic Equivalence

Quote:

Originally Posted by

**granprofaci** I have the following First order Logic statement:

If F(x) is not true then no H(y,x) satisfies G(x)

(∀x ¬F(x)) ⇒¬∃y G(y) ˄ H(y,x)

The English statement does not make sense. In first-order logic, there are two syntactic categories: terms and formulas. Semantically, terms range over objects and formulas range over properties of those objects. One can say that an object satisfies some property but not that a property satisfies another property (for this you need second-order logic). Therefore, H(y,x) cannot satisfy G(x). I think you mean that y such that H(y,x) satisfies G (and not G(x)). Also, the universal quantifier over x has to extend over the whole formula because otherwise x in H(y,x) is unbound. So, I think the English sentence should say,

If F(x) is not true then no y such that H(y,x) satisfies G

and its translation is

∀x (¬F(x) ⇒ ¬∃y (H(y,x) ˄ G(y))) (*)

Then

∀x (∃y (H(y,x) ˄ G(y)) ⇒ F(x))

is indeed equivalent to (*) because it is the contraposition of (*).

Re: Need Help Proving First Order Logic Equivalence

I see... just to make a clarification... The sentence essentially is obtained from:

If a square is not hot then no adjacent square contains a fire.

From a sentence for this, the latter has to be proven..

Re: Need Help Proving First Order Logic Equivalence

Quote:

Originally Posted by

**granprofaci** If a square is not hot then no adjacent square contains a fire.

If F(x) means "x is hot," H(y,x) means "y is adjacent to x" and G(y) means "y contains a fire," then the translation is indeed ∀x (¬F(x) ⇒ ¬∃y (H(y,x) ˄ G(y))) or ∀x (¬F(x) ⇒ ∀y (H(y,x) ⇒ ¬G(y))).