Inquiry into RDF and OWL Semantics

Abstract

The purpose of this paper is to present the higher order formalization of RDF and OWL with setting up ontological meta-modeling criteria through the discussion of Russell’s Ramified Type Theory, which was developed in order to solve Russell Paradox appeared at the last stage in the history of set theory. This paper briefly summarize some of set theories, and reviews the RDF and OWL Semantics with higher order classes from the view of Russell’s Principia Mathematica. Then, a set of criteria is proposed for ontological meta-modeling. Several examples of meta-modeling, including sound ones and unsound ones, are discussed and some of solutions are demonstrated according to the meta-modeling criteria proposed.

1 Introduction

The OWL specifications has been split into two parts, Direct Semantics and RDF-based Semantics. The reason of this unhappy partition originates in the different formalizations between OWL DL and RDF. In order to match DL-based semantics to RDF-based semantics, the term of “comprehension conditions (principles)” is introduced into “OWL Semantics and Abstract Syntax, Sect. 5” (Patel-Schneider et al. 2004a) and “OWL 2 Web Ontology Language RDF-Based Semantics (Second Edition)” (Schneider 2014). In addition, “RDF-Compatible Model-Theoretic Semantics” (Patel-Schneider et al. 2004a) states that the only-if semantic conditions are necessary to prevent semantic paradoxes with the fourteen comprehension conditions, and OWL2 Appendix¹ mentions “formal inconsistency” instead of “paradox”. However, these statements are caused by misunderstanding paradoxes in set theories, and the word “comprehension conditions” is still left in “OWL2 (Second edition)”.

Granted that no choice but to introduce some postulates in order to make OWL semantics compatible to RDF semantics, this misunderstanding is partly attributed to RDF semantics itself; indeed, there are not enough explanations in RDF Semantics (Hayes 2004) on the setup of preventing “membership loops”. Hayes only claimed that the semantic model distinguishes both properties and classes, regarded as objects, from their extensions, so that this distinction prevents “membership loops”. He also stated that the violation of the axiom of foundation, which is one of the axioms of standard set theories like Zermelo-Fraenkel (ZF) that forbids infinitely descending chains of membership, does not happen in RDF. However, the mechanism of preventing membership loops is still obscure for readers of RDF Semantics.

In this paper, at Sect. 2, we describe Russell paradox that has roots in Cantor’s naive set theory, and summarize the history of set theories for the resolution of the paradox. At Sect. 3, we review RDF Semantics and OWL Semantics with higher order classes. Then, at Sect. 4, we propose a set of criteria for higher order classes and ontological meta-modeling. Those criteria are actually derived from the axioms and principles introduced in Ramified Type Theory for the resolution of Russell paradox in Principia Mathematica (PM, Vol.1). At Sect. 5, several examples of meta-modeling, including sound ones and unsound ones, are discussed, and some of solutions are demonstrated according to the meta-modeling criteria presented here.

We call the OWL Full with these criteria Restricted OWL Full. Thus, ambiguous word “punning” by W3C is clearly fixed on the meta-modeling with higher order classes and it helps us to deeply understand the semantics and the inference mechanism of RDF/OWL systems that allow ontological meta-modeling.

2 History of Set Theory and Type Theory

The history of set theory is a history of coping with Russell paradox essentially contained by the mathematical concept of set. Russell paradox was resolved in two ways. One is axiom of separation by Zermelo and the other is Ramified Type Theory by Whitehead and Russell. In the current set theory, a set is discriminated from a class that cannot be a member of set². It is simply stated by Bourbaki (Bourbaki 1966) that there are two sorts of relations, i.e., relations which can make sets and which cannot make sets. This section abstracts set theories by Cantor, Zermelo, type theories by Russell, and the resolution of Russell paradox in Knowledge Interchange Format (KIF 1994).

2.1 RDF Sematics and Sets of Objects

RDF semantics is built on the foundation of set theory as well as every other formal theory in mathematics and logics. In fact, Hayes invokes a set theory named Zermelo-Fraenkel in order to rationalize membership loops that do not cause any paradoxes.

When classes are introduced in RDFS, they may contain themselves. Such ‘membership loops’ might seem to violate the axiom of foundation, one of the axioms of standard (Zermelo-Fraenkel) set theory, which forbids infinitely descending chains of membership. However, the semantic model given here distinguishes properties and classes considered as objects from their extensions - the sets of object-value pairs which satisfy the property, or things that are ‘in’ the class - thereby allowing the extension of a property or class to contain the property or class itself without violating the axiom of foundation.    (Hayes 2004)

