[
Lists Home 
Date Index 
Thread Index
]
Thomas B. Passin wrote,
> [Miles Sabin]
> > This is easy to express in secondorder logic, or in firstorder
> > logic plus set theory (the "plus set theory" bit means that you can
> > forget about decidability). Not so easy in plain firstorder 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 firstorder theories (ie. they're expressed in firstorder
logic) but they're not firstorder 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 firstorder settheory 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: firstorder logic plus settheory.
> 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 firstorder _theory_, but it's not firstorder _logic_. Chances
are that the firstorder theory of widgetcoloursurchages will be
decidable, but that's not true of firstorder theories in general: viz.
arithmetic, settheory ...
And this is where the constraint that Len was complaining about bites:
the baselevel logical frameworks being considered for the SW insist on
decidability, and that excludes many practically useful, tho' formally
undecidable firstorder theories.
Here's something else you might try to firstorderize nicely,
Some widgets attach only to one another
You can express this is secondorder 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 firstorder 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 secondorder logic nor firstorder 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
