On Fri, Jul 6, 2012 at 12:41 PM, Michael Brunnbauer <brunni@xxxxxxxxxxxx> wrote:
On Fri, Jul 06, 2012 at 09:53:58AM -0500, Pat Hayes wrote:
Also, using CL or RDF allows you to treat the realtions as first-class entities and quantify over them. This immediately removes one class of arguments in favor of the 'constituent' view, that it is necessary to quantify over these things that are realtions in a relational view, and you cannot quantify over relations in a first-order formalism. You CAN quantify over relations in a first-order formalism.
This is interesting. What defines a first order formalism then ? That it has
a complete deductive calculus ?
I'm sure Pat has the usual characterization of Lindström in mind — a system is first-order if it is compact and has the downward Löwenheim-Skolem property.
Am I right that OWL allows quantification over properties via class axioms
combined with class descriptions ?
To some extent, although classes are extensional in OWL.
So someone trying to define OWL FOL would have to be careful to stay in first
order logic because Properties are first class entities ? Would that be a
difficult problem ?
As long as one adds no special semantic requirement that there must be as many properties as there are sets of individuals (which, by Cantor's Theorem, is simply impossible to require if properties are "first-class entities", i.e., a species of individual), there is no risk of moving beyond first-order logic.