Translate the following statements into FOL sentances
1) Alex likes John
Likes(alex, john) - I know this is correct
2) Each person is either a man or woman
AxAy( man(x) v woman(y) )
EDIT: Is this better??: Az(Person(z) -> man(x) v woman(y)) OR EDIT: Is this better??: Ax(Person(x) -> man(x) v woman(x))
3) No one is both man and woman
Ex( (man(x) ^ ¬woman(x)) v (¬man(x) ^ woman(x)) )
4) Alex likes a man who likes a woman
AxEy(Likes( man(x), woman(y) ) -> Likes(alex, man(x) ))
Thanks
Here is a screenshot of the background info
EDIT: For number 3, I have found this online "The exclusive disjunction of p and q asserts that either p is true or q is true but not both. The natural, but long-winded, way to express exclusive disjunction, then, is (p | q) & ~(p & q)."
If this can apply, then I assume the correct answer is Ax( (man(x) v woman(x)) ^ ¬(man(x) & woman(x)) )
But now I am getting confused as to how 2 and 3 are different...
Hey I just wanted to know if these were correct
One of the ways to test if a first order sentence agrees with an informal specification is to use a model.
To perform a test you need:
To determine how many relations are there in your first order sentence and list them. This list would play the role of the logical signature of your model.
Now take a set of individuals large enough to have all interesting combinations of properties assigned to at least one individual.
Assign the properties to individuals according to your understanding of the meaning of relations in your first order sentence.
Finally for each universally quantified variable try different assignments of individuals to variables and check if the property holds.
Consider one of the examples from the post.
Informal specification: Alex likes a man who likes a woman
We have
Now consider a structure where we have an individual for Alex, an individual for a man who is not Alex, and an individual for a woman who is not Alex.
Let's start with three: p1, p2, p3.
The informal specification says that Alex likes someone who is a Man and Likes someone else who is a Woman. Our model satisfies this specification.
Now consider the following statement taken from the OP:
AxEy(Likes( man(x), woman(y) ) -> Likes(alex, man(x) ))
This statement is from a different language. Here man(x) and woman(y) are unary functions instead of unary relations, so we cannot check this sentence.
I would not speculate any further on the subject of woman(y) or man(x) being a function (Pun intended). Instead I would consider a different sentence.
AxEy(Man(x) & Woman(y) & Likes( x, y ) -> Likes(alex, x ))
Let's see what happens if x=p2 and y=p1. In our model the premise
Man(p2) & Woman(p3) & Likes( p2, p3 )
holds, and the conclusion
Likes(p1,p2)
also holds, therefore the formula is true under this variable assignment.
Now consider a different model. This time with four individuals: p1,p2,p3,p4.
This model also satisfies our informal specification as Alex likes p2 who is a Man and likes p3 who is a Woman.
Consider the assignment x=p4 and y=p3.
Once again the premise holds in our model
Man(p4) & Woman(p3) & Likes( p4, p3 )
however the conclusion
Likes(p1,p4)
does not hold in our model. Since x is universally quantified this might be a problem as the formula does not hold under this assignment, however y is under an existential quantifier. Let's see if we can find an assignment for y that would turn our formula into a true statement with x=p4.
This is indeed possible. Let y=p2.
Man(p4) & Woman(p2) & Likes( p4, p2 )
does not hold, therefore the formula
Man(p4) & Woman(p2) & Likes( p4, p2 ) -> Likes(p1,p4)
is true. This sounds better yet to satisfy the formula we took an assignment that is far from the intended meaning of the informal specification. The original specification clearly was not speaking about a man who likes another man. So we are not done yet.
Consider a model with just two individuals: p1 and p2.
The informal specification does not hold in this model, so our sentence also should be false. There are four possible assignments of variables
Since Like(x,y) is always false in our model, the premise fails therefore according to the rules of implication, the formula is true. So our sentence is also true in a model where it should not hold. Once again, our first-order formalization does not hold against the informal specification.
This seems to be a very complex process that we have taken to test the translation. It assumes a certain skill of finding counterexamples and always keeping in mind the intended meaning of the informal specification.
Let's look back at our informal specification
Informal specification: Alex likes a man who likes a woman
and reformulate it in a way that is easier to translate
There exists a man whom Alex likes, and this man likes some woman
There are two parts in this sentence connected with an and
So we have
Ex (Man(x) & Likes(Alex,x) & Ey (Woman(y) & Likes(x,y))).
You like prenex normal forms where all quantifiers are collected in one quantifier prefix. We can apply logical equivalence to get
ExEy (Man(x) & Likes(Alex,x) & Woman(y) & Likes(x,y)).
Now let's check if this statement agrees with the specification in each of the structures from the previous section.
Since the variables are existentially quantified and the specification holds, we need to find only one satisfying assignment for the formula.
Consider
The conjunction holds under this assignment.
The same assignment as in the previous subsection can be used. In fact Structure 1 is an substructure of Structure 2. For an existentially quantified statement we know that if it is true in a substructure, it is also true in the whole structure.
Since there is no pair of elements (x,y) such that Likes(x,y) in our structure, the conjunction
Man(x) & Likes(Alex,x) & Woman(y) & Likes(x,y)
cannot be true, so the statement is false. We also know that Structure 3 does not satisfy our informal specification, so our formula has passed our tests.
Our testing procedure is by no means complete. However it gives us some assurance that the translation is indeed correct.