In this paper we present a new labelled Natural Deduction calculus for the logic iALC, an intuitionistic description logic with nominals originally designed to reason over laws and other normative sentences in general. Even though this logic already has a formalised Sequent Calculus system, Natural Deduction is more adequate for extracting explanations for non-logicians - which is further aided by our use of labels as part of the calculus. We prove soundness and normalisation for the new Natural Deduction system, and show its completeness.
1. Introduction in Description Logics (DLs) that have a classical notion of validity, such as ALC and other canonical DLs. In the domain of law, this allows for the existence of a model representing two distinct legal systems, for instance, one in which the death penalty is not allowed and the other in which it is (referencing the same concept of death penalty). Representing law in a classical DL would force us to find a more conflated way to insert legal individuals into the logic at the risk of losing legibility and, even worse, soundness. In the example of death penalty, one would need a concept DeathPenaltyBrazil and another DeathPenaltyTexas as well as one or more formulas connecting both concepts in one manner or another (and would have to find another way to model VLSs, instead of directly having them being worlds in the model). By having this intuitionistic perception, we better translate the foundations of Private International Law into the modelling, connecting VLSs which are part of diferent legal systems via the same concept, for example, DeathPenalty , without having to resort to many workarounds. Legal precedence is, as well, something defined constructively in the logic through the VLSs, and does not need additional formulations in the model. In a regular (i.e. classical) DL, this cannot be represented as directly as in its intuitionistic counterpart when modelling laws since a Kripke model for a Classical Logic collapses all worlds (the legal individuals) to the same one, causing a contradiction by allowing and prohibiting the death penalty at the same time.
The logic iALC has been compared to other logical languages with respect to its adequacy for
representing normative systems. Comparison between iALC and diferent flavours of Deontic
Logics [
A Sequent Calculus (SC) for iALC was previously presented [
In this paper, we formally introduce the Natural Deduction system for iALC for the first time, bridging the gap between its informal presentation and the new calculus for iALC together with correctness results. It is our hope that the results contained in this paper will help fostering the utilisation of iALC not only as a language for the representation of the intended problems related to laws, but also to the implementation of tools for reasoning about those problems whilst retaining human-readability.
In the calculus, we introduce the use of labels as syntactic artefacts in order to represent
contexts to formulas of iALC. We assign labels in a similar fashion to [19], where the author
gives a labelled ND system for the classical sibling of iALC, ℒ. Labels represent contexts
for formulas in iALC, and allow for better concept manipulation. The use of labels was made
essential in [
The structure of the paper is as follows. In Section 2, we introduce the logic itself. In Section 3 we present the new Natural Deduction system for iALC, explaining the design choices we made. In Section 4 we show the normalisation, completeness and soundness proofs for the system. Finally, in Section 5, we conclude and discuss future work.
The logic iALC, first introduced in [ 20] and further developed in [
Let and be concepts, be an atomic concept, be an atomic role, be any formula and be a nominal. iALC formulas are described by the following grammar:
::= | : where the concepts ,
are given by the following grammar: ,
::= | ⊥ | ⊤ | ¬ | ⊓ | ⊔ | ⊑ | ∃. | ∀. where is an atomic concept. Formulas have a restricted use of nominals as nominal assertions are not concept constructors.
As given by the definition above, the main diference from the grammar of ALC is that, in iALC, ⊑ is a concept-forming operator, whereas in ℒ it is not, as defined and explained in [16]: Because iALC has an intuitionistic semantics, this entailment operator is analogous to the intuitionistic implication. This construction allows for an abstraction of the precedence relation ⪯ (a pre-order on worlds, as in the Kripke semantics for intuitionistic logics) in TBox reasoning, as well as allowing us to define negation using ⊑.
A constructive interpretation of iALC is a structure ℐ consisting of a non-empty set Δℐ of entities in which each entity represents a partially defined individual; a refinement pre-ordering ⪯ ℐ on Δℐ , i.e. a reflexive and transitive relation (a pre-order), and an interpretation function · ℐ mapping each role name to a binary relation ℐ ⊆ Δℐ × Δℐ and atomic concept to a set ℐ ⊆ Δℐ which is closed under refinement, i.e. ℐ ∈ ℐ and ℐ ⪯ ℐ ℐ implies ℐ ∈ ℐ .
The logic follows the semantics of IK, where the structures ℐ are models for iALC if they satisfy two frame conditions:
F1 if ⪯ ′ and then ∃′.′′ and ⪯ ′; and F2 if ⪯ ′ and then ∃′.′′ and ⪯ ′.
The interpretation ℐ is lifted from atomic concepts to arbitrary concepts as follows: ⊤ℐ = Δℐ ⊥ℐ = ∅ ( ⊓ )ℐ = ℐ ∩ ℐ ( ⊔ )ℐ = ℐ ∪ ℐ
(¬ )ℐ = { ∈ Δℐ | ∀, ⪯ ⇒ ̸∈ ℐ } (∀. )ℐ = { ∈ Δℐ | ∀( ⪯ ⇒ ∀((, ) ∈ ℐ ⇒ ∈ ℐ ))} (∃. )ℐ = { ∈ Δℐ | ∀( ⪯ ⇒ ∃((, ) ∈ ℐ ∧ ∈ ℐ ))} ( ⊑ )ℐ = { ∈ Δℐ | ∀, ( ⪯ ∧ ∈ ℐ ) ⇒ ∈ ℐ }
And the interpretation for formulas with nominals such as ( : )ℐ (where is any formula) is ℐ |=ℐ ℐ , where |=ℐ is the usual satisfaction relation of Kripke models.
The ND system we developed aims to reach TBox validity and it uses Gentzen-style proofs, based especially on [21]. Formulas are labelled in order to allow for the mixing of nominals and existential/universal restrictions in a TBox-only style of reasoning, even though role assertions belong in the ABox.
We expand the language with labels for our ND system, essentially giving context of universal and existential restrictions in formulas, as explained in Section 1. The grammar for iALC is then extended with:
As for labelled formulas, following [19], we first define an function to make a labelled ND system that translates from a non-labelled formula to a labelled formula as given below: ::= ::= ∃, | ∀, | ∅
( ) = ∅ (∀. ) = ( )∀ (∃. ) = ( )∃ ( ⊓ ) = ( ) ⊓ ( ) ( ⊔ ) = ( ) ⊔ ( )
(¬ ) = ¬ ( ) (
⊑ ) = ( ) ⊑ ( )
Given , the semantics for a labelled formula is given by ( )ℐ . This way, ∀3,∃2,∀1 , for example, has the same semantics as ∀1.∃2.∀3. .
[︁ ∃]︁ [︁ ∃]︁ ( ⊓ )∀ ⊓ − ( ⊓ )∀ ∀
⊓ − 1 ∃ ( ⊔ )∃ ⊔ − 1 : ∃, : (∃. ) ∃ − ⊥ ︀[ : ]︀ ( ⊔ )∃ ⊔ − 2
( ⊔ )∃ : (∃. ) : ∃, ∃ − : ∀, : (∀. ) ∀ − : (∀. ) : ∀, ∀ − ︀[ : 1]︀ : ( 1 ⊑ 2) ⊑ − : 1 : ( 1 ⊑ 2) : 2 ⊑ − : ⊥ : (¬ )¬ ¬ − : ( ⊓ )∀ : ∀ ⊓ − 1 : : (¬ )¬
: ⊥ : ( ⊓ )∀ : ∀ ⊥ − ⊓ − 2 : ∀ : ∀ : ( ⊓ )∀
⊓ − : ∃ : ( ⊔ )∃ ⊔ − 1 : ∃ : ( ⊔ )∃ ⊔ − 2
,∀
: : ,∀ : ( ⊔ )∃ [︁ : ∃]︁ [︁ : ∃]︁ . . . .
⊔ −
: ⊥ : (∃. )1 : ∀.( 1 ⊑ 2) : (∃. )2 − ∃ for each rule are given over the bar and its (single) conclusion lies below. Assumptions in the premises are enclosed by square brackets. The proofs in ND have a tree-like form, by connecting together the deduction steps given by the applied rules in the proof. Some of the rules have formulas surrounded by brackets, indicating that the rule in question can discharge these hypotheses, i.e. the conclusion of the proof does not depend on them explicitly anymore.
Let and be concepts, and be nominals, be a formula, and be a role. represents a (possibly empty) list of labels. Labels represent universal or existential restrictions on concepts, made implicit by the introduction rules - the associated elimination rules make them explicit. We denote by ∀ a list that has only universal restrictions, and by ∃ a list with existential restrictions only. ¬ swaps existential and universal restrictions throughout .
Rules ∃ − , ∃ − , ∀ − and ∀ − require that there be an assertion in order to function.
These rules are what allows our calculus to use the labels as restrictions. Even though this is a
TBox-centered calculus, we assume that there is a subjacent ABox extension that introduces
these role assertions. In [
Rules and stand for the principle of explosion. The structural rules and deal with modal necessitation. Rule − ∃ allows for context permutation within a subsumption.
Some rules have two versions, one without nominals and one with nominals (notated with a subscript in the name). For instance, we have ⊓ − and ⊓ − .
From now on, every rule that has a version with nominals (i.e. has a subscript ) will have only this version being used, as the other version is trivial in the correctness proofs given in the next section. As such, they will only be called by their original name, without the , in order to avoid visual clutter. For instance, ⊓ − will be referred to as ⊓ − .
In this section we show that important properties which are expected of ND systems hold in the one here proposed for iALC. Due to limited size and redundancy in arguments, some proofs are sketched and inductive cases may be omitted - mainly the ones involving operators analogue to propositional ones, since those are very similar in functionality. Full proofs can be found in https://github.com/Bpalkmim/iALC_ND_proofs. In order to improve readability, lists of labels are omitted whenever possible throughout Section 4.1, as they do not interfere with the process of normalisation. When dealing with soundness and completeness in Sections 4.2 and 4.3, however, labels will be explicitly shown.
Our main focus here is to show that these properties still hold when dealing with labels and the rules which introduce and eliminate existential and universal restrictions.
Normalisation is a crucial step to show that the sub-formula principle holds in our system. This principle states thatevery step in a proof contains only sub-formulas of either the conclusion or the premises. This is extremely important to order to do proof search in an eficient way. We will base our normalisation proof on the ones presented in [21, 22, 23, 24]. We will utilise the words proof and derivation interchangeably from now on (one can see a proof in ND as a derivation from the premises to the conclusion).
To reach normalisation, the following definitions are needed.
Definition 1 (Major premise). The major premise is the premise of an elimination rule which contains the operator to be eliminated. Other premises, if existent, are called minor premises. Definition 2 (Detour). A detour occurs when a formula is introduced via an introduction rule only to be eliminated immediately later as the major premise of an elimination rule.
Our goal in the end will be to remove such detours via reductions and arrive at so called normal proofs, to show that the system has normalisation.
Example 1 (A detour with ⊓). Let Π1 and Π2 be sub-proofs. An example of a detour is given below, where the list of labels is empty: Π1 Π2 : : : ( ⊓ ) ⊓ −
: ⊓ − 1
By introducing and eliminating a conjunction, : occurs twice in the same branch of the proof. This is clearly an unnecessary step, as no progress is made in the proof.
Maximum formulas are precisely those that represent a detour. Its definition is given next. Definition 3 (Maximum Formula). A formula in a derivation Π is a maximum formula if: 1. is the conclusion of an application of an introduction rule and the major premise of an application of an elimination rule of the same operator; or 2. is the conclusion of an application of ⊔ − as well as the major premise of an application of an elimination rule.
The second case covers a hidden detours in the ⊔ − . An example will be shown later.
In order to evaluate how a reduction works in simplifying a proof, it is necessary to have some kind of measure. We then introduce the concept of degree of a formula, indicating its size by the number of occurrences of logical operators. Not surprisingly, the name maximum formula is related to this measurement.
Definition 4 (Degree of a Formula). The degree of a formula is given as follows: () = 0, for an atomic concept C ( : ) = ( ) + 2 ( ⊔ ) = ( ) + ( ) + 1 ( ⊓ ) = ( ) + ( ) + 1 ( ⊑ ) = ( ) + ( ) + 1 (¬ ) = ( ) + 1 (∃. ) = ( ) + 2 (∀. ) = ( ) + 2 Definition 5 (Degree of a Derivation). The degree of a derivation Π is defined as: (Π) = {( ) : is a maximum formula in Π} Definition 6 (Normal Derivation). A derivation Π is called normal when (Π) = 0.
In other words, a normal derivation has a maximum formula of degree 0, i.e. has no detours. Definition 7 (Critical Derivation). A derivation Π is called critical when 1. Π ends with an application of an elimination rule ; 2. the major premise of is a maximum formula; 3. (Π) = ( ); and 4. for all Π′ sub-derivation of Π, (Π′) < ( ) = (Π).
This way we know that the main detour to be reduced lies (at first) in .
A reduction is an operation on proofs that functions as a way to remove maximum formulas locally. The reductions for the propositionally-based operators are extensions of the usual Prawitz-reductions. As such, we have a permutation operation in order to arrange a ⊔-maximum formula to be properly reduced. This will be shown after the more basic cases. Definition 8 (Reduction). We say a derivation Π reduces to another, Π′, when we apply zero or more reductions to maximum formulas of Π and it becomes equal to Π′. We denote by Π ◁ Π′ the reduction from Π to Π′.
As a quick note on reductions, they usually end up copying whole sections of proofs (thus increasing the size of the proof itself), but they do not increase the complexity of the formulas therein. First we will show some basic cases. ⊓-reduction Taking the derivation from Example 1, we have: Π1 Π2 : : : ( ⊓ ) ⊓ − : ⊓ − 1 Π3 ◁ Π1 : Π3
This way the proof goes directly through : , without introducing and eliminating an unused operator. The reduction utilises ⊓ − 1, but ⊓ − 2 is analogous. ⊑-reduction This derivation has a maximum formula whose main operator is ⊑: Π1 : [ : ] Π2 : : ( ⊑ ) ⊑ − : ⊑ − Π3 ◁ Π1 : Π2 : Π3
Note that, in this case, there can be multiple occurrences of the hypothesis discharge over Π2, so this reduction ends up copying the entirety of Π1 possibly many times, increasing the size of the proof itself, but not its complexity, since the maximum formula was removed.
The case of ¬-reduction via ¬ − and ⊥ − (which acts as ¬ − ) is analogous, as negation is but a special case of ⊑.
As always, we assume that is in the ABox. ∀-reduction The case for the universal restriction on concepts is rather simple. Let be a role.
Π1 : ∀ : ∀. ∀ − : ∀ ∀ − Π2 : ∀ Π1 Π2
The case for ∃-reduction is the analogous.
Only the one involving ⊔ − 1 will be shown. ⊔-reduction This operator, much like ⊓, has two possible reductions, but both are equivalent. Π1 : : ⊔ ⊔ − 1 [ : ] [ : ] Π2 Π4
As was the case with ⊑, there can be multiple copies of Π1 to be added. can be the major premise of another elimination rule. Let us, then, define a ⊔-permutation This operator has a peculiarity in that it may hide a maximum formula, since that allows for a rearrangement of the proof tree around the ⊔ − . Here we will only show the case of ⊔ − 1, without loss of generality. Let be an elimination rule with major premise 1, minor premise 2 and conclusion 3. Due to limited space, we assume that has only one ⊔-permutation minor premise; with more premises the argument is analogous.
Π1 : : ⊔ ⊔ − 1 1 [ : ][ : ] Π2 1 Π3 1 3 Π5
With this derivation in hand, the detour that may happen with becomes apparent, since is an elimination rule and there may be other detours to be reduced in the sub-derivations. It is important to note that this permutation does not increase the degree of the derivation, since the maximum formula, be it : ⊔ or any of the ’s, does not increase in complexity.
In order to optimise space, from here on we will refer to simple derivations utilising the following notation: Π/ represents a derivation Π with as a conclusion. Conversely, / Π represents a derivation Π with as a premise. Note that there may be more copies of in the actual derivation Π, as stated previously.
Lemma 1. Let Π1/ and / Π2 be two derivations in the ND system such that (Π1) = 1 and (Π2) = 2. Then, (Π1/[ ]/Π2) = {( ), 1, 2}.
Proof. Directly from Definition 5: the maximum formula in this derivation is either in Π1, in Π2 or is itself.
Lemma 2. If Π reduces to Π′, then (Π′) ≤ (Π).
Proof. It follows directly from the reductions in Definition 8 and the degree of a formula in Definition 4: Since a reduction always lowers the degree of a maximum formula, it also lowers the degree of the derivation in which it is contained (as per Definition 5).
Lemma 3. Let be a formula in iALC, Γ be a set of formulas, Δ ⊆ Γ and Π be a critical derivation of Γ ⊢ . Then, Π reduces to a derivation Π′ of Δ ⊢ such that (Π′) < (Π). Proof. The proof follows by induction on the structure of Π. We will use the reductions shown in Definition 8, but assuming they are critical derivations. We will call each derivation before a reduction Π, and Π′ after the reduction.
Lemma 4. Let be a formula in iALC, Γ be a set of formulas, Δ ⊆ Γ and Π be a derivation of Γ ⊢ such that (Π) > 0. Then, Π reduces to a derivation Π′ of Δ ⊢ such that (Π′) < (Π).
Proof. It follows directly from Lemmas 2 and 3 using induction on the length of Π. Theorem 1 (Normalisation). Let Π be a derivation of Γ ⊢ . Then, Π reduces to a normal derivation Π′ of Δ ⊆ Γ ⊢ .
Proof. This follows directly from Lemma 4 by applying the reductions (and the permutation when necessary) inductively over the degree of Π in order to remove its maximum formulas. In the end, the proof generated will be normal. Moreover, since it is done inductively, the normalisation process is terminating.
Theorem 2 (Soundness). Let be a formula in iALC and Γ a set of formulas. Then, Γ ⊢ implies Γ |= .
Proof. The proof follows by showing that each rule preserves soundness. For rules that involve hypothesis discharge, we use induction on the length of derivations.
Theorem 3 (Completeness). Let be a formula in iALC and Γ a set of formulas. Then, Γ |= implies Γ ⊢ .
Proof. We prove completeness in regards to TBox reasoning. In [
(MP) If and ⊑ are theorems, then is a theorem too.
In [25], the authors prove that this system is sound and complete for TBox validity. So, in order to prove completeness of our ND system, all we have to do is prove each of these axioms. Axiom (IPL) is easily proven since all substitution instances of IPL theorems can be proven in our ND system using only propositional rules. (MP) is covered by our ⊑ − rule, and (Nec), by the rule. We, then, only have to prove the remaining five axioms. Full proofs can be found in https://github.com/Bpalkmim/iALC_ND_proofs.
In this paper we presented a Natural Deduction system for the intuitionistic description logic iALC, originally tailored to deal with norms, especially in a legal context. Although iALC had a Sequent Calculus (SC) system formalised, it was not widely used due to the interdisciplinary characteristic of the application of this logic, which favoured a more readable style of making proofs - Natural Deduction (ND).
The ND system is sound and complete and its normalisation is terminating. The proofs for those properties closely follow the ones presented previously for the SC system, with roots on the ND system designed for classical ℒ, so they share many similarities.
With the formalisation of this system, we intend to further apply iALC to contexts involving law and norms, and expand its usage to diferent areas, now with a more approachable style of showing proofs for non-logicians.
A version of this system without nominals would be PSPACE-complete. We believe that he labelled ND system for iALC with nominals has 2-EXPTIME-hard complexity. We intend to formally establish this using the same techniques given in [17, 26], which were used for the SC system for iALC. Establishing complexity is a future work.
We intend, in the future, to implement these proofs in an interactive theorem prover such as Coq and plan to create an automated theorem prover for iALC. In the theoretical side, we aim to increment iALC with some kind of non-monotonic reasoning, which will most likely be related to default logic.
The first author is financially funded by CNPq (process number 141290/2019-6).