# Re: Semantic Web and First Order Logic

```Thomas B. Passin wrote,
> [Miles Sabin]
> > This is easy to express in second-order logic, or in first-order
> > logic plus set theory (the "plus set theory" bit means that you can
> > forget about decidability). Not so easy in plain first-order logic.
>
> Hmm, it depends on your definition of FOL, I suppose, and it also
> depends on how you model things.  I assumed that FOL includes types
> and your "plus set" stuff

Those'd be first-order theories (ie. they're expressed in first-order
logic) but they're not first-order logic. And they're not necessarily
decidable (a type theory might be, set theory isn't).

> (but a set of individuals is a kind of quantifier over individuals, is
> it not?).

In first-order set-theory a set of individuals is an individual in it's
own right, not a quantifier.

> I take it that in FOL, quantifiers range over individuals while in
> second order logic, quantifiers can range over predicates and
> relations. Is that what you understand?

More or less.

> Applying this to your example,  if you used Red(widget), then your
> statement would be about the predicate (ie., Red), and therefore
> second order, right?

Yup.

> But the redness can be modeled in other ways.

Oh, sure. I mentioned one: first-order logic plus set-theory.

> For example, we could say Color(x,red) and IsPrimaryColor(red).  Then
> your example could be stated something like this -
>
> {for all x,y| Widget(x) and Color(x,y) and IsPrimaryColor(y)}==>
> Surcharge(x,5%)
> {Widget(x) and Color(x,red)}
> {IsPrimaryColor(red)}
>
> Now we are only making statements about the arguments, and they are
> individuals, not predicates or relations.  So it is FOL, right? And
> an SQL query could extract the surcharge from a database.

It's a first-order _theory_, but it's not first-order _logic_. Chances
are that the first-order theory of widget-colour-surchages will be
decidable, but that's not true of first-order theories in general: viz.
arithmetic, set-theory ...

And this is where the constraint that Len was complaining about bites:
the base-level logical frameworks being considered for the SW insist on
decidability, and that excludes many practically useful, tho' formally
undecidable first-order theories.

Here's something else you might try to first-orderize nicely,

Some widgets attach only to one another

You can express this is second-order logic,

{exists P |
{exists x | Px } and
{for all x |
Px ==>
Widget(x) and {for all y | attach(x, y) ==> Py } } }

and you can express it in first-order set theory,

{exists X |
{exists x | member(x, X) } and
{for all x |
member(x, X) ==>
Widget(x) and {for all y | attach(x, y) ==> member(y, X) } } }

but neither second-order logic nor first-order set theory are decidable,
so neither of these renderings is compatible with the frameworks touted
for the SW which respect the decidability constraint. Can you come up
with a rendering which is?

OTOH, can you persuade me that this kind of assertion is irrelevant to
business applications? All it's doing is saying that there's a binary
relation ("attach" in the example) which partitions the domain of
widgets in a particular way. That seems like a useful kind of thing to
be able to say.

Cheers,

Miles
```

### PURCHASE STYLUS STUDIO ONLINE TODAY!

Purchasing Stylus Studio from our online shop is Easy, Secure and Value Priced!

### Download The World's Best XML IDE!

Accelerate XML development with our award-winning XML IDE - Download a free trial today!

Don't miss another message! Subscribe to this list today.
Email
First Name
Last Name
Company
Subscribe in XML format
 RSS 2.0 Atom 0.3 Stylus Studio has published XML-DEV in RSS and ATOM formats, enabling users to easily subcribe to the list from their preferred news reader application.

 Stylus Studio Sponsored Links are added links designed to provide related and additional information to the visitors of this website. they were not included by the author in the initial post. To view the content without the Sponsor Links please click here.