Skolemization with multiple arguments -- how to unify

Edit: answerers keep finding (valid!) problems with my example. I'll try again. The older version is below the horizontal line. Thanks to Klaus below for pointing out the last problem.

My question is how to unify skolemizations that have differing numbers of arguments. As he points out, there is rarely any need for this. For example, if the statements are

Some homes are blue.
There is a home with two stories.

The skolemizations here should not unify, because we can't know from this if a blue home is two-storied.

If we're going to ever need to unify one skolemization with another, we'll need to know we're talking about the same home. This would do it:

Jane's and Mark's home is blue (their only home).
Jane's home has two stories (her only home).

Here it is in FOPC:

$$
\exists x: has(Jane,x) \wedge has(Mark,x) \wedge home(x) \wedge blue(x) \wedge
$$
$$
(\forall y: has(Jane,y) \wedge home(y) \implies x=y) \wedge
$$
$$
(\forall y: has(Mark,y) \wedge home(y) \implies x=y)
$$
and
$$
\exists x: has(Jane,x) \wedge home(x) \wedge twoStories(x) \wedge (\forall y: (has (Jane,y) \wedge home(y) \implies x=y)
$$

Converting to conjunctive normal form with skolemization gives us this set:

$$
has(Jane,skolem1(Jane,Mark))
$$
$$
has(Mark,skolem1(Jane,Mark))
$$
$$
home(skolem1(Jane,Mark))
$$
$$
blue(skolem1(Jane,Mark))
$$
$$
\neg has(Jane,y) \vee \neg home(y) \vee skolem1(Jane,Mark) =y
$$
$$
\neg has(Mark,y) \vee \neg home(y) \vee skolem1(Jane,Mark)=y
$$

$$
home(skolem2(Jane))
$$
$$
twoStories(skolem2(Jane))
$$
$$ \neg has (Jane,y) \vee \neg home(y) \vee skolem2(Jane)=y
$$

Now, if I want to reason about whether there's a blue house with two stories -- which I should be able to start by resolving the first and last clauses in the set -- I can't, because the two skolemizations can't unify: they have different numbers of arguments.

Is there a good protocol of picking arguments to prevent this problem -- other than a

"Everyone has a heart" gets first encoded first as $\forall x. \text{Person}(x) \Rightarrow \exists y. \text{Hart}(y) \wedge \text{Has}(x,y)$. Then you get the Skolemization (that you found in RN) from that.

Now "Everybody who has a house pays utilities" is just $\forall x. \text{Houseower}(x) \Rightarrow \text{PaysUtilities}(x)$ because there is no assertion that anything exists in this statement. However, if you want to spell out what houseowner means, $\forall x.\text{Houseowner}(x) \Leftrightarrow (\text{Person}(x)\wedge\exists y.\text{House}(y) \wedge Has(x,y))$. And you can skolemize that... but it's not even needed for what you want to infer.

As to "Jane and Mark have a house", it's actually a bit ambiguous. Do they have the same house? But that's an irrelevant detail if you just encode $\text{Houseower}(\text{Jane}) \wedge \text{Houseower}(\text{Mark})$. From that it immediately follows that $\text{Houseower}(\text{Jane})$ and using $\forall x. \text{Houseower}(x) \Rightarrow \text{PaysUtilities}(x)$ it follows that $\text{PaysUtilities}(\text{Jane})$ with the obvious unification $x=\text{Jane}$.

As you can see, the definition of houseowner (which asserts the existence of a house etc.) is completely irrelevant to the inference you wanted. In general, not every "has" in the English language gets translated into a binary predicate, unless it's relevant to what you want to prove. Nobody managed to invent a rigorous way to formally and universally translate all of English (or any other natural language) into first-order logic. While there are some guidelines, a translation of a problem statement from natural language to FO ultimately uses a problem-specific encoding method.

Also note that your first sentence "Everybody who has a house pays utilities" bears some resemblance to a donkey sentence, but it's not actually one; you'd have to say "Everybody who has a house pays utilities on it" to get a donkey sentence.

StackExchange Computer Science Q#40114, answer score: 2