[SCL] Identity and Horrocks sentences

[Michael Gruninger]

pat hayes wrote:

> >
> >Not sure what you mean.  Upward and downward L-Sk hold for both FOL and
> >FOL=.
>
> Upward doesn't: (forall (?x ?y)(?x = ?y)) doesn't have a countable
> model in FOL=, does in plain FOL. Countable means cardinality
> aleph-0, right?
>

You lost me on this one.
Any model of the sentence
(forall (?x ?y)(?x = ?y))
has cardinality 1, but this doesn't mean that Upward LST fails.
One condition for the theorem is that the theory has infinite models
(which is not true for your sentence).

- michael