=Paper=
{{Paper
|id=Vol-3875/ARQNL2024_paper6
|storemode=property
|title=When Epsilon meets Lambda: Extended Leśniewski's Ontology
|pdfUrl=https://ceur-ws.org/Vol-3875/ARQNL2024_paper6.pdf
|volume=Vol-3875
|authors=Andrzej Indrzejczak
|dblpUrl=https://dblp.org/rec/conf/arqnl/Indrzejczak24
}}
==When Epsilon meets Lambda: Extended Leśniewski's Ontology==
https://ceur-ws.org/Vol-3875/ARQNL2024_paper6.pdf
When Epsilon meets Lambda: Extended Leśniewski’s
Ontology⋆
Andrzej Indrzejczak
Department of Logic, University of Lodz, Poland
Abstract
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.
Keywords
Leśniewski, ontology, calculus of names, sequent calculus, cut elimination
1. Introduction
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
ARQNL 2024: Automated Reasoning in Quantified Non-Classical Logics, 1 July 2024, Nancy, France
$ andrzej.indrzejczak@filhist.uni.lodz.pl (A. Indrzejczak)
0000-0003-4063-1651 (A. Indrzejczak)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
ceur-ws.org
ISSN 1613-0073 ARQNL 2024 62 P ROCEEDINGS
Proceedings
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 well-
behaved 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.
63
2. Extended Ontology of Leśniewski
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 Rn , 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 Rt1 ...tn , where all arguments are simple terms, i.e. variables, identities t1 ≡ t2 , where
both arguments can be simple or complex, and ε-atoms t1 εt2 . 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 ≡ t) = c(s) + c(t) + 1.
We consider the hierarchy of three languages: weak, medium and strong, depending on what
kind of terms are admitted as arguments of ε-atoms t1 εt2 :
1. Lw : t1 simple, t2 arbitrary;
2. Lm : additionally ε-atoms with both arguments complex;
3. Ls : additionally ε-atoms with t1 complex and t2 simple.
So only Ls admits all possible combinations of terms, as in identities.
Note that in the setting of ELO, the axiom LA covers in fact four schemata:
LA1 ab ↔ ∃z(za) ∧ ∀z(za → zb) ∧ ∀zv(za ∧ va → zv):
LA2 aλxψ ↔ ∃z(za) ∧ ∀z(za → zλxψ) ∧ ∀zv(za ∧ va → zv);
LA3 λxϕλxψ ↔ ∃z(zλxϕ) ∧ ∀z(zλxϕ → zλxψ) ∧ ∀zv(zλxϕ ∧ vλxϕ → zv);
LA4 λxϕb ↔ ∃z(zλxϕ) ∧ ∀z(zλxϕ → zb) ∧ ∀zv(zλxϕ ∧ vλxϕ → zv).
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:
1. weak ELOw in Lw satisfying LA1 , LA2 ;
2. medium ELOm in Lm satisfying LA1 , LA2 , LA3 ;
3. strong ELOs in Ls satisfying LA1 , LA2 , LA3 , LA4 .
64
However, even ELOs 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:
aλxϕ ↔ aa ∧ ϕ[x/a]
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:
t ≡ s ↔ ∀x(xt ↔ xs)
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: LA1 , LA2 in LOw , LA1 , LA2 , LA3 in LOm , and
LA1 , LA2 , LA3 , LA4 in LOs .
3. Sequent Calculi GELO
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 LA1 (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 Lw , Lm , Ls , i.e. with added relational atoms and lambda
terms, is too weak to obtain any specific results related to complex terms. Moreover, with quan-
tifier 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 GELOw we have to add to GOI (in Lw ) the rules from Fig. 2. The most direct
way to obtain the system capable of proving LA2 is to strengthen the rules (R), (T ), (S), (E)
65
Γ ⇒ ∆, ϕ ϕ, Π ⇒ Σ
(Cut) (AX) ϕ ⇒ ϕ
Γ, Π ⇒ ∆, Σ
Γ ⇒ ∆, ϕ ϕ, Γ ⇒ ∆ Γ⇒∆
(¬⇒) (⇒¬) (W⇒)
¬ϕ, Γ ⇒ ∆ Γ ⇒ ∆, ¬ϕ ϕ, Γ ⇒ ∆
Γ ⇒ ∆, ϕ Γ ⇒ ∆, ψ ϕ, ψ, Γ ⇒ ∆ Γ⇒∆
(⇒∧) (∧⇒) (⇒W )
Γ ⇒ ∆, ϕ ∧ ψ ϕ ∧ ψ, Γ ⇒ ∆ Γ ⇒ ∆, ϕ
ϕ, Γ ⇒ ∆ ψ, Γ ⇒ ∆ Γ ⇒ ∆, ϕ, ψ ϕ, ϕ, Γ ⇒ ∆
(∨⇒) (⇒∨) (C⇒)
ϕ ∨ ψ, Γ ⇒ ∆ Γ ⇒ ∆, ϕ ∨ ψ ϕ, Γ ⇒ ∆
Γ ⇒ ∆, ϕ ψ, Γ ⇒ ∆ ϕ, Γ ⇒ ∆, ψ Γ ⇒ ∆, ϕ, ϕ
(→⇒) (⇒→) (⇒C)
ϕ → ψ, Γ ⇒ ∆ Γ ⇒ ∆, ϕ → ψ Γ ⇒ ∆, ϕ
Γ⇒ ∆, ϕ, ψ ϕ, ψ, Γ⇒ ∆ ϕ[x/b], Γ⇒ ∆ Γ⇒ ∆, ϕ[x/b]
(↔⇒) (∀⇒) (⇒∃)
ϕ ↔ ψ, Γ⇒ ∆ ∀xϕ, Γ⇒ ∆ Γ⇒ ∆, ∃xϕ
ϕ, Γ⇒ ∆, ψ ψ, Γ ⇒ ∆, ϕ Γ⇒ ∆, ϕ[x/a] ϕ[x/a], Γ⇒ ∆
(⇒↔) (⇒∀) (∃⇒)
Γ⇒ ∆, ϕ ↔ ψ Γ⇒ ∆, ∀xϕ ∃xϕ, Γ⇒ ∆
Γ⇒ ∆, bt, bs bt, bs, Γ⇒ ∆ at, Γ⇒ ∆, as as, Γ ⇒ ∆, at
(≡⇒) (⇒≡)
t ≡ s, Γ⇒ ∆ Γ⇒ ∆, t ≡ s
bb, Γ⇒ ∆ bd, Γ⇒ ∆ cb, Γ⇒ ∆
(R) (T ) (S)
bc, Γ⇒ ∆ bc, cd, Γ⇒ ∆ bc, cc, Γ⇒ ∆
ab, Γ⇒ ∆, ac ac, Γ⇒ ∆, ab cd, Γ ⇒ ∆
(E)
bd, Γ ⇒ ∆
where a is a fresh parameter (eigenvariable), not present in Γ, ∆ and ϕ, whereas b, c, d are arbitrary
parameters, t, s are arbitrary terms.
Figure 1: Calculus GOI
ϕ[x/b], Γ⇒ ∆ Γ⇒ ∆, bb Γ⇒ ∆, ϕ[x/b]
(β ⇒) (⇒ β)
bλxϕ, Γ⇒ ∆ Γ⇒ ∆, bλxϕ
a ≡ t, Γ⇒ ∆ Γ⇒ ∆, b ≡ c Γ⇒ ∆, ϕ[x/c]
(≡⇒ E) (⇒≡ E)
Γ⇒ ∆ Γ⇒ ∆, ϕ[x/b]
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.
Figure 2: The rules for GELOw
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 LA2 ; the rules which apparently characterise only LA1 are
sufficient for this aim (it will be shown in section 5), and it is crucial for proving cut elimination
in section 6.
66
(⇒ β) 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 (∀ ⇒):
a ≡ t, ϕ[x/a] ⇒ ϕ[x/t]
(∀ ⇒)
a ≡ t, ∀xϕ ⇒ ϕ[x/t]
(≡⇒ E)
∀xϕ ⇒ ϕ[x/t] ϕ[x/t], Γ ⇒ ∆
(Cut)
∀xϕ, Γ ⇒ ∆
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 (⇒ ∃):
(⇒≡) at ⇒ at at ⇒ at
a ≡ t, Γ ⇒ ∆
(⇒ ∃) ⇒ t ≡ t (∃ ⇒)
⇒ ∃x(x ≡ t) ∃x(x ≡ t), Γ ⇒ ∆
(Cut)
Γ⇒∆
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 GELOm we add the rules from Fig. 3 to GELOw formulated in Lm . 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 GELOs we change the
language for Ls 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:
• GELOw is obtained by addition of the rules from Fig. 2 to GOI in Lw ;
• GELOm is obtained by addition of the rules from Fig. 3 to GELOw in Lm ;
67
aλxϕ, at, Γ⇒ ∆ Γ⇒ ∆, cλxϕ Γ⇒ ∆, dλxϕ cd, Γ ⇒ ∆
(λ ⇒ 1) (λ ⇒ 2)
λxϕt, Γ⇒ ∆ λxϕt, Γ ⇒ ∆
Γ⇒ ∆, cλxϕ Γ⇒ ∆, ct aλxϕ, bλxϕ, Γ ⇒ ∆, ab
(⇒ λ)
Γ ⇒ ∆, λxϕt
where a, b are new parameters (eigenvariable), c, d are arbitrary, t is complex.
Figure 3: The rules for GELOm
• GELOs is obtained by relaxing the condition on t in rules from Fig. 3 in Ls .
We finish this section with an example of a cut-free proof of the sequent which will be useful
in further considerations:
Lemma 1. The following sequent is cut-free provable in GELOw and all its extensions:
ac ⇒ ac (T )
bλxϕ ⇒ bc, bλxϕ bc, bλxϕ, ab ⇒ ac
(≡⇒)
c ≡ λxϕ, bλxϕ, ab ⇒ ac, aλxϕ ac, aλxϕ ⇒ aλxϕ
(≡⇒)
c ≡ λxϕ, ab, bλxϕ ⇒ aλxϕ
(≡⇒ E)
ab, bλxϕ ⇒ aλxϕ
4. Identity
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).
Lemma 2. The following sequents are cut-free provable in all variants of GELO for arbitrary
s, t, u:
1. ⇒ t ≡ t
2. s ≡ t ⇒ t ≡ s
3. s ≡ t, s ≡ u ⇒ t ≡ u
4. s ≡ t, u ≡ s ⇒ u ≡ t
5. t ≡ s, s ≡ u ⇒ t ≡ u
6. t ≡ s, u ≡ s ⇒ u ≡ t
Proof. Case 1 is trivial, by one application of (⇒≡). Case 2:
at ⇒ as, at as, at ⇒ as as ⇒ as, at as, at ⇒ at
(≡⇒) (≡⇒)
at, s ≡ t ⇒ as as, s ≡ t ⇒ at
(⇒≡)
s≡t⇒t≡s
Case 3:
as ⇒ as, au as, au ⇒ au
(≡⇒)
at ⇒ as, at as, at, s ≡ u ⇒ au
(≡⇒)
s ≡ t, s ≡ u, at ⇒ au s ≡ t, s ≡ u, au ⇒ at
(⇒≡)
s ≡ t, s ≡ u ⇒ t ≡ u
68
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.
Lemma 3. GELOw ⊢ s ≡ t, ϕ[x/s] ⇒ ϕ[x/t]
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:
1. s ≡ t, us ⇒ ut
2. s ≡ t, su ⇒ tu
3. t ≡ s, us ⇒ ut
4. t ≡ s, su ⇒ tu
Case 1: u must be simple (the character of s, t does not matter):
us ⇒ us, ut us, ut ⇒ ut
(≡⇒)
s ≡ t, us ⇒ ut
Case 2: s, t are simple; let u be simple (subcase 2.1):
as ⇒ as, at as, at ⇒ at at ⇒ as, at as, at ⇒ as
(≡⇒) (≡⇒)
s ≡ t, as ⇒ at s ≡ t, at ⇒ as tu ⇒ tu
(E)
s ≡ t, su ⇒ tu
Subcase 2.2: let u be complex:
tc ⇒ tc, tu tc, tu ⇒ tu
(≡⇒)
s ≡ t, as ⇒ at s ≡ t, at ⇒ as tc, su, c ≡ u ⇒ tu
(E)
su ⇒ sc, su sc, su, c ≡ u, s ≡ t ⇒ tu
(≡⇒)
c ≡ u, s ≡ t, su ⇒ tu
(≡⇒ E)
s ≡ t, su ⇒ tu
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.
Lemma 4. GELOm ⊢ s ≡ t, ϕ[x/s] ⇒ ϕ[x/t]
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:
69
bu ⇒ bu cu ⇒ cu bc ⇒ bc
(λ ⇒ 2)
au ⇒ au s ≡ t, as ⇒ at us, bu, cu ⇒ bc
(⇒ λ)
s ≡ t, au, as, us ⇒ ut
(λ ⇒ 1)
s ≡ t, us ⇒ ut
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:
s ≡ t, as ⇒ at au ⇒ au s ≡ t, su, bt, ct ⇒ bc
(⇒ λ)
s ≡ t, as, au, su ⇒ tu
(λ ⇒ 1)
s ≡ t, su ⇒ tu
where s ≡ t, as ⇒ at is the case 1 of the previous lemma and s ≡ t, su, bt, ct ⇒ bc is proven
as follows:
bs ⇒ bs cs ⇒ cs bc ⇒ bc
(λ ⇒ 2)
ct ⇒ cs, ct cs, ct, su, bs ⇒ bc
(≡⇒)
bt ⇒ bs, bt bs, bt, s ≡ t, su, ct ⇒ bc
(≡⇒)
s ≡ t, su, bt, ct ⇒ bc
2.2: s simple, t complex:
ss ⇒ ss, st ss, st ⇒ st
(≡⇒)
s ≡ t, ss ⇒ st su ⇒ su s ≡ t, ss, bt, ct ⇒ bc
(⇒ λ)
s ≡ t, ss, su ⇒ tu
(R)
su ⇒ sa, su sa, su, s ≡ t ⇒ tu
(≡⇒)
a ≡ u, s ≡ t, su ⇒ tu
(≡⇒ E)
s ≡ t, su ⇒ tu
where the rightmost sequent is proved as follows:
bc ⇒ bc (T )
sc, bs ⇒ bc
(S)
ct ⇒ cs, ct cs, ct, ss, bs ⇒ bc
(≡⇒)
bt ⇒ bs, bt bs, bt, s ≡ t, ss, ct ⇒ bc
(≡⇒)
s ≡ t, ss, bt, ct ⇒ bc
2.3. s complex, t simple:
tc ⇒ tc, tu tc, tu ⇒ tu
(≡⇒)
D1 D2 tc, c ≡ u ⇒ tu
(E)
au ⇒ ac, au ac, au, c ≡ u, s ≡ t, as, su ⇒ tu
(≡⇒)
c ≡ u, s ≡ t, as, au, su ⇒ tu
(≡⇒ E)
s ≡ t, as, au, su ⇒ tu
(λ ⇒ 1)
s ≡ t, su ⇒ tu
70
where D1 is:
bs ⇒ bs as ⇒ as ba ⇒ ba
(λ ⇒ 2)
bt ⇒ bs, bt bs, bt, as, su ⇒ ba
(≡⇒)
s ≡ t, as, su, bt ⇒ ba
and D2 is:
ba, as ⇒ bs
(⇒ W )
as, ba ⇒ bs, bt bs, bt ⇒ bt
(≡⇒)
s ≡ t, as, ba ⇒ bt
where ba, as ⇒ bs is a generalised transitivity cut-free provable by lemma 1.
Proving LL for GELOs , 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.
5. Adequacy of GELO
To show that all variants of GELO adequately characterise respective forms of ELO we demon-
strate that different variants of LA are provable and that these rules are derivable if we use
respective forms of LA as additional axioms. LA1 was proved in [10] by means of the rules
(R), (S), (T ), (E), which were in turn shown derivable in the presence of LA1 . These proofs
are correct in GELOw so we only need to prove LA2 :
Lemma 5. aλxψ ↔ ∃x(xa) ∧ ∀x(xa → xλxψ) ∧ ∀xy(xa ∧ ya → xy) is provable in GELOw .
aa ⇒ aa (⇒ ∃)
aa ⇒ ∃x(xa)
(R)
aλxϕ ⇒ ab, aλxϕ ab, aλxϕ ⇒ ∃x(xa)
(≡⇒)
b ≡ λxϕ, aλxϕ ⇒ ∃x(xa)
(≡⇒ E)
aλxϕ ⇒ ∃x(xa)
bc ⇒ bc (T )
aλxϕ ⇒ ac, aλxϕ ac, aλxϕ, ba ⇒ bc
(≡⇒)
c ≡ λxϕ, aλxϕ, ba ⇒ bc, bλxϕ bc, bλxϕ ⇒ bλxϕ
(≡⇒)
c ≡ λxϕ, aλxϕ, ba ⇒ bλxϕ
(≡⇒ E)
aλxϕ, ba ⇒ bλxϕ
(⇒→)
aλxϕ ⇒ ba → bλxϕ
(⇒ ∀)
aλxϕ ⇒ ∀x(xa → xλxϕ)
71
cd ⇒ cd (T )
ca, ad ⇒ cd
(S)
aa, ca, da ⇒ cd
(R)
aλxϕ ⇒ ab, aλxϕ ab, aλxϕ, ca, da ⇒ cd
(≡⇒)
b ≡ λxϕ, aλxϕ, ca, da ⇒ cd
(∧ ⇒)
b ≡ λxϕ, aλxϕ, ca ∧ da ⇒ cd
(⇒→)
b ≡ λxϕ, aλxϕ ⇒ ca ∧ da → cd
(⇒ ∀)
b ≡ λxϕ, aλxϕ ⇒ ∀xy(xa ∧ ya → xy)
(≡⇒ E)
aλxϕ ⇒ ∀xy(xa ∧ ya → xy)
yield together by (⇒ ∧) and (⇒→) the left-right implication of LA2 . The other part is proved
as follows:
bλxϕ ⇒ bc, bλxϕ D
(≡⇒)
c ≡ λxϕ, ba, bλxϕ, ∀xy(xa ∧ ya → xy) ⇒ aλxϕ
(≡⇒ E)
ba ⇒ ba ba, bλxϕ, ∀xy(xa ∧ ya → xy) ⇒ aλxϕ
(→⇒)
ba, ba → bλxϕ, ∀xy(xa ∧ ya → xy) ⇒ aλxϕ
(∀ ⇒)
ba, ∀x(xa → xλxϕ), ∀xy(xa ∧ ya → xy) ⇒ aλxϕ
(∃ ⇒)
∃x(xa), ∀x(xa → xλxϕ), ∀xy(xa ∧ ya → xy) ⇒ aλxϕ
where D is:
da ⇒ da (T ) ac ⇒ ac, aλxϕ ac, aλxϕ ⇒ aλxϕ
(≡⇒)
D1 ba, db ⇒ da ac, c ≡ λxϕ ⇒ aλxϕ
(E)
bc, bλxϕ, c ≡ λxϕ, ba, ∀xy(xa ∧ ya → xy) ⇒ aλxϕ
where D1 is:
(⇒ ∧) ba ⇒ ba da ⇒ da
ba, da ⇒ da ∧ ba db ⇒ db
(→⇒)
ba, da, da ∧ ba → db ⇒ db
(∀ ⇒)
ba, ∀xy(xa ∧ ya → xy), da ⇒ db
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 LA1 ) are the rules for ≡; even the
rules for β-conversion are not required.
The adequacy of GELOm (and GELOs 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 LA3 used as an
additional axiomatic sequent.
Proof. For (λ ⇒ 1):
72
aλxϕ ⇒ aλxϕ at ⇒ at
(→⇒)
aλxϕ → at, aλxϕ ⇒ at aλxϕ, at, Γ ⇒ ∆
(Cut)
aλxϕ → at, aλxϕ, Γ ⇒ ∆
(∀ ⇒)
∀x(xλxϕ → xt), aλxϕ, Γ ⇒ ∆
(∃ ⇒)
∀x(xλxϕ → xt), ∃x(xλxϕ), Γ ⇒ ∆
by two cuts with λxϕt ⇒ ∀x(xλxϕ → xt), λxϕt ⇒ ∃x(xλxϕ) which are derivable from LA3 .
For (λ ⇒ 2):
Γ ⇒ ∆, bλxϕ Γ ⇒ ∆, cλxϕ
(⇒ ∧)
Γ ⇒ ∆, bλxϕ ∧ cλxϕ bc, Γ ⇒ ∆
(→⇒)
bλxϕ ∧ cλxϕ → bc, Γ ⇒ ∆
(∀ ⇒)
S ∀xy(xλxϕ ∧ yλxϕ → xy), Γ ⇒ ∆
(Cut)
λxϕt, Γ ⇒ ∆
where S is λxϕt ⇒ ∀xy(xλxϕ ∧ yλxϕ → xy) which is derivable from LA3 . For (⇒ λ) first
we prove:
aλxϕ ⇒ aλxϕ bλxϕ ⇒ bλxϕ
(⇒ ∧)
aλxϕ, bλxϕ ⇒ aλxϕ ∧ bλxϕ ab, bt ⇒ at
(→⇒)
aλxϕ, bλxϕ, bt, aλxϕ ∧ bλxϕ → ab ⇒ at
(∀ ⇒)
aλxϕ, bλxϕ, bt, ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ at
(⇒→)
bλxϕ, bt, ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ aλxϕ → at
(⇒ ∀)
bλxϕ, bt, ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ ∀x(xλxϕ → xt)
where the rightmost sequent is proved by lemma 1 (in case of LA4 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(xλxϕ ∧ yλxϕ → xy) respectively, by cuts
with ∃x(xλxϕ), ∀x(xλxϕ → xt), ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ λxϕt (derivable from LA3 )
we get ∀x(xλxϕ → xt), Γ ⇒ ∆, λxϕt. Two final cuts yield the conclusion of (⇒ λ).
Lemma 7. λxϕt ↔ ∃x(xλxϕ) ∧ ∀x(xλxϕ → xt) ∧ ∀xy(xλxϕ ∧ yλxϕ → xy) is provable in
GELOm with t complex, and in GELOs with t arbitrary.
aλxϕ, at ⇒ aλxϕ
(⇒ ∃)
aλxϕ, at ⇒ ∃x(xλxϕ)
(λ ⇒ 1)
λxϕt ⇒ ∃x(xλxϕ)
aλxϕ ⇒ aλxϕ bλxϕ ⇒ bλxϕ ab, bt ⇒ at
(λ ⇒ 2)
aλxϕ, bλxϕ, bt, λxϕt ⇒ at
(λ ⇒ 1)
aλxϕ, λxϕt ⇒ at
(⇒→)
λxϕt ⇒ aλxϕ → at
(⇒ ∀)
λxϕt ⇒ ∀x(xλxϕ → xt)
73
where the rightmost sequent is proved by lemma 1 (or by (T ) in case of LA4 ).
aλxϕ ⇒ aλxϕ bλxϕ ⇒ bλxϕ ab ⇒ ab
(λ ⇒ 2)
λxϕt, aλxϕ, bλxϕ ⇒ ab
(∧ ⇒)
λxϕt, aλxϕ ∧ bλxϕ ⇒ ab
(⇒→)
λxϕt ⇒ aλxϕ ∧ bλxϕ → ab
(⇒ ∀)
λxϕt ⇒ ∀xy(xλxϕ ∧ yλxϕ → xy)
the above proofs yield the left-right part of LA3 after application of (⇒ ∧) and (⇒→). For
the right-left implication we derive:
aλxϕ ⇒ aλxϕ at, aλxϕ, ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ λxϕt
(→⇒)
aλxϕ, aλxϕ → at, ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ λxϕt
(∀ ⇒)
aλxϕt, ∀x(xλxϕ → xt), ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ λxϕt
(∃ ⇒)
∃x(xλxϕ), ∀x(xλxϕ → xt), ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ λxϕt
where the rightmost sequent is proved as follows:
bλxϕ ⇒ bλxϕ cλxϕ ⇒ cλxϕ
(⇒ ∧)
bλxϕ, cλxϕ ⇒ bλxϕ ∧ cλxϕ bc ⇒ bc
(→⇒)
bλxϕ, cλxϕ, bλxϕ ∧ cλxϕ → bc ⇒ bc
(∀ ⇒)
aλxϕ ⇒ aλxϕ at ⇒ at bλxϕ, cλxϕ, ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ bc
(⇒ λ)
at, aλxϕ, ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ λxϕt
Together, these two lemmata guarantee the adequacy of GELOm . For GELOs 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:
cb ⇒ cb
(T )
aλxϕ ⇒ ab, aλxϕ ab, aλxϕ, ca ⇒ cb
(≡⇒)
D b ≡ λxϕ, aλxϕ, ca ⇒ cb bt, b ≡ λxϕ ⇒ λxϕt
(E)
b ≡ λxϕ, at, aλxϕ, ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ λxϕt
(≡⇒ E)
at, aλxϕ, ∀xy(xλxϕ ∧ yλxϕ → xy) ⇒ λxϕt
where the rightmost leaf is provable as an instance of LL, and D is:
b ≡ λxϕ, cb ⇒ cλxϕ aλxϕ ⇒ aλxϕ
(⇒ ∧)
b ≡ λxϕ, aλxϕ, cb ⇒ cλxϕ ∧ aλxϕ ca ⇒ ca
(→⇒)
b ≡ λxϕ, aλxϕ, cλxϕ ∧ aλxϕ → ca, cb ⇒ ca
(∀ ⇒)
b ≡ λxϕ, aλxϕ, ∀xy(xλxϕ ∧ yλxϕ → xy), cb ⇒ ca
where the leftmost leaf again is a provable instance of LL.
74
6. Cut Elimination Theorem
Before we focus on the proof of the cut elimination theorem let us note that for all variants of
GELO the following result holds:
Lemma 8 (Substitution). If ⊢k Γ ⇒ ∆, then ⊢k Γ[a/b] ⇒ ∆[a/b].
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 height-
preserving 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
GELOw and GELOm . 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:
75
Lemma 9. 1. The rules (⇒ β) with (β ⇒) are reductive in general;
2. Both (⇒ λ) with (λ ⇒ 1), and (⇒ λ) with (λ ⇒ 2) are reductive in GELOm .
Proof. The two rules of β-conversion are trivially reductive. It remains to show that the three
rules for λ are reductive in GELOm .
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:
Γ ⇒ ∆, cλxϕ cλxϕ, cλyψ, Π ⇒ Σ
(Cut)
Γ ⇒ ∆, cλyψ cλyψ, Γ, Π ⇒ ∆, Σ
(Cut)
Γ, Γ, Π ⇒ ∆, ∆, Σ
(C ⇒), (⇒ C)
Γ, Π ⇒ ∆, Σ
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:
Π ⇒ Σ, cλxϕ cλxϕ, dλxϕ, Γ ⇒ ∆, cd
(Cut)
Π ⇒ Σ, dλxϕ dλxϕ, Γ, Π ⇒ ∆, Σ, cd
(Cut)
Γ, Π, Π ⇒ ∆, Σ, Σ, cd cd, Π ⇒ Σ
(Cut)
Γ, Π, Π, Π ⇒ ∆, Σ, Σ, Σ
(C ⇒), (⇒ C)
Γ, Π ⇒ ∆, Σ
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 GELOw and GELOm can be transformed into a cut-free proof.
What with GELOs ? Note that in GELOs 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 GELOs 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 GELOw or GELOm , we obtain:
Theorem 2. Every proof in GELOs can be transformed into a cut-free proof.
And as the consequence of these theorems we obtain:
Corollary 1. If ⊢ Γ ⇒ ∆ in GELOw , GELOm or GELOs , then it is provable in a proof which is
closed under subformulae of Γ ∪ ∆ and atomic formulae with possibly new parameters.
76
7. Conclusion
ELO, similarly to LO, is not characterised semantically here. In fact, there are known controver-
sies 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, Γ⇒ ∆ Γ⇒ ∆, bs bt, bs, Γ⇒ ∆
(≡⇒ 1) (≡⇒ 2)
t ≡ s, Γ⇒ ∆ 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.
77
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.
References
[1] Artale, A., Mazzullo, A., Ozaki, A., Wolter, F.: On Free Description Logics with Definite
Descriptions. In: Bienvenu, M., Lakemeyer, G., Erdem, E. (eds.): Proceedings of the 18th
International Conference on Principles of Knowledge Representation and Reasoning, pp.
63–73. IJCAI Organization (2021).
[2] Ben-Yami, H.: Logic and Natural Language: On Plural Reference and Its Semantic and
Logical Significance. Routledge, New York (2004).
[3] Borgida, A., Toman, D., Weddell, G.: On Referring Expressions in Query Answering over
First Order Knowledge Bases. In: Proceedings of the 15th International Conference on
Principles of Knowledge Representation and Reasoning, pp. 319–328. IJCAI Organization
(2016).
[4] Braüner, T.: Hybrid Logic and its Proof-Theory. Springer, Cham (2011).
[5] Ciabattoni, A.: Automated Generation of Analytic Calculi for Logics with Linearity. In:
Marcinkowski, J., Tarlecki, A. (eds.): CSL 2004, LNCS vol. 3210, pp. 503–517. Springer,
Heidelberg (2004).
[6] Girard, J-Y.: From Foundations to Ludics. The Bulletin of Symbolic Logic. 9(2), 131–168
(2003).
[7] Indrzejczak, A.: Free Logics are Cut-free. Studia Logica 109(4) 859–886 (2021).
[8] Indrzejczak, A.: A Novel Approach to Equality. Synthese 199 4749–4774 (2021).
[9] Indrzejczak, A.: Sequents and Trees. An Introduction to the Theory and Applications of
Propositional Sequent Calculi. Birkhäuser (2021).
[10] Indrzejczak, A.: Leśniewski’s Ontology – Proof-Theoretic Characterization. In: Blanchette,
J., Kovacs, L., Pattinson, D. (eds.) Automated Reasoning, IJCAR 2022, LNAI vol. 13385, pp.
541–558. Springer, Heidelberg (2022).
[11] Indrzejczak, A.: Russellian definite description theory—a proof-theoretic approach. The
Review of Symbolic Logic. 16(2), 624–649 (2023).
[12] Indrzejczak, A.: Leśniewski’s Ontology satisfies interpolation. Proceedings of AWPL,
Sapporo (2024).
[13] Indrzejczak, A., Kürbis, N.: A Cut-Free, Sound and Complete Russellian Theory of Definite
Descriptions. In: Ramanayake, R., Urban, J. (eds) Automated Reasoning with Analytic
Tableaux and Related Methods. TABLEAUX 2023. Lecture Notes in Computer Science, vol.
14278, pp. 131–149. Springer, Cham (2023).
[14] Indrzejczak, A., Zawidzki, M.: When Iota meets Lambda. Synthese 201/72 (2023), DOI:
10.1007/s11229-023-04048-y.
[15] Iwanuś, B.: On Leśniewski’s Elementary Ontology. Studia Logica 31(1), 73–119 (1973).
78
[16] Küng, G., Canty, J.T.: Substitutional quantification and Leśniewskian quantifiers. Theoria
36, 165–182 (1970).
[17] Leśniewski, S.: Collected Works. Vol. II. Surma, S., Srzednicki, J., Barnett, D.I. Kluwer/PWN
(1992).
[18] Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press, Cambridge
(2001).
[19] Oliver, A., Smiley, T.: Plural Logic. Oxford University Press, Oxford (2016).
[20] Paśniczek, J.: The Logic of Intentional Objects. A Meinongian Version of Classical Logic.
Kluwer, Dordrecht (1998).
[21] Pratt-Hatmann, I., Moss, L.,S.: Logics for the Relational Syllogistic. The Review of Symbolic
Logic. 2(4), 647–683 (2023).
[22] Rickey, F.: Interpretations of Leśniewski’s Ontology. Dialectica 39(3), 181–192 (1985).
[23] Schroeder-Heister, P.: Proof-theoretic Semantics. in: Stanford Encyclopedia of Philosophy
2012, https://plato.stanford.edu/entries/proof-theoretic-semantics/.
[24] Słupecki, J.: S. Leśniewski’s Calculus of Names. Studia Logica 3(1), 7–72 (1955).
[25] Sommers, F.: The Logic of Natural Language. Clarendon Press, Oxford (1982).
[26] Urbaniak, R.: Leśniewski’s Systems of Logic and Foundations of Mathematics. Springer,
Cham (2014).
[27] Waragai, T.: Ontology as a Natural Extension of Predicate Calculus with Identity Equipped
with Description. Annals of the Japan Association for Philosophy of Science, 7(5), 233–250
(1990).
79