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))).