Although the Recommendation claims that the semantic model in RDF semantics does not violate the axiom of foundation on membership loops, yet there are not enough discussions on why and how the membership loops do not violate the axiom of foundation. It only states that for an object x, where is the class extension of x, and $p\ne \mathrm {I\!EXT}(p)$ for a property p, where $\mathrm {I\!EXT}(p)$ is the extension of p.

This paper claims the rdfs:Resource and rdfs:Class are proper classes in sets that do not cause paradoxes on sets, because the extension of rdfs:Resource is a totality and the extension of rdfs:Class is also a totality. A totality is not regarded as a set in today’s theory. So, the rdfs:Resource and the rdfs:Class should be conceived to be a convention of referring the universal class concept and the universal metaclass concept respectively in the universe of discourse.

2.2 Cantor’s Paradox and His Final Legacy

The history of set theories started with Georg Cantor. It is obvious that Cantor assumed members of sets are countable objects and a set is a collection of objects (Cantor 1895). Yet, he actually did not mention about objects, and he clarified the concept of natural numbers based on a (naive) set theory. However, Cantor became to know a paradox (called Cantor’s paradox) contained by his own set theory in case of handling the totality of infinite sets including sets of sets³, and he noticed it in his letter to Dedekind⁴ (Cantor 1967). Aczel wrote,

Cantor’s final legacy, beyond the discovery of the transfinite numbers and the continuum hypothesis, was his realization that there could be no set containing everything ... since, given any set, there is a larger set – its set of subsets, the power set.   (Aczel 2000)

Today, we know the power set $\wp (a)=\{x \mid x \subseteq a \}$ is too powerful for making sets of infinite cardinality, whereby Cantor discovered the transfinite ordinal numbers, but he also opened a door to lead paradoxes involved by set theories.

2.3 Comprehension Principle and Russell Paradox

The followings are some of axioms in naive set theory (Boolos 1971).

$$\begin{aligned} \forall x \forall y \forall z[(z\in x \Leftrightarrow z\in y)\Rightarrow x = y] \end{aligned}$$

(1)

$$\begin{aligned} \exists y\forall x [x\in y \Leftrightarrow x\ne x] \end{aligned}$$

(2)

$$\begin{aligned} \forall z\forall w\exists y\forall x[x\in y \Leftrightarrow (x=z \vee x=w)] \end{aligned}$$

(3)

$$\begin{aligned} \exists y \forall x\exists w[x\in y \Leftrightarrow (x\in w \wedge w\in z)] \end{aligned}$$

(4)

$$\begin{aligned} \exists y \forall x[x\in y \Leftrightarrow x = x] \end{aligned}$$

(5)

The first one is called axiom of extensionality (1), and in order respectively, empty set (2), pairing (3), union (4), and universal (5). Especially, the empty set $\emptyset$ is defined by the second formula, such that $\emptyset \equiv \{ x \mid x \ne x \}$.

The intensional definition of sets such that $\{x \mid \varphi (x) \}$, where $\varphi (x)$ is any formula, is called comprehension principle (Kamareddine et al. 2004).

Definition 1

(Comprehension Principle).

$$\begin{aligned} \exists y\forall x[x\in y \Leftrightarrow \varphi (x)] \qquad \text { where }y \text { is not free in } \varphi (x) \end{aligned}$$

(6)

It was once conceived that the comprehension principle was very natural for intensionally defining a set because any (unary) predicate could be applied to a given object in order to determine the membership of an object to a set that holds a property featured by the formula under the law of excluded middle; namely, we can determine for any objects whether an object belongs to the set or not. Meanwhile, Russell keenly pointed a paradox in sets. If we take $\varphi (x)$ to $x \not \in x$, which intends to denote a set that does not include any membership loops, then it follows that $y = \{x \mid x \not \in x\}$ or $\exists y \forall x[x\in y \Leftrightarrow x \not \in x]$. Then, in case of instantiating an arbitrary x to y, we obtain a contradiction as follows.

Definition 2

(Russell Paradox).

$$\begin{aligned} \exists y[y\in y \Leftrightarrow y \not \in y]. \end{aligned}$$

Russell revealed that the comprehension principle inevitably involves a paradox⁵. J. van Heijenoort stated,

Bertrand Russell discovered what became known as the Russell paradox in June 1901 [...]. In the letter [to Frege], written more than a year later and hitherto unpublished, he communicates the paradox to Frege. The paradox shook the logicians’ world, and the rumbles are still felt today.   (From Frege to Gödel in van Heijenoort 1967)

2.4 Zermelo’s Axiom of Separation

To avoid Russell paradox, Ernst Zermelo replaced the comprehension principle with the axiom of separation (aussonderung) (Kamareddine et al. 2004).

