Why is OWL Full undecidable?

Question

I've been looking all around on why OWL Full is undecidable, but I haven't found an easy to understand example that would lead me to comprehend it.

I've found statements that explain that it is due to "Entailment Closure" and that is also correlated with the fact that OWL Full can have Classes that are Properties and that are also Individuals all at the same time.

But I don't understand the relationship between those statements.

Answer 1

Here is an example that should be sufficient to understand why OWL 2 Full is undecidable. This has something to do with Russel's paradox.

In OWL Full, you can define a class that has itself as an instance:

:IsInstanceOfItself  a  :IsIntanceOfItself .

This is also possible in RDF/RDFS but it does not make the logic undecidable. What leads to undecidability is the fact that you can define classes that are paradoxical in OWL 2 Full. You can define the class of classes that have themselves as instances:

:HaveThemselvesAsInstance
    rdfs:subClassOf  [
        a  owl:Restriction;
        owl:onProperty  rdf:type;
        owl:hasSelf  true
    ] .

Then you can define the classes that do not have themselves as instances:

:DoNotHaveThemselvesAsInstance
    owl:equivalentClass  [ owl:complementOf  :HaveThemselvesAsInstance ] .

Now, we can ask the question: is :DoNotHaveThemselvesAsInstance an instance of itself? Assume that it is the case. Then:

:DoNotHaveThemselvesAsInstance  a  :DoNotHaveThemselvesAsInstance .

is true. Therefore, :DoNotHaveThemselvesAsInstance abides by the definition that it's in a class where there is no relationship with itself with the rdf:type property. So the assumption is wrong. Therefore :DoNotHaveThemselvesAsInstance must be in the complement of those classes that have rdf:type with themselves. So it must be an instance of :DoNotHaveThemselvesAsInstance. So the assumed relationship above should hold. Back to the initial step. Consequently, there cannot be any model for any ontology that defines the class defined above. So there cannot be a class of classes that do not have themselves as instance. So perhaps, all classes have themselves as instances, perhaps? But there are models of ontologies where some classes are not instances of themselves. So... OWL 2 Full is really fucked up, isn't it?

Answer 2

Your question makes a lot of sense and it's not easy to answer. Also, the distinction between OWL-DL and OWL-Full is not fixed. Something initially restricted in OWL has been later on allowed, the most popular case being that of punning.

But basically, the idea is to be able to write a reasoner that can answer yes or no and avoid don't know or an "infinite" don't know yet. This 30min lecture on Tableaux Algorithm and maybe a couple of others before and after in the same course might help.

By the way, undecidability and impossibility of computing entailment closure are not the same thing.