**Warning:**

This wiki has been archived and is now read-only.

# BrokenOwl1FullFeaturesWithArgumentLists

This document describes the technical problems behind Issue 120.

## Contents

## The problem with the main semantic conditions

The main semantic conditions for the sequence-based axioms were wrongly defined. This error leads to inconsistency of every ontology that makes use of any sequence based axiom. In particular, due to the comprehension principles for the sequence based axioms the empty graph consists of unions, intersections, and enumerations, and this leads to inconsistency of OWL 1 Full eventually.

The following example shows the the original main semantic condition for 'owl:unionOf' axioms in OWL 1 Full. For better understanding, the (normally not presented) global universal quantor has been put in front of the condition:

∀ c, l, n, d_1, ..., d_n: (c,l) ∈ EXT_I(S_I(owl:unionOf)) IF AND ONLY IF c ∈ IOC, l is a sequence of d_1, ..., d_n over IOC, CEXT_I(c) = CEXT_I(d_1) ∪ ... ∪ CEXT_I(d_n)

Note that for the ONLY-IF direction the variables *d_1*, ..., *d_n* are not mentioned in the antecedent.
This allows for interpreting these variables *arbitrarily* in the consequent.
The problem can be characterized more generally by the following "law of prenexity":

( ∀x: A → B(x) ) ↔ ( A → ∀x: B(x) )

where the variable *x* must not occur free in the predicate *A*.

### Unsatisfiability of every ontology which uses sequence based axioms

*Note:*
The inconsistency of an arbitrary ontology containing sequence based axioms is *not* dependent on comprehension principles.

Consider the following ontology O:

O := { C owl:unionOf _:l1 . _:l1 rdf:first D . _:l1 rdf:rest rdf:nil . }

Normally, this ontology should be satisfiable. However, we receive from the ONLY-IF semantics of the original semantic condition, after applying the "prenexity law" mentioned above:

∀ n, d_1, ..., d_n: _:l1 is a sequence of d_1, ..., d_n over IOC, CEXT_I(C) = CEXT_I(d_1) ∪ ... ∪ CEXT_I(d_n)

Neither the original length of the list starting with bNode _:l1,
nor the list content (the class D) matters here anymore.
Since the universal quantifier has been moved to the front of the consequent of the ONLY-IF condition,
_:l1 becomes the starting bNode of *every* possible list of arbitrary length *n*
consisting of arbitrary existing classes *d_1, ..., d_n*.
Since owl:Thing and owl:Nothing are two classes that exist for each OWL Full interpretation,
the following two statements are valid specializations of the above universally quantified statement:

_:l1 is a sequence of S_I(owl:Thing), CEXT_I(C) = CEXT_I(S_I(owl:Thing))

and

_:l1 is a sequence of S_I(owl:Nothing), CEXT_I(C) = CEXT_I(S_I(owl:Nothing))

And since CEXT_I(S_I(owl:Thing)) != CEXT_I(S_I(owl:Nothing)), we receive CEXT_I(C) != CEXT_I(C), i.e. the triple "C owl:unionOf (D)" denotes a contradiction in OWL 1 Full, i.e. the ontology O is not satisfiable.

### Inconsistency of OWL Full

*Note:*
The inconsistency of OWL Full demands the existence of the comprehension principles.

The empty RDF graph Full-entails the following statement:

owl:Thing rdf:type owl:Thing

By means of the comprehension principles for owl:unionOf and lists, we receive the following entailment in the empty graph:

{} |= { _:x owl:unionOf _:l1 . _:l1 rdf:first owl:Thing . _:l1 rdf:rest rdf:nil . }

With D := owl:Thing, the inconsistency of the empty graph follows in an analog way as above.

### Remedy

The straightforward repair works by pulling the sequence out of the IFF condition as a "guard":

IF l is a sequence of d_1,...,d_n over R_I THEN (c,l) ∈ EXT_I(S_I(owl:unionOf)) IF AND ONLY IF c ∈ IOC, d_1, ..., d_n ∈ IOC, CEXT_I(c) = CEXT_I(d_1) ∪ ... ∪ CEXT_I(d_n)