Definition 3

(Axiom of Separation).

$$\begin{aligned} \exists y\forall x[x\in y \Leftrightarrow x\in z\wedge \varphi (x)]\quad \text { where } y \text { does not occur in } \varphi (x) \end{aligned}$$

(7)

In this case, y must be a proper subset of a set z, of which members satisfy the formula. It may be phrased that the paradox is work-arounded by introducing z distinctively existing. Today, a set theory based on a series of axioms by Zermelo is called Zermelo-Fraenkel (ZF) set theory together with Fraenkel’s axiom of replacement.

It is worthy to note that in some of modern computer languages a functionality to make a list whose elements are selected from another list so that they satisfy a specified condition is accidentally misnamed list comprehension ⁶. We claim that this functionality in computer languages should be properly named “list-separation” or “list-selection” in order to avoid misunderstanding between comprehension principle in set theories and list comprehension in computer languages. As well, the term of “comprehension conditions (principles)”, which is strongly associated with paradoxes in sets, in “OWL Semantics and Abstract Syntax, Sect. 5”, should be renamed to “list conditions by selection” or something else, in order to avoid unfounded fear of paradoxes associated with comprehension principle.

2.5 NBG and Set Theory of KIF 3.0

The Knowledge Interchange Format (KIF) 3.0 theory proposed a special set theory that is based on von Neumann-Bernays-Gödel (NBG) set theory. The Chap. 7 of the reference manual (KIF 1994), which is titled “Sets”, starts with the statement below.

In many applications, it is helpful to talk about sets of objects as objects in their own right, e.g. to specify their cardinality, to talk about subset relationships, and so forth. The formalization of sets of simple objects is a simple matter; but, when we begin to talk about sets of sets, the job becomes difficult due to the threat of paradoxes (like Russell’s hypothesized set of all sets that do not contain themselves).

(Knowledge Interchange Format version 3.0 Reference Manual (KIF 1994))

It is obvious that the KIF Group were worried about involving the paradoxes on sets in the KIF specification. NBG allows us to make sets that include individuals and sets or classes of individuals. The axioms in NBG is roughly separated into two parts; one is for sets, in which a set is expressed using variables with lower letters, and the other is for classes, in which a class is expressed using variables with upper letters. Although both parts of axioms are composed of almost same forms, they are separated owing to the idea that classes are a different sort from sets of individuals in NBG.

KIF distinguishes bounded set (set) from unbounded set (proper class). A bounded set can be a member of a set, but an unbounded set cannot be a member of set. A bounded set is finite. A finite set is bounded, but an infinite set is unbounded. It is consistent to the standard set theories, ZF and NBG. KIF contains one more notion, that is, individuals.

In KIF, a fundamental distinction is drawn between individuals and sets. A set is a collection of objects. An individual is any object that is not a set. A distinction is also drawn between objects that are bounded and those that are unbounded. This distinction is orthogonal to the distinction between individuals and sets. There are bounded individuals and unbounded individuals. There are bounded sets and unbounded sets. The fundamental relationship among these various types of entities is that of membership. Sets can have members, but individuals cannot. Bounded objects can be members of sets, but unbounded objects cannot. (It is this condition that allows us to avoid the traditional paradoxes of set theory.)    (KIF 1994, Sect. 7.1 Basic Concepts)

Although we may have a curiosity what unbounded individuals are, there is no explanation in KIF what they are, and the study is beyond the scope of this paper. Russell paradox is described in KIF as follows.

The paradoxes appear only when we try to define set primitives that are too powerful. We have defined the sentence ‘(member $\tau ~\sigma$)’ to be true in exactly those cases when the object denoted by $\tau$ is a member of the set denoted by $\sigma$, and we might consider defining the term ‘(setofall $\tau ~\phi$)’ to mean simply the set of all objects denoted by $\tau$ for any assignment of the free variables of $\tau$ that satisfies $\phi$. Unfortunately, these two definitions quickly lead to paradoxes.

Let $\phi _{\nu /\tau }$ be the result of substituting term $\tau$ for all free occurrences of $\nu$ in sentence $\phi$. Provided that $\tau$ is a term not containing any free variables captured in $\phi _{\nu /\tau }$, then the following schema follows from our informal definition. This schema is called the principle of unrestricted set abstraction.

$$\begin{aligned} (\Leftrightarrow (\mathrm {member}~\tau ~(\mathrm {setofall}~\nu ~\phi ))~\phi _{\nu /\tau }) \end{aligned}$$

(KIF 1994, Sect. 7.4 Paradoxes)

Note that this form is equivalent to the unrestricted comprehension principle (6) and it causes Russell paradox.

