[
Lists Home |
Date Index |
Thread Index
]
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
|
