Is property with exact cardinality one functional?

Question

In an OWL-DL ontology, consider a property p with domain D and range R where D has a restriction over p to have cardinality of exactly one:

D SubClassOf p exactly 1 Thing

• (D ⊑ =1 p.Thing)

Can we then infer that p is a functional property, since each d of type D will have exactly one value for p? If this is correct, can a reasoner infer this knowledge?

Answer 1

In OWL, a property is function when each individual has at most one value for the property. That "at most" is important; it is permitted for something to have no value for the property. (That means that a functional property in OWL is actually more like a possibly partial function in mathematics.) That said, if every individual has a exactly one value for a property, then it clearly has at most one value for the property, so the property would, as you suspect, be functional. We can walk though a specific case, though, to be sure that this is general, and because we need to make sure that the property p here actually has at most one value for every individual.

Proof: Suppose the property p has domain D, and D is a subclass of =1 p.Thing, so that every D has exactly one p value. Is it the case that every individual x has at most one value for p? There are two cases to consider:

1. x is a D. Then by the subclass axiom with the restriction, x must have exactly one value for p, and one is less than or equal to one.
2. x is not a D. Then x has no values for p. If it did, then it would be in the domain of p, which is D, and that is a contradiction. Then x has zero values for p, and zero is less than or equal to one.

Then any individual x at most one value for the property p, which is the definition of p being functional. Thus, p is functional. QED

An OWL DL reasoner should be able to confirm this, and it shouldn't be hard to check.