Instead of this principle, Russell paradox is avoided in KIF by restricted set abstraction, in which a set is restricted to bounded sets.

In the von-Neuman-Gödel-Bernays version of set theory, these paradoxes are avoided by replacing the principle of unrestricted set abstraction with the principle of restricted set abstraction given above.

$$\begin{aligned} (\Leftrightarrow (\mathrm {member}~\tau ~(\mathrm {setofall}~\nu ~\phi ))~(\mathrm {and}~(\mathrm {bounded}~\tau )~\phi _{\nu /\tau })) \qquad \mathrm {({ ibid.})} \end{aligned}$$

Note that this form resembles the axiom of separation (7) in ZF. Here a bounded object ‘$(\mathrm {bounded}~\tau )$’ is used instead of the restriction ‘${x \in z}$’.

KIF succeeded to eliminate paradoxes by the concept of bounded set of objects, whereas Russell’s Ramified Type Theory is much suitable to explain how RDFS can avoid Russell paradox for the correct comprehension of the framework for meta-modeling⁷.

2.6 Russell’s Ramified Type Theory

Alfred N. Whitehead and Bertrand Russell developed the first type theory, Ramified Type Theory, in the epoch-making three-volume books, ‘Principia Mathematica’ (hereafter PM for short). They attempted to solve the Russel paradox together with other paradoxes by capturing them as variations of vicious circle.

An analysis of the paradoxes to be avoided shows that they all result from a certain kind of vicious circle.   (PM, Vol.1, Introduction, Chap. 2)

They emphasized that statements about “all propositions” are meaningless owing to the totality contained in the statements.

[...] if we suppose the set to have a total, it will contain members which presuppose this total, then such a set cannot be a total.   (ibid.)

Therefore, they, first of all, postulate the vicious-circle principle in order to avoid paradoxes caused by self-reference.

The principle which enables us to avoid illegitimate totalities may be stated as follows: “Whatever involves all of a collection must not be one of the collection”; or, conversely: “If, provided a certain collection had a total, it would have members only definable in terms of that total, then the said collection has no total.” We shall call this the “vicious-circle principle”, [...]    (ibid.)

Whitehead and Russell introduced the idea of propositional function, in which sentences may include variables for not only objects but also functions⁸, and value assignments for all variables of objects and functions turn open sentences unambiguous propositions. Thus, functions are also applied to as logical expression. For example, Leibniz equality of $x = y$ is defined as $\forall f [ f(x) \Leftrightarrow f(y) ]$.

Ramified Types. Types in PM have a double hierarchy, that is, (simple) types and orders. The second hierarchy is introduced by regarding also the types of the variables that are bound by a quantifier. Kamareddine, et al. explained the reason using a propositional function $z(\,) \vee \lnot z(\,)$, which can involve an arbitrary proposition for z, then $\forall z\!\uparrow \!(\,)[z(\,) \vee \lnot z(\,)]$ ⁹ quantifies over all propositions for z in the universe. We must distinguish a simple proposition C(a) and quantified $\forall z\!\uparrow \!(\,)[z(\,) \vee \lnot z(\,)]$. The former does not involve any self-reference but the latter may involve the self reference for z. This problem is solved by dividing types into orders. An order is simply a natural number that starts with 0, and in $\forall z\!\uparrow \!(\,)[z(\,) \vee \lnot z(\,)]$ we must restrict the form by mentioning the order of propositions. Thus, propositional function of the form $\forall z\!\uparrow \!(\,)^n[z(\,) \vee \lnot z(\,)]$ quantifies over only all propositions of order n, and this form has its own order $n+1$.

Definition 4

(Ramified Types). PM explained ramified types for only unary and binary functions. Kamareddine, et al. extended the definition to n-ary. (Kamareddine et al. 2004).

• 1. $0^0$ is a ramified type;

• 2. If  $t_1^{a_1}, \dots , t_n^{a_n}$ are ramified types and , then $(t_1^{a_1}, \dots , t_n^{a_n})^a$ is a ramified type (if $n=0$ then take $a\ge 0$) ;

• 3. All ramified types can be constructed using rules 1 and 2.

Note that in $(t_1^{a_1}, \dots , t_n^{a_n})^a$ we demand that $a > a_i$ for all i. Furthermore, Whitehead and Russell defined predicative condition on ramified types.

Definition 5

(Predicative Types).

$$\begin{aligned} (t_1^{a_1}, \dots , t_n^{a_n})^a ~~~~~\mathrm {where}~~ a=0 ~~\mathrm {if}~~ n=0, ~\mathrm {else}~ a = 1 + max(a_1, \dots , a_n) \end{aligned}$$

