Leśniewski's ontology LO is an expressive calculus of names. It provides a basis for mereology but allows also for direct formalisation of reasoning in natural languages. Recently its elementary part was characterised by means of the cut-free sequent calculus GO. In this paper we investigate its extended version ELO which introduces lambda terms to represent complex descriptive names. The hierarchy of three systems is formalised in terms of sequent calculi which satisfy cut elimination and the subformula property.
Despite of the great success of standard first-order languages and their priviliged role in automated deduction, it is often difficult to apply them in a direct and satisfactory way to formalisation of natural languages. The following two features of natural languages are usually discussed in this context: 1) the subject-predicate structure of atomic sentences, characteristic not only for traditional logic but also for modern linguistics with its NP+VP model of sentences applied in generative grammar; 2) the wide class of naming expressions which are used not only to refer to x, but also to convey information about x, and even if they refer to something it is not necessarily the singular reference.
No wonder that several approaches alternative to FOL (first-order logic) were proposed, attempting to obtain a formalisation of arguments in natural languages which is closer to their original structure. One may mention here for example, the calculi of names due to Sommers [25], the variety of relational sylogistics of Moss and Pratt-Hartmann [21], or the logic QUARC of Ben-Yami [2]. Even in the approaches based on the standard first-order languages one may find several proposals related to the second feature of natural languages. Thus the notion of name was extended to non-referring terms in free logics, or the logic of intentional objects of Paśniczek [20], and even to general names (plural reference) in the plural logic of Oliver and Smiley [19]. Not surprisingly, in these approaches a lot of work was devoted to the development of theories of complex names conveying information, like definite descriptions.
One of the oldest approaches of this kind is the calculus of names called Leśniewski's ontology (LO) (see e.g. [24], [15] or [26]). It satisfies both features mentioned above: the subject-predicate structure of atomic sentences and a wide understanding of names, including empty and general names (like 'Pegasus' or 'an emperor'). LO in the original form was introduced as a formal basis for developing another, better known theory of Leśniewski -mereology [17]. Thus LO was introduced as an alternative to Frege's construction of logic, while mereology was introduced as an alternative to set theory. LO is a theory of the binary predicate ε understood as the formalisation of the Greek 'esti', hence formulae of the form sεt express sentences '(the) s is (a/the) t', and their truth conditions are expressed by means of Leśniewski's axiom LA: ∀xy(xεy ↔ ∃z(zεx) ∧ ∀z(zεx → zεy) ∧ ∀zv(zεx ∧ vεx → zεv))
It roughly says that xεy holds iff x exists, is y, and is unique. The weak form of LO, called elementary LO (cf. [24]), may be formalised as an extension of an arbitrary axiomatic system for first-order logic (FOL) with added LA. Of course one has to remember that, in spite of the name 'elementary', and the fact that we refer to FOL as the basis, elementary LO is not an elementary theory in the standard sense, since name variables represent also empty and general names. Accordingly, quantifiers have no existential import; this role is taken up by ε.
Recently the elementary LO and its extension with the variety of predicates obtained wellbehaved proof-theoretic characterisation in terms of sequent calculi GO and GOP [10]. But there is a problem, at least from the proof-theoretic standpoint, with formalising complex names in LO. We have briefly discussed in [10] the original approach of Leśniewski to the problem and its deficiences. As a result of these problems both GO and GOP were restricted to simple terms only. However, the advantages of having formal tools for dealing with complex names, like definite descriptions, were recognised in many fields, including: proof theory [11,14,13], query answering, [3], knowledge representation [1], and many other.
In this paper we focus on the problem of dealing with complex names in LO. To this aim we introduce extended LO (ELO), with lambda terms applied to represent descriptive names. The main idea is to keep two essential features of LO: the subject-predicate structure and the wide notion of name. However, to represent descriptive terms we admit also the application of relational atoms from FOL, in particular inside lambda-terms. Some way of mixing LO with FOL was already considered by Waragai [27] but he introduced special operators for this aim, similarly like Słupecki [24]. The present approach is simpler in the sense that, except the lambda operator, no extra machinery is needed.
Three versions of ELO are considered, differring in the strength of involvement of complex terms in atomic sentences, and characterised by means of sequent calculi which are cut-free and analytic. In section 2 we describe the language and axioms of three variants of ELO, then we focus on the problem of constructing for them well-behaved sequent calculi called GELO. Before proving their adequacy we focus on the characterisation of identity which provides a necessary prerequisite for further formal development. Section 5 presents the adequacy of all variants of GELO and section 6 provides a constructive proof of cut elimination. We close the paper with a few remarks on open problems and possible further developments.
The set of logical constants of the language of all variants of ELO consists of connectives (¬, ∧, ∨, →, ↔), quantifiers (∀, ∃), two special binary predicates (ε, ≡) and lambda operator λ. We assume a denumerable set of n-ary relational predicate variables R n , n > 1 and name variables divided into bound: x, y, z, ... (possibly with subscripts), and free: a, b, c, ... (also called parameters). Arbitrary terms are denoted as t, s, u (possibly with subscripts), formulae as ϕ, ψ, χ, their finite multisets as Γ, ∆, Π, Σ. ϕ[s/t] denotes the result of correct substitution of t for all occurrences of s.
The notion of a term and formula is defined by simultaneous recursion. Terms are simple, i.e. name variables, and complex, i.e. lambda terms of the form λxϕ, where ϕ is a formula. The set of formulae is the set of atoms closed under quantification of name variables and boolean combinations of formulae. What is specific is that there are three kinds of atoms: relational atoms Rt 1 ...t n , where all arguments are simple terms, i.e. variables, identities t 1 ≡ t 2 , where both arguments can be simple or complex, and ε-atoms t 1 εt 2 . Similarly as in [10] we apply for simplicity the convention of omitting ε, thus writing st instead of sεt; it has a deeper sense connected with counting the complexity of terms and formulae. Roughly, the complexity of any term or formula (c(t), c(ϕ)) is the number of occurrences of logical constants, except ε. Thus the complexity of relational atoms, as well as of ab is 0, whereas c(a ≡ b) = 1. However, in general for ε-atoms and identities we have c(st) = c(s) + c(t) and c(s
We consider the hierarchy of three languages: weak, medium and strong, depending on what kind of terms are admitted as arguments of ε-atoms t 1 εt 2 :
1. L w : t 1 simple, t 2 arbitrary; 2. L m : additionally ε-atoms with both arguments complex; 3. L s : additionally ε-atoms with t 1 complex and t 2 simple. So only L s admits all possible combinations of terms, as in identities. Note that in the setting of ELO, the axiom LA covers in fact four schemata:
They form a hierarchy of the commitment of complex terms in forming atoms of ELO, representing different strength of expression. Moreover, in the sequent system, they will be dealt with different kinds of rules. Accordingly, we will be talking about three variants of ELO formalised in respective languages:
However, even ELO s is in a sense too weak for real applications to the analysis of reasoning in natural languages. For example, we are not able to demonstrate the validity of such simple argument as 'Ann is the oldest daughter of Betty. Therefore, she is Betty's daughter. ' It may be formalised as aλx(Dab ∧ ∀y(Dyb → Oay)) / aλxDab but to derive the conclusion we need some ways of unfolding the content of lambda term. To resolve this problem we introduce a kind of β-conversion (BC) of the form:
where aa is added to restrict a to individual names. Similar principles were considered by Waragai [27] and Słupecki [24] for their special operators for making complex terms.
Finally, mainly for technical reasons, we introduce as the primitive notion the predicate of strong identity ≡ axiomatised by the following equivalence SI:
Summing up, we assume that in each variant of ELO we have BC and SI as axioms added to FOL, and suitable forms of LA, namely:
All variants of ELO will be characterised in terms of sequent calculi called GELO. First we introduce the auxiliary calculus GOI which is the subsystem of the modular extension of GO called GOP (GO with predicates) from [10]. It consists of the rules defined on sequents Γ ⇒ ∆ and specified in Fig. 1. Formulae displayed in the schemata are active, the remaining ones are parametric, or form a context. In particular, all active formulae in the premisses are called side formulae, and the one in the conclusion is the principal formula of this rule application. Proofs are finite trees with nodes labelled by sequents. The height of a proof D of Γ ⇒ ∆ is defined as the number of nodes of the longest branch in D. ⊢ k Γ ⇒ ∆ means that Γ ⇒ ∆ has a proof of the height at most k. In general, when presenting proofs, we omit structural rules to save space. Incidentally we use underlining for side formulae and bold type letters for principal formulae of some steps to facilitate reading of proofs.
GOI is cut-free, satisfies the interpolation theorem and LA 1 (the essential rules are (R), (T ), (S), (E); see [10,12]). We assume for further investigations that GOI is the core calculus for obtaining three variants of GELO in their respective languages. But GOI, even if formulated in any of the languages L w , L m , L s , i.e. with added relational atoms and lambda terms, is too weak to obtain any specific results related to complex terms. Moreover, with quantifier rules (∀ ⇒), (⇒ ∃) admitting only parameters as instantiated terms it is incomplete. We could admit arbitrary term t instead of parameter b in these rules, like we did for (≡⇒), (⇒≡) which were also formulated for parameters only in [10], but it destroys the subformula property. Fortunatelly, much better solution is possible.
To obtain GELO w we have to add to GOI (in L w ) the rules from Fig. 2. The most direct way to obtain the system capable of proving LA 2 is to strengthen the rules (R), (T ), (S), (E)
where a is a fresh parameter (eigenvariable), not present in Γ, ∆ and ϕ, whereas b, c, d are arbitrary parameters, t, s are arbitrary terms.
where a is a fresh parameter (eigenvariable), b, c are arbitrary parameters, t ∈ term(Γ ∪ ∆) [the set of complex terms of Γ ∪ ∆] in (≡⇒ E), and ϕ in (⇒≡ E) is a relational atom.
The rules for GELO w in the sense of admitting atoms of the form bλxϕ. The identical proofs as those provided in [10] would do the job. But the most direct does not mean the best. If any of (R), (T ), (S), (E) admits ε-atoms bλxϕ it is possible that cut formula of this form is introduced in the left premiss of (Cut) by (⇒ β) and in the right premiss by any of (R), (T ), (S), (E). In such situation it is not possible to eliminate cut. It is worth emphasizing the important fact: we don't need to modify (R), (T ), (S), (E) to obtain LA 2 ; the rules which apparently characterise only LA 1 are sufficient for this aim (it will be shown in section 5), and it is crucial for proving cut elimination in section 6.
(⇒ β) and (β ⇒) adequately characterise our principle BC. Two sequents giving by (⇒↔) the effect of BC are easily provable; on the other hand, two β-rules are easily derivable if such sequents are used as additional axioms.
(≡⇒ E) is not much related to the characterisation of ≡ since it is adequately expressed by (⇒≡), (≡⇒), which may be shown in a similar way as in the case of BC versus (⇒ β), (β ⇒). This rule rather uses ≡ as a vehicle for introducing new parameters representing complex terms. It makes possible to use in our calculi (∀ ⇒), (⇒ ∃) restricted to arbitrary b instead of t, in the way we already exploited for free logics [7] and the Russelian theory of descriptions [11]. As a result, these restricted quantifier rules are sufficiently strong to obtain everything which is provable by means of unrestricted rules admitting arbitrary terms as instances of variables. Formally it may be shown by proving derivability of stronger variants. Here is the case of unrestricted (∀ ⇒):
where the left top sequent is a provable instance of Leibniz Law LL (see section 4). In a similar way we prove derivability of unrestricted (⇒ ∃). On the other hand, (≡⇒ E) is easily derivable in the calculus with unrestricted (⇒ ∃):
Since (⇒≡), (≡⇒) deal only with ε-atoms, (⇒≡ E) is added to extend the applicability of ≡ to relational atoms. In the effect we get a calculus where ≡ can express Leibniz law (LL) in the unrestricted way. There are several possible rules to obtain this effect (see [8]) and one may think that, for instance, the popular solution due to Negri and von Plato [18] would be more convenient. However, with other kind of rules we face the same problem of the failure of cut elimination as indicated above, in the context of discussion on modified (R), (T ), (S), (E) versus (⇒ β). To avoid such problems and to allow one to prove cut elimination, this form of the extra rule for ≡ is optimal.
To obtain GELO m we add the rules from Fig. 3 to GELO w formulated in L m . These rules are similar to the rules introduced in [13] to characterise the Russellian theory of definite descriptions with lambda terms. LA is very similar to the Russellian schema of elimination for descriptions, hence this solution works here as well. Eventually to obtain GELO s we change the language for L s and relax the proviso concerning t in rules from Fig. 3: t may be an arbitrary term.
Summing up the calculi for three versions of ELO are constructed as follows:
• GELO w is obtained by addition of the rules from Fig. 2 to GOI in L w ;
• GELO m is obtained by addition of the rules from Fig. 3 to GELO w in L m ;
where a, b are new parameters (eigenvariable), c, d are arbitrary, t is complex. • GELO s is obtained by relaxing the condition on t in rules from Fig. 3 in L s .
We finish this section with an example of a cut-free proof of the sequent which will be useful in further considerations:
Before we show the adequacy of our calculi we need to prove some properties of ≡, in particular the provability of the full form of LL (Leibniz Law).
The following sequents are cut-free provable in all variants of GELO for arbitrary s, t, u: where the rightmost sequent is provable in symmetric way. Case 4: For s ≡ t, u ≡ s ⇒ u ≡ t the proof is similar. Cases 5 and 6 are provable in the same way as 3 and 4, since the only difference is that the respective applications of (≡⇒) to t ≡ s give at, as instead of as, at in premisses and the order does not matter. Now we are in the position to prove that LL holds for all variants of GELO.
Proof. The proof is by induction on the complexity of ϕ. In the basis we must show that it holds for ϕ atomic. Since, the previous lemma guarantees the result for identities, and (⇒≡ E) for relational atoms, it remains to show that the following cases hold: where sequent s ≡ t, as ⇒ at is the case 1, already proven, and s ≡ t, at ⇒ as is the case 3, which is provable exactly as case 1, according to the observation made by the end of the proof of lemma 2. The same applies to case 4 which is proved in the same way as case 2.
The induction step for non-atomic cases is provable as in FOL.
Proof. We need to demonstrate the same cases as in the previous lemma but now for atoms which have complex terms as both arguments. Case 1 with all terms complex:
where sequent s ≡ t, as ⇒ at is the case 1 of the previous lemma. Case 2. This time what matters is the character of s and t with u fixed complex. Since the case of s, t both simple was proven in the preceding lemma, there are three subcases:
2.1. all terms complex: where ba, as ⇒ bs is a generalised transitivity cut-free provable by lemma 1.
Proving LL for GELO s , i.e. for the cases λxϕb, is in some cases identical and in some other simpler than in the previous lemma, hence we omit the proof.
To show that all variants of GELO adequately characterise respective forms of ELO we demonstrate that different variants of LA are provable and that these rules are derivable if we use respective forms of LA as additional axioms. LA 1 was proved in [10] by means of the rules (R), (S), (T ), (E), which were in turn shown derivable in the presence of LA 1 . These proofs are correct in GELO w so we only need to prove LA 2 :
yield together by (⇒ ∧) and (⇒→) the left-right implication of LA 2 . The other part is proved as follows:
where D is:
As we already noticed it is quite an interesting fact that all that is needed to prove this axiom beyond rules from Fig. 1 (which were sufficient for proving LA 1 ) are the rules for ≡; even the rules for β-conversion are not required.
The adequacy of GELO m (and GELO s too, as the only differences concern the character of t) follows from the next two lemmata: Lemma 6. The rules of Fig. 3 are derivable by means of the rules from Fig. 1 and LA 3 used as an additional axiomatic sequent.
Proof. For (λ ⇒ 1):
where S is λxϕt ⇒ ∀xy(xλxϕ ∧ yλxϕ → xy) which is derivable from LA 3 . For (⇒ λ) first we prove:
where the rightmost sequent is proved by lemma 1 (in case of LA 4 the application of (T ) is enough).
Eventually by two cuts with the premisses of (⇒ λ) we obtain ∀xy(xλxϕ ∧ yλxϕ → xy), Γ ⇒ ∆, ∀x(xλxϕ → xt). Since from the leftmost and the rightmost premiss of (⇒ λ) we can derive Γ ⇒ ∆, ∃x(xλxϕ) and Γ ⇒ ∆, ∀xy ( where the rightmost sequent is proved as follows:
Together, these two lemmata guarantee the adequacy of GELO m . For GELO s the proof of the counterpart of lemma 6 is the same, and in the proof of the counterpart of lemma 7 only the last part (see the proof-tree above) requires more involved work: where the rightmost leaf is provable as an instance of LL, and D is:
where the leftmost leaf again is a provable instance of LL.
Lemma 9.
1. The rules (⇒ β) with (β ⇒) are reductive in general; 2. Both (⇒ λ) with (λ ⇒ 1), and (⇒ λ) with (λ ⇒ 2) are reductive in GELO m .
Proof. The two rules of β-conversion are trivially reductive. It remains to show that the three rules for λ are reductive in GELO m .
Let the right premiss of cut with the principal formula λxϕλyψ be derived by (⇒ λ). In case the right premiss is derived by (λ ⇒ 1) we apply lemma 8 to its premiss to substitute the occurrences of fresh a with c, then we continue:
Both cuts are of lower degree, hence both rules are reductive.
If the right premiss is derived by (λ ⇒ 2) we apply lemma 8 to the rightmost premiss of the application of (⇒ λ) instead, to substitute the occurrences of fresh a, b with c, d respectively, then we continue:
Since all cuts are of lower degree, we are done.
Combining lemma 9 with the results proved in [10] we obtain the cut elimination theorem for two of the considered systems: Theorem 1. Every proof in GELO w and GELO m can be transformed into a cut-free proof.
What with GELO s ? Note that in GELO s cut may be performed also on the formulae of the form λxϕb by means of (⇒ λ) and (λ ⇒ 1), or (⇒ λ) and (λ ⇒ 2). In such cases we are not guaranteed that the transformed proofs contain cuts on formulae of lower degree. However, note that the transformations displayed above in each case replace cuts on formulae of the form λxϕb with cuts performed only on formulae of the form bλxϕ. It follows: Lemma 10. Every proof in GELO s can be transformed into a proof with no cuts on formulae of the form λxϕb.
Since such proofs may be dealt with as proofs in GELO w or GELO m , we obtain: Theorem 2. Every proof in GELO s can be transformed into a cut-free proof.
And as the consequence of these theorems we obtain: Corollary 1. If ⊢ Γ ⇒ ∆ in GELO w , GELO m or GELO s , then it is provable in a proof which is closed under subformulae of Γ ∪ ∆ and atomic formulae with possibly new parameters.
ELO, similarly to LO, is not characterised semantically here. In fact, there are known controversies concerning the proper interpretation of quantifiers for LO (cf. [16,22]), and for the time being we prefer to avoid these issues, since our aim is to provide a proof-theoretic analysis. However, note that referring to model-theoretic semantics is not the only option. Girard [6] emphasized that a cut-free system with the subformula property is complete in an internal sense. The idea of proof-theoretic semantics (see e.g. [23]) also shows that we can locate meaning in the well-defined rules. It seems that GELO satisfies these requirements sufficiently well. To strengthen this view it would be welcome to prove also the interpolation theorem for GELO, following the lines of proof of this result for GO and GOP in [12]. It is an open problem.
It was noticed in [10] that we can relatively easy obtain the intuitionistic version of GO (called GIO there) by restricting the sequents to single-succedent and changing slightly some of the rules. One may easily modify in this way also GOP from [10] and all variants of GELO introduced in this paper. The crucial point is to replace the present rule (≡⇒) with two variants (with ∆ empty):
Γ⇒ ∆, bt bt, bs, Γ⇒ ∆ t ≡ s, Γ⇒ ∆ (≡⇒ 2) Γ⇒ ∆, bs bt, bs, Γ⇒ ∆ t ≡ s, Γ⇒ ∆
It may be easily checked that all proofs we needed to establish adequacy and cut elimination, hold also in the intuitionistic versions, since, even in the places where (≡⇒) is applied, there is only one active formula in the succedent. This way we obtain for free also intuitionistic companions of considered calculi. Again, it must be emphasized that, similarly as in the case of 'classical' variants, the background logic is only apparently intuitionistic, since the terms are not restricted to individual ones, and the quantifiers have no existential import.
Because of the lack of space we were not concerned with the problem of expressivity of ELO. To simplify things we considered the calculus as built on the combination of the language of LO with simple language of pure FOL. However, it is possible to modify LO by admitting richer or different languages as the additional component. For example, even if we keep the first-order language, we may admit arbitrary terms as arguments of relational atoms. Or we may use a totally different language, like the languages of description logics, of QUARC, or of relational syllogistics. Of course, in case of mixing LO with other kinds of languages, it may be necessary to extend also the set of rules to cover specific logics different than FOL. Alternatively, we can consider a different approach to extending LO keeping the language of LO as the outer language and restricting the application of the other as the inner language admitted only inside complex terms. Again, because of the additional complications connected with more complex grammar we did not consider such an approach in this short paper. However, it is another promising field for further exploration.
Together with [10] this paper is meant as a theoretical foundation necessary for developing the novel tools in the field of automated deduction. Close resemblance of the structure of ELO to the structure of natural languages may help in the preparation of provers and proof assistants allowing for more direct and efficient processing of the reasoning tasks in natural languages. It is going to be one of the next steps in future research.
Before we focus on the proof of the cut elimination theorem let us note that for all variants of GELO the following result holds:
Proof. By induction on the height of a proof. The rules (E), (⇒≡), (≡⇒ E), (λ ⇒ 1), (⇒ λ) may require similar relettering like (∃ ⇒) and (⇒ ∀). Note that the proof provides the heightpreserving admissibility of substitution and that it is restricted to substitution of parameters for parameters only.
Let us assume that all proofs are regular in the sense that every parameter a which is fresh by side condition on the respective rule must be fresh in the entire proof, not only on the branch where the application of this rule takes place. There is no loss of generality since every proof may be systematically transformed into a regular one by the substitution lemma.
In [10] the cut elimination theorem was proved for GO and for GOP which covers GOI as its subsystem. Due to the construction of the rules from Fig. 2 and 3, this proof may be extended to GELO w and GELO m . It is enough to show that new rules are reductive in the sense of Ciabattoni [5]. Roughly: a pair of introduction rules (⇒ ⋆), (⋆ ⇒) for a constant ⋆ is reductive if an application of cut on cut formulae introduced by these rules may be replaced by the series of cuts made on less complex formulae, in particular on their subformulae. This feature of rules enables the reduction of the cut-degree in the proof of cut elimination. The latter notion, and the notion of proof-degree, is defined as follows:
1. The cut-degree dϕ is the complexity of the cut-formula ϕ, i.e. the number of connectives, quantifiers and lambda operators occurring in ϕ. 2. The proof-degree (dD) is the maximal cut-degree in D.
The reductivity of rules is sufficient for our aim on condition that no other rule in the system introduces the principal formula of such rules as active. It was the main reason for restricting (R), (S), (T ), (E) to atoms with simple terms as both arguments and for introducing the new rules for atoms with complex terms, as we explained in section 3. The separation of rules for different cases is the key to avoid the problems with elimination of cuts. Note that:
1. if st is strictly atomic, i.e. containing parameters only, it can be principal only in the antecedent of the right premiss of cut, due to (R), (S), (T ), (E); 2. if it is of the form bλxϕ, it can be principal in both premisses of cut but only via (⇒ β) and (β ⇒); 3. if it is of the form λxϕt, it can be principal in both premisses of cut but only via (⇒ λ) and (λ ⇒ 1) or (λ ⇒ 2); 4. identity is principal in both premisses of cut only via (⇒≡) and (≡⇒); 5. relational atom is principal only in the succedent of the left premiss via (⇒≡ E).
The first and the fourth case are dealt with in the proof of cut elimination in [10]. The fifth case can be dealt with in a similar way as the first, by pushing cut up until it disappears either because in the opposite premiss the atom was introduced by (W ⇒) or it is an axiom. For the remaining cases it is sufficient to prove: 7.0.1. Acknowledgements.
I would like to thank the anonymous reviewers and Nils Kürbis for valuable comments. Funded by the European Union (ERC, ExtenDD, project number: 101054714). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.