The followings are some examples of predicative types.

• $0^0$;

• $\left( 0^0\right) ^1$;

• $\left( \left( 0^0\right) ^1,\left( 0^0\right) ^1\right) ^2$;

• $\left( \left( 0^0\right) ^1,\left( \left( 0^0\right) ^1,\left( 0^0\right) ^1\right) ^2\right) ^3$.

The above expressions of ramified types are also expressed as follows by Stevens (Stevens 2003) using function symbol F, G, H, and I, and their arguments.

• $^0x^0$;

• $^1F^{(0/0)}(^0x^0)$;

• $^2H^{(1/(0/0),1/(0/0))}\left( ^1F^{(0/0)}(^0x^0),{^1G^{(0/0)}}(^0y^0)\right)$;

• $^3I^{(1/(0/0),2/(1/(0/0),1/(0/0)))}\left( ^1F^{(0/0)}(^0x^0), {^2H^{(1/(0/0),1/(0/0))}}\right)$.

Here the first 0 in (0 / 0) stands for the order as argument and the last 0 stands for the type as argument at the individual level. 1 in 1 / (0 / 0) stands for the order as first order as argument. The prefix number of function stands for orders of the form.

Suggested by ramified types, we can put orders to classes on RDF semantics with interpreting a class name as unary predicates in predicate calculus or propositional functions in PM. In the next section, we attempt to formalize RDF semantics taking into account of orders in Ramified Type Theory for classes, and claims that RDFS may avoid Russell paradox.

3 Formalization of RDF/OWL Semantics Based on Higher Order Types

3.1 Preliminary Explanations of Notations, Denotations, and Universe of Discourse

Notation. In this formulation, $\mathbb {R}$ stands for the universe of discourse, $\mathcal {P}$ stands for a finite set of logical predicate symbols, $\mathcal {F}$ stands for a finite set of functional symbols, and $\mathcal {V}$ stands for a countable set of vocabularies. Every sentence in this formulation is a triple like $\langle s, p, o\rangle$ composed of words in a vocabulary in $\mathcal {V}$.

Interpretation $\mathcal {I}$ is a mapping from a set of triples and vocabularies $\mathcal {V}$ into the universe of discourse $\mathbb {R}$. Logical symbols, i.e., $\in$ (relation between elements and a set), $\subseteq$ (inclusiveness among sets), $\sqsubseteq$ (sub/super concept of class relation), are used in addition to common logical connectives $\wedge$ (conjunction) and $\vee$ (disjunction). In the domain of RDF and OWL, $\mathcal {F}$ contains only (extension of property) and (extension of class).

There are no variables except for blank nodes in RDF and OWL. So, note that every symbol in RDF and OWL standing for an object is a constant term in logics. However, discussions on sets require variables. Thus, variables for sets are expressed x, y, ...or $x_1$, $x_2$, ..., and $x_i$, $y_i$. When we indicate variables in logical forms, they may be explicitly expressed with quantifiers $\forall$ or $\exists$.

Tarskian Denotational Semantics. We discriminate sentences and words in sentences from their denotations (Tarski 1946). For example, a word “Tokyo” as logical term $\textit{Tokyo}$ interpreted as a city named Tokyo in Japan, and the denotation is expressed as $\mathcal {I}[\![\textit{Tokyo}]\!]$ or $\textit{Tokyo}^\mathcal {I}$. In this case, we say “$\textit{Tokyo}$ denotes $\textit{Tokyo}^\mathcal {I}$” or “$\textit{Tokyo}^\mathcal {I}$ is the denotation of $\textit{Tokyo}$” for $\mathcal {I}[\![\textit{Tokyo}]\!] = \textit{Tokyo}^\mathcal {I}$. In this representation, $x = x$ is interpreted as $x^\mathcal {I} = x^\mathcal {I}$ (as tautology), and $a = b$ is interpreted to $a^\mathcal {I} = b^\mathcal {I}$ (when both denotations are identical). A sentence denotes truth value, of which truth or falsity is decided depending on rules of interpretation and models constructed by ontologists. For example, $\textit{New\_York}^\mathcal {I} = \textit{Apple\_City}^\mathcal {I}$ is true in some case or false in another case.

The interpretation by denotational semantics do not require us to make unique name assumption. We represent $a \simeq b$ for owl:sameAs and $a \not \simeq b$ for owl:differentFrom in OWL sentences. Then, the followings hold on different nodes of RDF graph $a^\mathcal {I}$ and $b^\mathcal {I}$ in OWL¹⁰.

$$\begin{aligned} \mathcal {I}[\![a \simeq b]\!] \Rightarrow a^\mathcal {I} = b^\mathcal {I} \\ \mathcal {I}[\![a \not \simeq b]\!] \Rightarrow a^\mathcal {I} \not = b^\mathcal {I} \end{aligned}$$

Universe of Discourse by Set Theory. In set theories, a set is extensionally defined by enumerating all members of the set, or intensionally defined by using logical conditions that all members in the set satisfy, which is like comprehension principle. However, the expression $x^\mathcal {I} = x^\mathcal {I}$ is always true in any case, thus the universe of discourse that stands for the totality can be defined as follows,

$$\begin{aligned} \mathbb {R} \equiv \{{x^\mathcal {I}} \mid {x^\mathcal {I}} = {x^\mathcal {I}}\} . \end{aligned}$$

Note that $\mathbb {R}$ as the universe of discourse can contain all denotations (objects in models), and every entity in the universe always belongs to $\mathbb {R}$ because ${x^\mathcal {I}} = {x^\mathcal {I}}$ is always true for any $x^\mathcal {I}$. Also note that this form looks like a set but $\mathbb {R}$ is actually not a set but a proper class that contains everything in the universe and cannot be a member of a set.

Property Extension. In this paper, the interpretation of a triple $\langle s, p, o\rangle$ or $\langle s, o\rangle \in \mathrm {EXT}(p)$ is represented as $\langle s^\mathcal {I}, o^\mathcal {I}\rangle \in \mathrm {I\!EXT}(p^\mathcal {I})$,

$$\begin{aligned} \mathcal {I}[\![\langle s, o\rangle \in \mathrm {EXT}(p)]\!] \Rightarrow \langle s^\mathcal {I}, o^\mathcal {I}\rangle \in \mathrm {I\!EXT}(p^\mathcal {I}) . \end{aligned}$$

$\mathrm {I\!EXT}(p^\mathcal {I})$ is called the (semantic) extension of property $p^\mathcal {I}$. $\mathrm {I\!EXT}(p^\mathcal {I})$ is a mapping into the powerset of direct product $\mathbb {R} \times \mathbb {R}$, thereby the arguments $x^\mathcal {I}$ and $y^\mathcal {I}$ of an ordered pair $\langle x^\mathcal {I},y^\mathcal {I} \rangle$ are in $\mathbb {R}$, namely, ($x^\mathcal {I} \in \mathbb {R} \wedge y^\mathcal {I} \in \mathbb {R}$)¹¹.

Class Extension. We express a triple $\langle s, rdf\!:\!type, o\rangle$ as $s\!\uparrow \!o$ in this paper, then the class extension can be captured as a set of which members can be interpreted as instances of classes. Namely, for an instance $x^\mathcal {I}$ of class $y^\mathcal {I}$,

is called the (semantic) class extension of class $y^\mathcal {I}$.

3.2 Higher Order Classes

We introduce orders into the description of RDFS classes. Namely,

Here n and m is an order of class x and y, respectively. When exactly $m = n + 1$, we call it predicative as well as PM.

Definition 6

(Predicative Classes).

(8)

(9)

We distinguish $^nx^\mathcal {I}$ from $^{n+1}x^\mathcal {I}$ as different nodes in an RDF graph, while the x is the same lexical token as IRI or nodeID in $\mathcal {V}$. Therefore, we can obtain the following lemma without violating vicious circle principle,

Lemma 1

(10)

(11)

We assume that rdf:type has the same role in the universe from $n = 0$ to $\infty$. This is actually the same as axiom of reducibility (PM, Vol.1, Introduction, VI), which is required to enable that there exists a (higher order) function as formally the same as the predicative function that takes individuals as arguments. We extend this principle to every RDF and OWL properties later on.

3.3 Subsumption in Higher Order Classes

The RDFS semantic condition on rdfs:subClassOf contains the following condition that is obtained with extending RDFS-original classes to higher order classes,

Here $\sqsubseteq$ represents subclass-superclass relation that is designated by rdfs:subClassOf, and $\mathbb {C}$ may be called the universal domain of classes, to which all classes in the universe of discourse belong. The above condition is called subsumption.

Then, we introduce a new notion onto the subsumption by higher order classes. If $n = m$ on the above condition, let us call it interpretable.

Definition 7

(Interpretable Class Condition).

(12)

Namely, both classes related by rdfs:subClassOf must be the same order.

The order n of classes should be greater than zero $(n > 0)$, since order 0 is assigned only individuals and an individual cannot have its own extension. Note that this interpretable class condition is constructively obtained in accordance with the definition of “being of the same type” PM *9.131, in which it is stated u and v “are the same type,” if “(1) both are individuals, (2) both are elementary functions taking arguments of the same type”. Individuals are interpretable. So, the first order classes are also interpretable. Then, we consider rdfs:subClassOf relation among the first order classes also interpretable. Thus, this procedure may be repeated again and again from order 0 to order n.

3.4 Universal Class in Higher Order Classes

As shown in the entailment rule rdfs4a and rdfs4b (Hayes 2004), every entity in the universe of discourse is an instance of $rdfs \!:\! Resource ^\mathcal {I}$,

RDFS entailment lemma in (Hayes 2004) states that every entity as class is a subclass of the class rdfs:Resource,

$$\begin{aligned} \vdash \forall c^\mathcal {I}[{c^\mathcal {I}} \sqsubseteq { rdfs\!:\!Resource ^\mathcal {I}}]. \end{aligned}$$

We extend these forms for entities and classes to higher order classes in the universe as well as described above.

(13)

$$\begin{aligned} ~~~~~~~~\vdash \forall \,^nc^\mathcal {I}[{^nc^\mathcal {I}} \sqsubseteq {^n rdfs\!:\!Resource ^\mathcal {I}}] ~~~~~~~~~~~~~\mathrm {where}~ n \ge 1. \end{aligned}$$

(14)

We see that all individuals, which is expressed as $^0u^\mathcal {I}$ belong to $^0\mathbb {R}$, and all first classes, which is expressed as $^1u^\mathcal {I}$ belong to $^1\mathbb {R}$, and so forth. Using this extended rule (13), we see that the universe of discourse $\mathbb {R}$ stratifies by orders. Every entity in n-th order universe $^n\mathbb {R}$ is an instance of $(n+1)$-th order $^{n+1} rdfs\!:\!Resource ^\mathcal {I}$. Therefore, all extensions of $^n rdfs\!:\!Resource ^\mathcal {I}$ ($n\ge 1$) covers all entities in the universe and the union of $^n\mathbb {R}$ coincides with the universe of discourse $\mathbb {R}$.

Definition 8

(Universal Class and Stratified Universe).

(15)

We abbreviate this form to the following that is described in RDF Semantics.

Thus, $rdfs\!:\!Resource ^\mathcal {I}$ is appropriate to name universal class due to the extension being the universe of discourse $\mathbb {R}$.

3.5 Universal Metaclass in Higher Order Classes

As well as the universe of discourse $\mathbb {R}$, we set up the universal domain of classes in discourse, $\mathbb {C}$, in which all classes in the universe exist. Then, we can define for higher order classes,

(16)

Definition 9

(Universal Metaclass and Stratified Universe of Classes).

(17)

The RDF semantics shows the following condition. It is deemed to be an abbreviation of the universal metaclass (17),

While $rdfs\!:\!Class ^\mathcal {I}$ is appropriate to be called universal metaclass as a representative class for the universal domain of classes in discourse, we need to make clear the relation between $\mathbb {R}$ and $\mathbb {C}$ or $rdfs \!:\! Resource ^\mathcal {I}$ and $rdfs \!:\! Class ^\mathcal {I}$.

From stratified universe (13) and stratified universal domains of classes (16), we obtain the followings,

We distinguish $^n rdfs\!:\!Class ^\mathcal {I}$ and $^{n+1} rdfs\!:\!Class ^\mathcal {I}$ as well as we distinguish $^n rdfs\!:\!Resource ^\mathcal {I}$ and $^{n+1} rdfs\!:\!Resource ^\mathcal {I}$. Thus, we obtain the followings from (13) and (16),

Let us call these complex relations between rdfs:Resource and rdfs:Class hemi-cross subsumption, as these equations draw a picture like cross fire but $^n rdfs\!:\!Resource ^\mathcal {I} \not \sqsubseteq {^n rdfs\!:\!Class ^\mathcal {I}}$.

Thus, if we neglect the orders of classes, the membership loops appear on rdfs:Resource and rdfs:Class, but by seeing the orders, no membership loops exist in the universe.

4 Meta-Modeling Criteria in RDFS and OWL

As shown above, several principles about the order number of classes are addressed to avoid infinite membership loops. Here we set up them as criteria for meta-modeling.

• 1. (reducible) Every property that is applicable to individuals and the first order classes is applicable to much higher order classes.

• 2. (predicative) In respect of properties that make the relation of instance and class, i.e., rdf:type, owl:oneOf, rdfs:domain, rdfs:range, etc., the order of class must be plus one to the order of the instances.

• 3. (interpretable) In respect of properties that make the relation among non-literal objects, the order of arguments must be the same. Note that this principle is not applied to instance objects of Datatype such as strings, numbers, or URLs as datatype.

• 4. (constructive) Even if we adopt the predicative and the interpretable principles, ambiguous and undecidable entities on orders may still remain. Such a case, the orders must be decidable by ascendingly computing orders from individuals ($n=0$), and first classes ($n=1$), or descendingly computable starting at higher orders to lower orders so that the computation terminates at individuals level $(n=0)$.

In RDF-based OWL semantics, the class extension of OWL is defined as follows¹²,

We extend this definition to higher order classes as

(18)

Namely, all individuals $^0x^\mathcal {I}$ in OWL belong to $^0\mathbb {R}$ of the RDF universe, and all first classes $^1c^\mathcal {I}$ belong to $^1\mathbb {R}$ of the RDF universe, and so forth.

In the document of RDF-based OWL semantics, a special syntax form is used for sequence of entities, i.e., . In this paper, we express the sequence of entities simply $(x, y, \dots )$. So, owl:intersectionOf and owl:unionOf¹³ are extended to higher order classes as follows,

(19)

(20)

As well, the semantic conditions of enumeration is extended as

(21)

5 Related Work and Discussion

On Punning. W3C posed six use cases on “punning”¹⁴, but only the first and the second cases in these use cases deserve to discuss in ontological view.

The first case is solved by making $a\!:\!Service$ a meta-class.

$$\begin{aligned} \varvec{^2a\!:\!Service}~&\varvec{rdf\!:\!subClassO\!f}~\varvec{^2owl\!:\!Class}~.\\ {^2a\!:\!Service}~&rdf\!:\!type~{^3owl\!:\!Class}~.\\ ^1a\!:\!Person~&rdf\!:\!type~^2owl\!:\!Class~.\\ ^1s1~&rdf\!:\!type~^2a\!:\!Service~.\\ ^1s1~&a\!:\!input~^1a\!:\!Person~. \end{aligned}$$

The first triple shown above is newly added to the original set of the triples, so that the system becomes decidable and s1 becomes to be interpreted as the first order class rather than an individual because $n>1$ for $^n owl\!:\!Class$. The last triple must be modified to the form for domain s1 and range $a\!:\!Person$ constraints.

The second use case is a typical quiz for meta-classing. Harry as individual is a eagle, and the eagle as species is in the Red List as endangered species. In the following triples, the first and second triples are newly added to the others, so that they set up $a\!:\!Species$ and $a\!:\!EndangeredSpecies$ as meta-classes. Then, the case becomes decidable.

$$\begin{aligned} \varvec{^2a\!:\!Species}~&\varvec{rdfs\!:\!subClassO\!f}~\varvec{^2owl\!:\!Class}. \\ \varvec{^2a\!:\!EndangeredSpecies}~&\varvec{rdfs\!:\!subClassO\!f}~\varvec{^2a\!:\!Species}. \\ {^1a\!:\!Eagle}~&rdf\!:\!type~{^2owl\!:\!Class}. \\ {^0a\!:\!Harry}~&rdf\!:\!type~{^1a\!:\!Eagle}. \\ {^1a\!:\!Eagle}~&rdf\!:\!type~{^2a\!:\!Species}. \\ {^1a\!:\!Eagle}~&rdf\!:\!type~{^2a\!:\!EndangeredSpecies}. \end{aligned}$$

Domino-Tilting Puzzle. Motik posed Domino-tilting Puzzle to exemplify undecidable OWL Full (Motik 2007). In this example, GRID is an OWL class and does not interpreted as property. However, this model involves the infinite ascending higher order computation by the resulted stratified form such as $^n GRID ~\sqsubseteq ~\exists rdf\!:\!type .{^{n+1} GRID }$, starting from an individual GRID $a_{0,0}$ at the coordinate (0, 0), and going to $a_{\infty ,\infty }$. Then we have no way to terminate the computation.

6 Conclusion

We focused on set theories involved in RDF and RDF-based OWL Semantics, and clarified that stratified proper classes such as $^n rdfs\!:\!Resource$, $^n rdfs\!:\!Class$ ($^n owl\!:\!Thing$ and $^n owl\!:\!Class$ as well) do not include membership loops. Then we proposed a set of criteria for meta-modeling that is derived from Ramified Type Theory in Principia Mathematica. While it is obvious that unrestricted OWL Full may be undecidable, the proposed meta-modeling criteria is not enough to make meta-modeling computation decidable, even if we fulfill these criteria in meta-modeling as shown in Domino-tilting Puzzle. Let us call such ones unsound meta-modeling setup. We need further ways in well-mannered OWL Full meta-modeling so that the systems would be decidable with the computation of higher order classes.