=Paper=
{{Paper
|id=Vol-3875/ARQNL2024_paper5
|storemode=property
|title=Bisequent Calculi for Neutral Free Logic with Definite Descriptions
|pdfUrl=https://ceur-ws.org/Vol-3875/ARQNL2024_paper5.pdf
|volume=Vol-3875
|authors=Andrzej Indrzejczak,Yaroslav Petrukhin
|dblpUrl=https://dblp.org/rec/conf/arqnl/IndrzejczakP24
}}
==Bisequent Calculi for Neutral Free Logic with Definite Descriptions==
https://ceur-ws.org/Vol-3875/ARQNL2024_paper5.pdf
Bisequent Calculi for Neutral Free Logic with Definite
Descriptions
Andrzej Indrzejczak1 , Yaroslav Petrukhin1
1
University of Lodz, 3/5 Lindleya St, Lodz, 90-131, Poland
Abstract
We present a bisequent calculus (BSC) for the minimal theory of definite descriptions (DD) in the setting of
neutral free logic, where formulae with non-denoting terms have no truth value. The treatment of quantifiers,
atomic formulae and simple terms is based on the approach developed by Pavlović and Gratzl. We extend their
results to the version with identity and definite descriptions. In particular, the admissibility of cut is proven for
this extended system.
Keywords
Bisequent Calculus, Cut Elimination, Three-valued Logic, Neutral Free Logic, First-order Logic, Definite Descrip-
tions
1. Introduction
There is a variety of logics called free logics (FL) and differing in many respects. The common feature
is that singular terms are free from existential assumptions, i.e. they are not assumed to denote an
existing object. On the other hand, in all free logics quantifiers are assumed to have an existential
import. One of the main divisions of this kind of logics is based on the treatment of atomic formulae
with non-denoting terms. In positive FL they can be true, in negative FL they are always false, in neutral
FL (NFL) they are neither true nor false. This makes NFL in a sense a kind of partial or three-valued
logic, with the third value expressing the truth-value gap.
We focus on the proof-theoretic perspective on free logics, namely the examination of sequent calculi
(SC). In case of positive and negative FL one may find several studies, due to Maffezioli and Orlandelli
[16], Pavlović and Gratzl [18], or Indrzejczak [5]. However, in case of NFL the situation is worse in
general, and particularly poor in the field of proof theory. In addition to the papers of Woodruff [21] and
Lehmann [15], where one may find some kind of natural deduction and tableau system, only Pavlović
and Gratzl [19] recently investigated SC for NFL based on strong and weak Kleene logics [11].
We are going to continue the research carried out in [19] in two ways: first, we reformulate the
results from [19] using our own approach based on bisequent calculi (BSC), developed in [9, 7]; second,
we extend the resulting proof systems to cover identity and definite descriptions (DD). These complex
terms are usually divided into proper (denoting a unique object, like ‘the present King of England’)
and improper (like non-denoting ‘the present King of France’ or not unique ‘the author of Principia
exploring their behaviour. Usually, DD are formalised by means of term-forming 𝚤-operator applied to a
Mathematica’). Improper DD are very troublesome and it seems that NFL is quite natural place for
variable 𝑥 and formula 𝜑 to obtain a term 𝚤𝑥𝜑. It is worth noting that there is an alternative treatment
follow here a more standard, 𝚤-operator based approach.
of DD based on the application of binary quantifier and recently developed by Kürbis [12, 13, 14]. We
The theories of DD in positive or negative free logics are usually based on Lambert axiom (𝐿):
∀𝑦(𝑦 = 𝚤𝑥𝜑 ↔ ∀𝑥(𝜑 ↔ 𝑦 = 𝑥)) (𝐿)
where 𝚤𝑥𝜑 is closed and does not have any occurrence of 𝑦. It is the weakest principle characterising the
behaviour of proper DD. In our research, devoted to NFL, we consider (𝐿) as well but to avoid using ↔,
ARQNL 2024: Automated Reasoning in Quantified Non-Classical Logics, 1 July 2024, Nancy, France
Envelope-Open andrzej.indrzejczak@filhist.uni.lodz.pl (A. Indrzejczak); yaroslav.petrukhin@gmail.com (Y. Petrukhin)
Orcid 0000-0003-4063-1651 (A. Indrzejczak); 0000-0002-7731-1339 (Y. Petrukhin)
© 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 48 P ROCEEDINGS
Proceedings
which considerably complicate the set of required rules and proofs in the setting of Kleene’s logic, we
will use instead two axioms which together express the same minimal theory of DD:
∀𝑦(𝑦 = 𝚤𝑥𝜑 → 𝜑[𝑥/𝑦] ∧ ∀𝑥(𝜑 → 𝑦 = 𝑥)) (𝐿→ )
∀𝑦(𝜑[𝑥/𝑦] ∧ ∀𝑥(𝜑 → 𝑦 = 𝑥) → 𝑦 = 𝚤𝑥𝜑) (𝐿← )
Moreover, we add a restriction: 𝚤𝑥𝜑 contains no other DD inside. There is a possible treatment of this
theory admitting nested DD but it leads to the formulation of rules which do not allow us to prove the
admissibility of cut.
Various definitions of the logical connectives and quantifiers can be considered in many-valued
logics in general, and the choice of them has an influence also on the behaviour of DD. In this study,
following [19], we examine two variants of NFL, based on strong and weak Kleene’s [11] interpretation
of connectives.
The goal of the paper is to provide a uniform proof-theoretic treatment of NFL with identity and
DD. Regarding the systems for DD in the setting of other logics, recently a great progress has been
made in the works of Fitting and Mendelsohn [1], Orlandelli [17] and Indrzejczak [6, 10, 8]. The paper
[4], particularly important for us, is devoted to sequent calculi for the theories of DD based on positive
and negative free logics. Currently we are going to continue this research and examine the behaviour
of DD in NFL, however this logic requires some nonstandard sequent basis, like the one originally
applied in [19]. We prefer to use for this aim a slightly different framework, namely a bisequent calculus
(BSC) [9, 7], since it has shown its usefulness in the field of formalisation of three- and four-valued
logics. Moreover, the rules of the generalised sequent calculus from [19] are easily translatable into
BSC. Summing up: the present paper is a combination and a continuation of the research presented in
[18, 5] (SC for negative and positive free logics), [19] (SC for neutral free logics), [4] (SC for DD theories
based on negative and positive free logics), and [9, 7] (BSC for many-valued logics).
The structure of the paper is as follows. Section 2 contains some preliminaries related to the language
and semantics. Section 3 is devoted to the introduction of the BSC for two variants of NFL based on
strong and weak Kleene’s logic. Section 4 is concerned with the constructive proof of cut admissibility.
Section 5 consists of some concluding remarks and open problems.
2. Preliminaries
Following [19], we consider the subsequent language but with added conjunction, for dealing with (𝐿).
Definition 2.1. [19, Definition 1.1] The alphabet of the language ℒ consists of:
(1) Terms: 𝑡, 𝑠, … , consisting of:
(𝑎) Denumerable list of free individual variables (parameters): 𝑎, 𝑏, 𝑐, …
(𝑏) Denumerable list of bound individual variables: 𝑥, 𝑦, 𝑧, …
(2) Denumerable list of 𝑛-ary predicates, including a unary predicate 𝐸
(3) ¬, →, ∧, ∀, (, ).
For our purposes we extend the language ℒ with identity and 𝚤-operator.
Definition 2.2. The alphabet of the language ℒ𝚤= consists of all symbols of the alphabet of the language
ℒ as well as = and 𝚤.
The notions of terms and formulae of the languages ℒ and ℒ𝚤= are defined by simultaneous recursion.
Note that in ℒ𝚤= , 𝑡, 𝑠 represent arbitrary terms, including DD. Complexity of formulae and terms is
measured by the number of logical symbols (including predicates 𝐸 and =). 𝜑[𝑡1 /𝑡2 ] is used for the
operation of correct substitution of an arbitrary term 𝑡2 for all occurrences of a variable/parameter 𝑡1 in
𝜑, and similarly Γ[𝑡1 /𝑡2 ] for a uniform substitution in all formulae in Γ. We use a simplified semantics
from [19, 18] to provide interpretation of this language.
49
Definition 2.3 (Neutral structure 𝒮𝑛𝑡 ). [19, Definition 4.1] [18, Definition 3.1] A neutral structure 𝒮𝑛𝑡 is a
pair ⟨𝒟 , ℐ ⟩, where 𝒟 = 𝑎1 , … , 𝑏1 , … is a countable list of parameters, and ℐ is an interpretation function
on ℒ (ℒ𝚤= ):
• ℐ (𝑡) = 𝑡, where 𝑡 ∈ 𝒟
• ℐ (𝐸) ⊆ 𝒟,
• ℐ (=) = 𝑅𝑒𝑓 ∪ 𝐼 𝑑, closed under symmetry and transitivity, where
– 𝑅𝑒𝑓 = {⟨𝑡, 𝑡⟩ ∣ 𝑡 ∈ ℐ (𝐸)},
– 𝐼 𝑑 ⊆ ℐ (𝐸) × ℐ (𝐸),
• ℐ (𝑃 𝑛 ) ⊆ ℐ (𝐸)𝑛 such that if ⟨𝑠, 𝑡⟩ ∈ ℐ (=), then ⟨… , 𝑠𝑖 , …⟩ ∈ ℐ (𝑃 𝑛 ) iff ⟨… , 𝑡𝑖 , …⟩ ∈ ℐ (𝑃 𝑛 ), for any 𝑛
and any 1 ⩽ 𝑖 ⩽ 𝑛.
Note that identity is in principle treated as other predicates but it cannot be defined in this way since
ℐ is extended to cover descriptions 𝚤𝑥𝜑, where 𝜑 does not contain other DD, by partial mapping from
domains of models contain just parameters, so it should be defined as a condition on models like in [18].
the set of so restricted DDs to 𝒟. In case ℐ (𝚤𝑥𝜑) = 𝑎, for some 𝑎 ∈ ℐ (𝐸), we say that 𝚤𝑥𝜑 is defined and
assume that it satisfies the following condition:
𝑎 iff 𝒱 𝑖 (𝜑[𝑥/𝑎]) = 1 and 𝒱 𝑖 (𝜑[𝑥/𝑏]) = 0 for every 𝑎 ≠ 𝑏 ∈ ℐ (𝐸);
ℐ (𝚤𝑥𝜑) = {
otherwise it is undefined.
There is a matter of debate (cf. [15]) which Kleene’s logic, strong or weak, provides better option for
their approach. Accordingly 𝒱 𝑖 may be either weak (𝑖 = 𝑤) or strong (𝑖 = 𝑠), and is defined as follows:
interpreting truth-value gaps in NFL. Pavlović and Gratzl [19] consider both options and we follow
Definition 2.4 (Weak valuation 𝒱 𝑤 ). (An extended version of [19, Definition 4.2]) The truth-value
assignment 𝒱 𝑤 on the structure ⟨𝒟 , ℐ ⟩ is defined as follows:
1 iff 𝑡 ∈ ℐ (𝐸),
𝒱 𝑤 (𝐸𝑡) = {
0
(1)
iff otherwise;
1 iff ⟨𝑡1 , … , 𝑡𝑛 ⟩ ∈ ℐ (𝑃 𝑛 ),
𝒱 (𝑃 (𝑡1 , … , 𝑡𝑛 )) = { /2
𝑤 𝑛 iff for some 1 ⩽ 𝑖 ⩽ 𝑛, 𝑡𝑖 ∉ ℐ (𝐸),
0
1 (2)
iff otherwise;
1 iff 𝒱 𝑤 (𝜑) = 0,
𝒱 𝑤 (¬𝜑) = { 1/2 iff 𝒱 𝑤 (𝜑) = 1/2,
0 iff 𝒱 𝑤 (𝜑) = 1;
(3)
1 iff 𝒱 𝑤 (𝜑) = 1 and 𝒱 𝑤 (𝜓 ) = 1,
𝒱 𝑤 (𝜑 ∧ 𝜓 ) = { 1/2 iff 𝒱 𝑤 (𝜑) = 1/2 or 𝒱 𝑤 (𝜓 ) = 1/2,
0
(4)
iff otherwise;
0 iff 𝒱 𝑤 (𝜑) = 1 and 𝒱 𝑤 (𝜓 ) = 0,
𝒱 𝑤 (𝜑 → 𝜓 ) = { 1/2 iff 𝒱 𝑤 (𝜑) = 1/2 or 𝒱 𝑤 (𝜓 ) = 1/2,
1
(5)
iff otherwise;
1 iff for every 𝑡 ∈ ℐ (𝐸), 𝒱 𝑤 (𝜑[𝑥/𝑡]) = 1,
𝒱 𝑤 (∀𝑥𝜑) = { 0 iff for some 𝑡 ∈ ℐ (𝐸), 𝒱 𝑤 (𝜑[𝑥/𝑡]) = 0,
1/2
(6)
iff otherwise.
Definition 2.5 (Strong valuation 𝒱 𝑠 ). [19, Definition 4.3] The truth-value assignment 𝒱 𝑠 on the structure
⟨𝒟 , ℐ ⟩ is defined as follows (the other cases are defined as in Definition 2.4):
0 iff 𝒱 𝑠 (𝜑) = 0 or 𝒱 𝑠 (𝜓 ) = 0,
𝒱 𝑠 (𝜑 ∧ 𝜓 ) = { 1 iff 𝒱 𝑠 (𝜑) = 1 and 𝒱 𝑠 (𝜓 ) = 1, (4′ )
1/2 iff otherwise.
50
0 iff 𝒱 𝑠 (𝜑) = 1 and 𝒱 𝑠 (𝜓 ) = 0,
𝒱 (𝜑 → 𝜓 ) = { 1
𝑠 iff 𝒱 𝑠 (𝜑) = 0 or 𝒱 𝑠 (𝜓 ) = 1, (5′ )
1/2 iff otherwise.
𝐷 either as {1} or {1, 1/2}. However, we examine here only the first route, hence in what follows 𝐷
For each of these valuations, we can obtain two different logics by taking the set of designated values
always denotes {1}. The notion of the entailment (consequence) relation is defined as follows.
Definition 2.6. For any set of formulas Γ and any formula 𝜑, it holds that
Γ ⊧ 𝜑 iff for any valuation 𝒱: if 𝒱 (Γ) ⊆ 𝐷, then 𝒱 (𝜑) ∈ 𝐷, where 𝐷 = {1}.
In what follows the strong Kleene’s logic will be referred to as K3 and the weak one as Kw3 . Although
propositional K3 has an empty set of validities it is not so for related NFL as defined by the semantics
above; in particular it holds:
Lemma 2.1. (𝐿→ ) and (𝐿← ) are valid in K3 and Kw
3.
Proof. As an example, let us prove that (𝐿→ ) is valid in K3 . Suppose that (𝐿→ ) is not valid in K3 , that is
𝒱 𝑠 ((𝐿→ )) ≠ 1. Suppose that 𝒱 𝑠 ((𝐿→ )) = 0. Then for some 𝑡 ∈ ℐ (𝐸), 𝒱 𝑠 (𝑡 = 𝚤𝑥𝜑 → 𝜑[𝑥/𝑡] ∧ ∀𝑥(𝜑 →
𝑡 = 𝑥)) = 0. Consequently, 𝒱 𝑠 (𝑡 = 𝚤𝑥𝜑) = 1 and 𝒱 𝑠 (𝜑[𝑥/𝑡] ∧ ∀𝑥(𝜑 → 𝑡 = 𝑥)) = 0. Therefore,
𝒱 𝑠 (𝜑[𝑥/𝑡]) = 0 or 𝒱 𝑠 (∀𝑥(𝜑 → 𝑡 = 𝑥)) = 0. Since 𝑡 ∈ ℐ (𝐸) and 𝒱 𝑠 (𝑡 = 𝚤𝑥𝜑) = 1, 𝒱 𝑠 (𝜑[𝑥/𝑡]) = 1
and 𝒱 𝑠 (𝜑[𝑥/𝑏]) = 0 for every 𝑡 ≠ 𝑏 ∈ ℐ (𝐸). Since 𝒱 𝑠 (𝜑[𝑥/𝑡]) = 1, we get 𝒱 𝑠 (∀𝑥(𝜑 → 𝑡 = 𝑥)) = 0.
Then for some 𝑢 ∈ ℐ (𝐸), 𝒱 𝑠 (𝜑[𝑥/𝑢] → 𝑡 = 𝑢) = 0. Hence, 𝒱 𝑠 (𝜑[𝑥/𝑢]) = 1 and 𝒱 𝑠 (𝑡 = 𝑢) = 0. Since
𝑡 ≠ 𝑢 ∈ ℐ (𝐸), 𝒱 𝑠 (𝜑[𝑥/𝑢]) = 0. A contradiction.
Suppose that 𝒱 𝑠 ((𝐿→ )) = 1/2. Let (𝐻 → ) denote 𝑡 = 𝚤𝑥𝜑 → 𝜑[𝑥/𝑡] ∧ ∀𝑥(𝜑 → 𝑡 = 𝑥). Hence,
we can infer that either there is 𝑡 ∉ ℐ (𝐸) and 𝒱 𝑠 ((𝐻 → )) ∈ {1, 1/2, 0} or there is 𝑡 ∈ ℐ (𝐸) such that
𝒱 𝑠 ((𝐻 → )) = 1/2. Suppose that there is 𝑡 ∉ ℐ (𝐸) and 𝒱 𝑠 ((𝐻 → )) ∈ {1, 1/2, 0}. However, ℐ (=) = 𝑅𝑒𝑓 ∪ 𝐼 𝑑,
where 𝑅𝑒𝑓 = {⟨𝑡, 𝑡⟩ ∣ 𝑡 ∈ ℐ (𝐸)} and 𝐼 𝑑 ⊆ ℐ (𝐸) × ℐ (𝐸). Thus, it cannot be the case that there is 𝑡 ∉ ℐ (𝐸)
and 𝒱 𝑠 ((𝐻 → )) ∈ {1, 1/2, 0}. Hence, there is 𝑡 ∈ ℐ (𝐸) such that 𝒱 𝑠 ((𝐻 → )) = 1/2. It cannot be the case
𝒱 𝑠 (𝑡 = 𝚤𝑥𝜑) = 1/2, otherwise 𝑡 ∉ ℐ (𝐸) or 𝚤𝑥𝜑 ∉ ℐ (𝐸), but ℐ (=) ⊆ ℐ (𝐸). Thus, 𝒱 𝑠 (𝑡 = 𝚤𝑥𝜑) = 1
and 𝒱 𝑠 (𝜑[𝑥/𝑡] ∧ ∀𝑥(𝜑 → 𝑡 = 𝑥)) = 1/2. Since 𝑡 ∈ ℐ (𝐸) and 𝒱 𝑠 (𝑡 = 𝚤𝑥𝜑) = 1, 𝒱 𝑠 (𝜑[𝑥/𝑡]) = 1
and 𝒱 𝑠 (𝜑[𝑥/𝑏]) = 0 for every 𝑡 ≠ 𝑏 ∈ ℐ (𝐸). Since 𝒱 𝑠 (𝜑[𝑥/𝑡]) = 1 and 𝒱 𝑠 (𝜑[𝑥/𝑡] ∧ ∀𝑥(𝜑 → 𝑡 =
𝑥)) = 1/2, we have 𝒱 𝑠 (∀𝑥(𝜑 → 𝑡 = 𝑥)) = 1/2. Hence, we can infer that either there is 𝑢 ∉ ℐ (𝐸) and
𝒱 𝑠 (𝜑[𝑥/𝑢] → 𝑡 = 𝑢) ∈ {1, 1/2, 0} or there is 𝑢 ∈ ℐ (𝐸) such that 𝒱 𝑠 (𝜑[𝑥/𝑢] → 𝑡 = 𝑢) = 1/2. Due to the
properties of ℐ (=), only the latter option holds. Since ℐ (=) ⊆ ℐ (𝐸), 𝒱 𝑠 (𝑡 = 𝑢) ≠ 1/2. Thus, since
𝒱 𝑠 (𝜑[𝑥/𝑢] → 𝑡 = 𝑢) = 1/2, we obtain 𝒱 𝑠 (𝜑[𝑥/𝑢]) = 1/2 and 𝒱 𝑠 (𝑡 = 𝑢) = 0. Since 𝑡, 𝑢 ∈ ℐ (𝐸), 𝑡 ≠ 𝑢,
and 𝒱 𝑠 (𝜑[𝑥/𝑏]) = 0 for every 𝑡 ≠ 𝑏 ∈ ℐ (𝐸), we infer that 𝒱 𝑠 (𝜑[𝑥/𝑢]) = 0. But we already have that
𝒱 𝑠 (𝜑[𝑥/𝑢]) = 1/2. A contradiction.
3. Bisequent Calculi for NFL
form: Γ; Π ⇒ Σ; Δ. However we prefer to use for this aim bisequent calculus (BSC) which was already
Pavlović and Gratzl [19] formalise NFL by means of some nonstandard SC, where sequents are of the
applied as a uniform basis for arbitrary three-valued logics in [9]. Similar sequent system (but with a
pairs of sequents Γ ⇒ Δ ∣ Π ⇒ Σ, where Γ, Δ, Π, Σ are finite (possibly empty) multisets of formulae.
slightly different semantic interpretation) was applied also by Fjellstad [2, 3]. Bisequents are ordered
metavariables Γ, Δ, Π, Σ in both cases. 𝐵 and 𝑆 are used as metavariables for bisequents and sequents,
The correspondence of bisequents to nonstandard sequents from [19] is indicated by using the same
In both systems of NFL a bisequent Γ ⇒ Δ ∣ Π ⇒ Σ is axiomatic iff for some atomic formula 𝜑
respectively.
(including identities and 𝐸𝑡), either 𝜑 ∈ Γ ∩ Σ or 𝜑 ∈ Γ ∩ Δ or 𝜑 ∈ Π ∩ Σ. Moreover, bisequents of the form
𝐸𝑡1 , … , 𝐸𝑡𝑛 , Γ ⇒ Δ, 𝑃(𝑡1 , … , 𝑡𝑛 ) ∣ 𝑃(𝑡1 , … , 𝑡𝑛 ), Π ⇒ Σ are also axiomatic.
51
Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑 Γ ⇒ Δ ∣ 𝜑, Π ⇒ Σ
(¬⇒∣) (⇒¬ ∣)
¬𝜑, Γ ⇒ Δ ∣ Π ⇒ Σ Γ ⇒ Δ, ¬𝜑 ∣ Π ⇒ Σ
Γ ⇒ Δ, 𝜑 ∣ Π ⇒ Σ 𝜑, Γ ⇒ Δ ∣ Π ⇒ Σ
(∣ ¬⇒) (∣⇒¬)
Γ ⇒ Δ ∣ ¬𝜑, Π ⇒ Σ Γ ⇒ Δ ∣ Π ⇒ Σ, ¬𝜑
𝜑, 𝜓 , Γ ⇒ Δ ∣ 𝑆 Γ ⇒ Δ, 𝜑 ∣ 𝑆 Γ ⇒ Δ, 𝜓 ∣ 𝑆
(∧⇒∣) (⇒∧ ∣)
𝜑 ∧ 𝜓, Γ ⇒ Δ ∣ 𝑆 Γ ⇒ Δ, 𝜑 ∧ 𝜓 ∣ 𝑆
𝑆 ∣ 𝜑, 𝜓 , Γ ⇒ Δ 𝑆 ∣ Γ ⇒ Δ, 𝜑 𝑆 ∣ Γ ⇒ Δ, 𝜓
(∣ ∧⇒) (∣⇒∧)
𝑆 ∣ 𝜑 ∧ 𝜓, Γ ⇒ Δ 𝑆 ∣ Γ ⇒ Δ, 𝜑 ∧ 𝜓
Γ ⇒ Δ, 𝜓 ∣ 𝜑, Π ⇒ Σ 𝜑, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜓
(⇒→ ∣) (∣⇒→)
Γ ⇒ Δ, 𝜑 → 𝜓 ∣ Π ⇒ Σ Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑 → 𝜓
Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑 𝜓 , Γ ⇒ Δ ∣ Π ⇒ Σ
(→⇒ ∣)
𝜑 → 𝜓, Γ ⇒ Δ ∣ Π ⇒ Σ
Γ ⇒ Δ, 𝜑 ∣ Π ⇒ Σ Γ ⇒ Δ ∣ 𝜓 , Π ⇒ Σ
(∣→⇒)
Γ ⇒ Δ ∣ 𝜑 → 𝜓, Π ⇒ Σ
Figure 1: Rules of propositional K3
Γ ⇒ Δ ∣ 𝜑, 𝜓 , Π ⇒ Σ Γ ⇒ Δ, 𝜑 ∣ 𝜑, Π ⇒ Σ Γ ⇒ Δ, 𝜓 ∣ 𝜓 , Π ⇒ Σ
(∣ ∧𝑤 ⇒)
Γ ⇒ Δ ∣ 𝜑 ∧ 𝜓, Π ⇒ Σ
Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑, 𝜓 𝜑, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜓 𝜓 , Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑
(∣⇒∧𝑤 )
Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑 ∧ 𝜓
Γ ⇒ Δ, 𝜓 ∣ 𝜑, Π ⇒ Σ Γ ⇒ Δ, 𝜑 ∣ 𝜑, Π ⇒ Σ Γ ⇒ Δ, 𝜓 ∣ 𝜓 , Π ⇒ Σ
(⇒→𝑤 ∣)
Γ ⇒ Δ, 𝜑 → 𝜓 ∣ Π ⇒ Σ
𝜑, 𝜓 , Γ ⇒ Δ ∣ Π ⇒ Σ Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑, 𝜓 𝜓 , Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑
(→𝑤 ⇒ ∣)
𝜑 → 𝜓, Γ ⇒ Δ ∣ Π ⇒ Σ
Figure 2: Specific rules of propositional Kw
3
As follows from [9], propositional connectives of K3 are characterised by the rules from Fig. 1. The
propositional connectives of Kw 3 are mostly as in K3 , however in four cases we have three-premiss
rules given in Fig. 2. Fig. 3 contains the BSC rules for the universal quantifier as well as the existence
Note that the applications of (∀⇒∣) and (∣∀⇒) are restricted to parameters as instantiated terms, no
predicate in the spirit of the rules given in [19].
In negative FL a standard identity is replaced by its weaker variant with restricted reflexivity 𝐸𝑡 → 𝑡 = 𝑡.
DD are allowed as instantiated terms! It saves us from losing the subformula property.
In NFL we treat identity similarly so it behaves like other predicates and this is why the four rules for 𝐸
Notice that the rule (∣ ⇒ =), required for proving the Leibniz Principle, is like the rule from [4]. We
from Fig. 3 apply also to identities.
lose unrestricted subformula property but not in the essential way; in fact only terms 𝑠, 𝑡 and atoms
𝐴 are needed which are already present in the conclusion of this rule. It is of course possible to use
other rules, with smaller branching factor and satisfying the subformula property, to obtain the same
effect. However, in the presence of rules for DD with identities as principal formulas, it leads to serious
troubles with proving cut admissibility. On the other hand, this rule avoids the problems and allows
us to prove cut admissibility for reasonably small price. It is also possible to prepare a more refined
version of the calculus, like in [6], with the separation of rules for different kinds of identities, but this
leads to the proliferation of rules and, because of space restrictions, we present here a simpler form
easily provable since ∀𝑥𝜑, 𝐸𝑑 ⊢ 𝜑[𝑥/𝑑] holds.
of the calculus. A generalisation of quantifier rules to variants admitting DD as instantiated terms is
How BSC relates to the semantics from Section 2? Following [9, p. 331], we give the subsequent
52
𝐸𝑎, Γ ⇒ Δ, 𝜑[𝑥/𝑎] ∣ 𝑆 𝐸𝑎, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑[𝑥/𝑎]
(⇒∀ ∣) (∣⇒∀)
Γ ⇒ Δ, ∀𝑥𝜑 ∣ 𝑆 Γ ⇒ Δ ∣ Π ⇒ Σ, ∀𝑥𝜑
𝐸𝑏, ∀𝑥𝜑, 𝜑[𝑥/𝑏], Γ ⇒ Δ ∣ 𝑆 𝐸𝑏, Γ ⇒ Δ ∣ ∀𝑥𝜑, 𝜑[𝑥/𝑏], Π ⇒ Σ
(∀⇒∣) (∣∀⇒)
𝐸𝑏, ∀𝑥𝜑, Γ ⇒ Δ ∣ 𝑆 𝐸𝑏, Γ ⇒ Δ ∣ ∀𝑥𝜑, Π ⇒ Σ
𝐸𝑡, 𝑃[𝑡], Γ ⇒ Δ ∣ 𝑆 𝐸𝑡, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝑃[𝑡]
(𝐸⇒∣) (∣⇒𝐸)
𝑃[𝑡], Γ ⇒ Δ ∣ 𝑆 Γ ⇒ Δ ∣ Π ⇒ Σ, 𝑃[𝑡]
𝐸𝑡1 , … , 𝐸𝑡𝑛 , 𝑃(𝑡1 , … , 𝑡𝑛 ), Γ ⇒ Δ ∣ Π ⇒ Σ 𝐸𝑡, Γ ⇒ Δ ∣ Π ⇒ Σ
(∣𝐸⇒) (𝐸𝑇 𝑟1 )
𝐸𝑡1 , … , 𝐸𝑡𝑛 , Γ ⇒ Δ ∣ 𝑃(𝑡1 , … , 𝑡𝑛 ), Π ⇒ Σ Γ ⇒ Δ ∣ 𝐸𝑡, Π ⇒ Σ
𝐸𝑡1 , … , 𝐸𝑡𝑛 , Γ ⇒ Δ ∣ Π ⇒ Σ, 𝑃(𝑡1 , … , 𝑡𝑛 ) Γ ⇒ Δ ∣ Π ⇒ Σ, 𝐸𝑡
(⇒𝐸∣) (𝐸𝑇 𝑟2 )
𝐸𝑡1 , … , 𝐸𝑡𝑛 , Γ ⇒ Δ, 𝑃(𝑡1 , … , 𝑡𝑛 ) ∣ Π ⇒ Σ Γ ⇒ Δ, 𝐸𝑡 ∣ Π ⇒ Σ
where 𝑎 is fresh and 𝑏, 𝑏𝑖 are arbitrary parameters. Both 𝑃[𝑡] and 𝑃(𝑡1 , … , 𝑡𝑛 ) denote atoms or identities but not
𝐸𝑡, moreover identities of the form 𝑏 = 𝑑 are excluded since they are governed by rules from figure 5. In 𝑃[𝑡]
there is at least one occurrence of 𝑡 and there may be other terms; in 𝑃(𝑡1 , … , 𝑡𝑛 ) there are no other terms.
Figure 3: Rules for universal quantifier and existence predicate
Γ ⇒ Δ ∣ Π ⇒ Σ, 𝑡 ≈ 𝑠 Γ ⇒ Δ ∣ Π ⇒ Σ, 𝐴[𝑥/𝑡] 𝐴[𝑥/𝑠], Γ ⇒ Δ ∣ Π ⇒ Σ
(∣ ⇒ =)
Γ⇒Δ∣Π⇒Σ
𝑡 = 𝑡, 𝐸𝑡, Γ ⇒ Δ ∣ Π ⇒ Σ 𝑎 = 𝑑, 𝐸𝑑, Γ ⇒ Δ ∣ Π ⇒ Σ
(= ⇒ ∣) (𝐸𝚤⇒ ∣)
𝐸𝑡, Γ ⇒ Δ ∣ Π ⇒ Σ 𝐸𝑑, Γ ⇒ Δ ∣ Π ⇒ Σ
where 𝐴[𝑥/𝑡] is an atom, or identity or 𝐸𝑡, 𝑡 ≈ 𝑠 denotes either 𝑡 = 𝑠 or 𝑠 = 𝑡, 𝑎 is a fresh parameter and 𝑑 is an
arbitrary description.
Figure 4: Rules for identity
𝜑[𝑥/𝑐], 𝑐 = 𝚤𝑥𝜑, 𝐸𝑐, Γ ⇒ Δ ∣ 𝑆 𝐸𝑐, Γ ⇒ Δ ∣ 𝜑[𝑥/𝑐], 𝑐 = 𝚤𝑥𝜑, Π ⇒ Σ
(𝚤 ⇒∣ 1) (∣ 𝚤 ⇒ 1)
𝑐 = 𝚤𝑥𝜑, 𝐸𝑐, Γ ⇒ Δ ∣ 𝑆 𝐸𝑐, Γ ⇒ Δ ∣ 𝑐 = 𝚤𝑥𝜑, Π ⇒ Σ
𝑐 = 𝚤𝑥𝜑, 𝐸𝑏, 𝐸𝑐, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑[𝑥/𝑏] 𝑏 = 𝑐, 𝑐 = 𝚤𝑥𝜑, 𝐸𝑏, 𝐸𝑐, Γ ⇒ Δ ∣ Π ⇒ Σ
(𝚤 ⇒∣ 2)
𝑐 = 𝚤𝑥𝜑, 𝐸𝑏, 𝐸𝑐, Γ ⇒ Δ ∣ Π ⇒ Σ
𝐸𝑏, 𝐸𝑐, Γ ⇒ Δ, 𝜑[𝑥/𝑏] ∣ 𝑐 = 𝚤𝑥𝜑, Π ⇒ Σ 𝐸𝑏, 𝐸𝑐, Γ ⇒ Δ ∣ 𝑏 = 𝑐, 𝑐 = 𝚤𝑥𝜑, Π ⇒ Σ
(∣ 𝚤 ⇒ 2)
𝐸𝑏, 𝐸𝑐, Γ ⇒ Δ ∣ 𝑐 = 𝚤𝑥𝜑, Π ⇒ Σ
𝐸𝑐, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑[𝑥/𝑐] 𝐸𝑎, 𝐸𝑐, 𝜑[𝑥/𝑎], Γ ⇒ Δ ∣ Π ⇒ Σ, 𝑎 = 𝑐
(∣⇒ 𝚤)
𝐸𝑐, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝑐 = 𝚤𝑥𝜑,
𝐸𝑐, Γ ⇒ Δ, 𝜑[𝑥/𝑐] ∣ Π ⇒ Σ 𝐸𝑎, 𝐸𝑐, Γ ⇒ Δ, 𝑎 = 𝑐 ∣ 𝜑[𝑥/𝑎], Π ⇒ Σ
(⇒ 𝚤 ∣)
𝐸𝑐, Γ ⇒ Δ, 𝑐 = 𝚤𝑥𝜑 ∣ Π ⇒ Σ
where 𝑎 is a fresh parameter.
Figure 5: Rules for DD
definition.
Definition 3.1. ⊧ Γ ⇒ Δ ∣ Π ⇒ Σ iff every valuation 𝒱 satisfies Γ ⇒ Δ ∣ Π ⇒ Σ. The latter holds for 𝒱 iff
for some 𝜑: either (𝜑 ∈ Γ and 𝒱 (𝜑) ≠ 1) or (𝜑 ∈ Δ and 𝒱 (𝜑) = 1) or (𝜑 ∈ Π and 𝒱 (𝜑) = 0) or (𝜑 ∈ Σ and
𝒱 (𝜑) ≠ 0). Clearly ⊧Γ̸ ⇒ Δ ∣ Π ⇒ Σ iff for some 𝒱, all elements of Γ are true, all elements of Δ are either
false or undefined, all elements of Π are either true or undefined and all elements of Σ are false. In this case
we say that 𝒱 falsifies this sequent.
53
As follows from [9], all axiomatic bisequents are valid and all the rules for connectives are both sound
(validity-preserving) and invertible. The same holds for the rules from Fig. 3 as follows from [19]. It
may be extended to the new rules from Fig. 4 and 5, hence it holds:
Theorem 3.1 (Soundness). For any bisequent 𝐵, if ⊢ 𝐵, then ⊧ 𝐵.
example, let us illustrate soundness of the rule (∣⇒ 𝚤). The proof holds both for K3 and Kw
Proof. By induction of the height of the derivation, using the fact that all the rules are sound. As an
𝑎 is fresh.
3 . Recall that
(1) Suppose that ⊧ 𝐸𝑐, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑[𝑥/𝑐].
(2) Thus, for any valuation 𝒱, 𝒱 (𝐸𝑐) ≠ 1, or for some 𝛾 ∈ Γ, 𝒱 (𝛾 ) ≠ 1, or for some 𝛿 ∈ Δ, 𝒱 (𝛿) = 1,
or for some 𝜋 ∈ Π, 𝒱 (𝜋) = 0, or for some 𝜎 ∈ Σ, 𝒱 (𝜎 ) ≠ 0, or 𝒱 (𝜑[𝑥/𝑐]) ≠ 0.
(3) Suppose that ⊧ 𝐸𝑎, 𝜑[𝑥/𝑎], 𝐸𝑐, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝑎 = 𝑐.
(4) Hence, for any valuation 𝒱, 𝒱 (𝐸𝑎) ≠ 1, or 𝒱 (𝜑[𝑥/𝑎]) ≠ 1, or 𝒱 (𝐸𝑐) ≠ 1, or for some 𝛾 ∈ Γ,
𝒱 (𝛾 ) ≠ 1, or for some 𝛿 ∈ Δ, 𝒱 (𝛿) = 1, or for some 𝜋 ∈ Π, 𝒱 (𝜋) = 0, or for some 𝜎 ∈ Σ, 𝒱 (𝜎 ) ≠ 0,
or 𝒱 (𝑎 = 𝑐) ≠ 0.
(5) ⊧𝐸𝑐,
̸ Γ ⇒ Δ ∣ Π ⇒ Σ, 𝑐 = 𝚤𝑥𝜑.
(6) Therefore, there is a valuation 𝒱 such that 𝒱 (𝐸𝑐) = 1, for any 𝛾 ∈ Γ, 𝒱 (𝛾 ) = 1, for any 𝛿 ∈ Δ,
𝒱 (𝛿) ≠ 1, for any 𝜋 ∈ Π, 𝒱 (𝜋) ≠ 0, and for any 𝜎 ∈ Σ, 𝒱 (𝜎 ) = 0, 𝒱 (𝑐 = 𝚤𝑥𝜑) = 0.
(7) Then we obtain:
a) 𝒱 (𝜑[𝑥/𝑐]) ≠ 0,
b) 𝒱 (𝐸𝑎) ≠ 1, or 𝒱 (𝜑[𝑥/𝑎]) ≠ 1, or 𝒱 (𝑎 = 𝑐) ≠ 0,
c) 𝒱 (𝐸𝑐) = 1, 𝒱 (𝑐 = 𝚤𝑥𝜑) = 0.
(8) By the properties of ℐ (=), we have 𝑐, 𝚤𝑥𝜑 ∈ ℐ (𝐸).
(9) ℐ (𝚤𝑥𝜑) ≠ 𝑐, that is 𝒱 (𝜑[𝑥/𝑐]) ≠ 1 or 𝒱 (𝜑[𝑥/𝑏]) ≠ 0, for some 𝑐 ≠ 𝑏 ∈ ℐ (𝐸).
(10) Since 𝑎 is fresh, 𝒱 (𝜑[𝑥/𝑐]) ≠ 1 or (𝒱 (𝜑[𝑥/𝑎]) ≠ 0 and 𝑐 ≠ 𝑎 ∈ ℐ (𝐸)).
(11) Suppose that 𝒱 (𝜑[𝑥/𝑐]) ≠ 1. Thus, 𝒱 (𝜑[𝑥/𝑐]) = 1/2, since also 𝒱 (𝜑[𝑥/𝑐]) ≠ 0. Since 𝑐 ∈ ℐ (𝐸),
𝒱 (𝜑[𝑥/𝑐]) ≠ 1/2. Contradiction.
(12) Suppose that 𝒱 (𝜑[𝑥/𝑎]) ≠ 0 and 𝑐 ≠ 𝑎 ∈ ℐ (𝐸).
(13) Thus, 𝒱 (𝐸𝑎) = 1 and 𝒱 (𝑎 = 𝑐) ≠ 1.
(14) Hence, 𝒱 (𝜑[𝑥/𝑎]) ≠ 1 or 𝒱 (𝑎 = 𝑐) ≠ 0.
(15) If 𝒱 (𝜑[𝑥/𝑎]) ≠ 1, then 𝒱 (𝜑[𝑥/𝑎]) = 1/2, since 𝒱 (𝜑[𝑥/𝑎]) ≠ 0. Since 𝑎 ∈ ℐ (𝐸), 𝒱 (𝜑[𝑥/𝑎]) ≠ 1/2.
(16) If 𝒱 (𝑎 = 𝑐) ≠ 0, then 𝒱 (𝑎 = 𝑐) = 1/2, since 𝒱 (𝑎 = 𝑐) ≠ 1. However, 𝒱 (𝑎 = 𝑐) ≠ 1/2, because
Contradiction.
𝑎, 𝑐 ∈ ℐ (𝐸). Contradiction.
(17) Contradiction. Thus, ⊧ 𝐸𝑐, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝑐 = 𝚤𝑥𝜑.
In fact, for the NFL without DD and identity, as defined by rules from Fig. 1, 2, 3, also completeness
was proved in [19], and it may be extended in a straightforward way to cover identity, as was done for
negative FL in [18]. For DD we already demonstrated that (𝐿) is valid, so we restrict our considerations
of adequacy to show that in (complete) BSC for NFL without DD we can prove interderivability of our
rules for DD with both forms of (𝐿).
To do that we must restrict our general notion of provability in BSC. Although we defined satisifability
and validity for arbitrary bisequents, in fact we are interested in the narrower notion of BSC proof,
bisequents shows that the entailment between Γ and 𝜑 is expressed in BSC as provability of Γ ⇒ 𝜑 ∣ ⇒.
related to definition of consequence relation, as defined in Section 2. The definition of validity for
Moreover, although in propositional Kleene’s logic the set of validities is empty it is not so in the
first-order NFL based on it. In particular, both forms of (𝐿) are valid and will be shown provable.
To save space in the proofs we will usually omit repetitions of formulae which are still active in
premisses, according to rule schema, but which are not essential for the proof in question. The following
three results hold:
54
Lemma 3.1 (Substitution). If ⊢𝑛 Γ ⇒ Δ ∣ Θ ⇒ Λ is derivable (where 𝑛 denotes derivability with height
bounded by 𝑛), then the sequent ⊢𝑛 Γ[𝑏/𝑐] ⇒ Δ[𝑏/𝑐] ∣ Θ[𝑏/𝑐] ⇒ Λ[𝑏/𝑐] is likewise derivable.
Proof. Similar to the proof in [19]. Note that it is restricted to parameters.
Lemma 3.2. ⊢ 𝐸𝑡1 , … , 𝐸𝑡𝑛 , Γ ⇒ Δ, 𝜑(𝑡1 , … , 𝑡𝑛 ) ∣ 𝜑(𝑡1 , … , 𝑡𝑛 ), Π ⇒ Σ, where 𝑡1 , … , 𝑡𝑛 are all terms occuring in
𝜑
Proof. By induction on the complexity of 𝜑.
Lemma 3.3 (Leibniz Law). For any formula 𝜑, it holds that ⊢ 𝑡1 = 𝑡2 , 𝜑[𝑥/𝑡1 ] ⇒ 𝜑[𝑥/𝑡2 ] ∣ 𝑆.
Proof. By induction on the complexity of 𝜑.
The proof of (𝐿← ) in strong Kleene logic is as follows, where (𝐸) stands for provable 𝐸𝑎 ⇒ 𝜑[𝑥/𝑎] ∣
𝜑[𝑥/𝑎] ⇒:
𝐸𝑏 ⇒ 𝜑[𝑥/𝑏] ∣ 𝜑[𝑥/𝑏] ⇒ 𝐸𝑎, 𝐸𝑏 ⇒ 𝑎 = 𝑏 ∣ 𝑎 = 𝑏 ⇒
(∣→⇒)
𝐸𝑎, 𝐸𝑏 ⇒ 𝑎 = 𝑏 ∣ 𝜑[𝑥/𝑏], 𝜑[𝑥/𝑏] → 𝑎 = 𝑏 ⇒
(∣ ∀ ⇒)
𝐸𝑎, 𝐸𝑏 ⇒ 𝑎 = 𝑏 ∣ 𝜑[𝑥/𝑏], ∀𝑥(𝜑 → 𝑎 = 𝑥) ⇒
(⇒ 𝚤 ∣)
(𝐸)
𝐸𝑎 ⇒ 𝑎 = 𝚤𝑥𝜑 ∣ 𝜑[𝑥/𝑎], ∀𝑥(𝜑 → 𝑎 = 𝑥) ⇒
(∣ ∧ ⇒)
𝐸𝑎 ⇒ 𝑎 = 𝚤𝑥𝜑 ∣ 𝜑[𝑥/𝑎] ∧ ∀𝑥(𝜑 → 𝑎 = 𝑥) ⇒
(⇒→∣)
𝐸𝑎 ⇒ 𝜑[𝑥/𝑎] ∧ ∀𝑥(𝜑 → 𝑎 = 𝑥) → 𝑎 = 𝚤𝑥𝜑 ∣⇒
(⇒ ∀ ∣)
⇒ ∀𝑦(𝜑[𝑥/𝑦] ∧ ∀𝑥(𝜑 → 𝑦 = 𝑥) → 𝑦 = 𝚤𝑥𝜑) ∣⇒
For (𝐿→ ) let (𝐸 ′ ) stand for the following proof:
𝐸𝑎 ⇒ 𝜑[𝑥/𝑎] ∣ 𝜑[𝑥/𝑎] ⇒
(∣ 𝚤 ⇒ 1)
𝐸𝑎 ⇒ 𝜑[𝑥/𝑎] ∣ 𝑎 = 𝚤𝑥𝜑 ⇒
Then:
𝐸𝑏 ⇒ 𝜑[𝑥/𝑏] ∣ 𝜑[𝑥/𝑏] ⇒ 𝐸𝑎, 𝐸𝑏 ⇒ 𝑎 = 𝑏 ∣ 𝑎 = 𝑏 ⇒
(∣ 𝚤 ⇒ 2)
𝐸𝑎, 𝐸𝑏 ⇒ 𝑎 = 𝑏 ∣ 𝜑[𝑥/𝑏], 𝑎 = 𝚤𝑥𝜑 ⇒
(⇒→∣)
𝐸𝑎, 𝐸𝑏 ⇒ 𝜑[𝑥/𝑏] → 𝑎 = 𝑏 ∣ 𝑎 = 𝚤𝑥𝜑 ⇒
(⇒ ∀ ∣)
𝐸𝑎 ⇒ ∀𝑥(𝜑 → 𝑎 = 𝑥) ∣ 𝑎 = 𝚤𝑥𝜑 ⇒
(⇒ ∧ ∣)
(𝐸 ′ )
𝐸𝑎 ⇒ 𝜑[𝑥/𝑎] ∧ ∀𝑥(𝜑 → 𝑎 = 𝑥) ∣ 𝑎 = 𝚤𝑥𝜑 ⇒
(⇒→∣)
𝐸𝑎 ⇒ 𝑎 = 𝚤𝑥𝜑 → 𝜑[𝑥/𝑎] ∧ ∀𝑥(𝜑 → 𝑎 = 𝑥) ∣⇒
(⇒ ∀ ∣)
⇒ ∀𝑦(𝑦 = 𝚤𝑥𝜑 → 𝜑[𝑥/𝑦] ∧ ∀𝑥(𝜑 → 𝑦 = 𝑥)) ∣⇒
Proofs in BSC for weak Kleene’s logic are more complex since the applications of (⇒→∣) and (∣ ∧ ⇒)
form 𝐸𝑎, Γ ⇒ Δ, 𝜓 (𝑎) ∣ 𝜓 (𝑎), Π ⇒ Σ or 𝐸𝑎, 𝐸𝑏, Γ ⇒ Δ, 𝜓 (𝑎, 𝑏) ∣ 𝜓 (𝑎, 𝑏), Π ⇒ Σ which are provable.
introduce additional premisses. However, in all respective premisses we obtain simply sequents of the
proved admissible in the next section. Here is an example. From both premisses of (⇒ 𝚤 ∣) we obtain:
All rules for DD are derivable if we use (𝐿→ ) or (𝐿← ) as additional axioms and use cuts which will be
𝐸𝑐, 𝐸𝑎, Γ ⇒ Δ, 𝑐 = 𝑎 ∣ 𝜑[𝑥/𝑎], Π ⇒ Σ
(⇒→∣)
𝐸𝑐, 𝐸𝑎, Γ ⇒ Δ, 𝜑[𝑥/𝑎] → 𝑐 = 𝑎 ∣ Π ⇒ Σ
(⇒ ∀ ∣)
𝐸𝑐, Γ ⇒ Δ, 𝜑[𝑥/𝑐] ∣ Π ⇒ Σ 𝐸𝑐, Γ ⇒ Δ, ∀𝑥(𝜑 → 𝑐 = 𝑥) ∣ Π ⇒ Σ
(∣⇒ ∧)
𝐸𝑐, Γ ⇒ Δ, 𝜑[𝑥/𝑐] ∧ ∀𝑥(𝜑 → 𝑐 = 𝑥) ∣ Π ⇒ Σ
which by cut with 𝐸𝑐, 𝜑[𝑥/𝑐] ∧ ∀𝑥(𝜑 → 𝑐 = 𝑥) ⇒ 𝑐 = 𝚤𝑥𝜑 ∣⇒ yields the conclusion of (⇒ 𝚤 ∣). The
latter bisequent is proved by cuts on the axiomatic sequent (𝐿← ) i.e. ⇒ ∀𝑦(𝜑[𝑥/𝑦] ∧ ∀𝑥(𝜑 → 𝑦 = 𝑥) →
𝑦 = 𝚤𝑥𝜑) ∣⇒ with 𝐸𝑐, ∀𝑦(𝜑[𝑥/𝑦] ∧ ∀𝑥(𝜑 → 𝑦 = 𝑥) → 𝑦 = 𝚤𝑥𝜑) ⇒ 𝜑[𝑥/𝑐] ∧ ∀𝑥(𝜑 → 𝑐 = 𝑥) → 𝑐 = 𝚤𝑥𝜑 ∣⇒
and 𝜑[𝑥/𝑐] ∧ ∀𝑥(𝜑 → 𝑐 = 𝑥) → 𝑐 = 𝚤𝑥𝜑), 𝜑[𝑥/𝑐] ∧ ∀𝑥(𝜑 → 𝑐 = 𝑥) ⇒ 𝑐 = 𝚤𝑥𝜑 ∣⇒ which are easily
provable.
55
Γ⇒Δ∣𝑆 Γ⇒Δ∣𝑆 𝑆∣Π⇒Σ 𝑆∣Π⇒Σ
(𝑊⇒∣) (⇒𝑊 ∣) (∣ 𝑊⇒) (∣⇒𝑊 )
𝜑, Γ ⇒ Δ ∣ 𝑆 Γ ⇒ Δ, 𝜑 ∣ 𝑆 𝑆 ∣ 𝜑, Π ⇒ Σ 𝑆 ∣ Π ⇒ Σ, 𝜑
𝜑, 𝜑, Γ ⇒ Δ ∣ 𝑆 Γ ⇒ Δ, 𝜑, 𝜑 ∣ 𝑆 𝑆 ∣ 𝜑, 𝜑, Π ⇒ Σ 𝑆 ∣ Π ⇒ Σ, 𝜑, 𝜑
(𝐶⇒∣) (⇒𝐶 ∣) (∣ 𝐶⇒) (∣⇒𝐶)
𝜑, Γ ⇒ Δ ∣ 𝑆 Γ ⇒ Δ, 𝜑 ∣ 𝑆 𝑆 ∣ 𝜑, Π ⇒ Σ 𝑆 ∣ Π ⇒ Σ, 𝜑
Figure 6: Admissible structural rules
4. Cut Admissibility
In order to show that BSC is cut-free we need to prove the following results:
Lemma 4.1 (Generalisation of axioms). For any formula 𝜑, the following bisequents are derivable:
(1) 𝜑, Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑,
(2) 𝜑, Γ ⇒ Δ, 𝜑 ∣ Π ⇒ Σ,
(3) Γ ⇒ Δ ∣ 𝜑, Π ⇒ Σ, 𝜑.
(4) 𝐸𝑡1 , … , 𝐸𝑡𝑛 , Γ ⇒ Δ, 𝜑[𝑡1 , … , 𝑡𝑛 ] ∣ 𝜑[𝑡1 , … , 𝑡𝑛 ], Π ⇒ Σ.
Proof. By induction on the complexity of 𝜑.
Here we present proofs of the admissibility of cut with all forms of cuts from [19]. But first we
demonstrate the admissibility of structural rules, like in [19].
Lemma 4.2 (Admissibility of structural rules). Structural rules from Fig. 6 are height-preserving admissible.
Proof. By induction on the height of the derivation.
In fact, the proof of admissibility of contraction presupposes the following:
Lemma 4.3 (Invertibility). All the rules of the bisequent calculi in question are height-preserving invertible.
Proof. By induction on the height of the derivation, using Lemma 3.1.
We also need the following:
Lemma 4.4 (Transfer). The following rules are height-preserving admissible:
Γ ⇒ Δ ∣ 𝜑, Π ⇒ Σ Γ ⇒ Δ, 𝜑 ∣ Π ⇒ Σ
(𝐿𝑇 𝑟) (𝑅𝑇 𝑟)
𝜑, Γ ⇒ Δ ∣ Π ⇒ Σ Γ ⇒ Δ ∣ Π ⇒ Σ, 𝜑
Proof. Straightforward extension of the proof by induction on the height of the derivation from [19].
In bisequent framework, we have several cut rules1 listed in Fig. 7.
Theorem 4.1 (Cut admissibility). The rules (E-Cut), (L-Cut), (O-Cut), (I-Cut), (R-Cut), (3-Cut) are admissi-
ble.
Proof. Admissibility of (𝐸 − 𝐶𝑢𝑡) and (𝐿 − 𝐶𝑢𝑡) is proved first in [19], and their proof applies to our
system with no changes. The remaining variants of cut are proved in [19] simultaneously, by double
induction on the complexity of the cut formula and on the height of the cut (the sum of heights of
premises of cut). The extension of their proof to cover our rules is in some cases straightforward so we
consider only the most complex situation with triple cut:
Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1 , 𝑐 = 𝚤𝑥𝜑 𝑐 = 𝚤𝑥𝜑, Γ2 ⇒ Δ2 ∣ Λ2 ⇒ Θ2 𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
1
Notice that we considered just two cut rules on the propositional level [9]. However, the first-order case requires more
options, which are actually the same as Pavlović and Gratzl have [19]. They follow the strategy of Fjellstad [3] in this respect.
56
Γ ⇒ Δ ∣ Λ ⇒ Θ, 𝐸𝑡 𝐸𝑡, Π ⇒ Σ ∣ Ξ ⇒ Ω
(E-Cut)
Γ, Π ⇒ Δ, Σ ∣ Λ, Ξ ⇒ Θ, Ω
𝐸𝑡1 , … , 𝐸𝑡𝑛 , Γ ⇒ Δ ∣ Λ ⇒ Θ, 𝑃(𝑡1 , … , 𝑡𝑛 ) 𝐸𝑡1 , … , 𝐸𝑡𝑛 , 𝑃(𝑡1 , … , 𝑡𝑛 ), Π ⇒ Σ ∣ Ξ ⇒ Ω
(L-Cut)
𝐸𝑡1 , … , 𝐸𝑡𝑛 Γ, Π ⇒ Δ, Σ ∣ Λ, Ξ ⇒ Θ, Ω
Γ ⇒ Δ, 𝜑 ∣ Λ ⇒ Θ 𝜑, Π ⇒ Σ ∣ Ξ ⇒ Ω
(O-Cut)
Γ, Π ⇒ Δ, Σ ∣ Λ, Ξ ⇒ Θ, Ω
Γ ⇒ Δ ∣ Λ ⇒ Θ, 𝜑 Π ⇒ Σ ∣ 𝜑, Ξ ⇒ Ω
(I-Cut)
Γ, Π ⇒ Δ, Σ ∣ Λ, Ξ ⇒ Θ, Ω
Γ ⇒ Δ ∣ 𝜑, Λ ⇒ Θ Π ⇒ Σ, 𝜑 ∣ Ξ ⇒ Ω
(R-Cut)
Γ, Π ⇒ Δ, Σ ∣ Λ, Ξ ⇒ Θ, Ω
𝜑, Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1 Γ2 ⇒ Δ2 ∣ Λ2 ⇒ Θ2 , 𝜑 Γ3 ⇒ Δ3 , 𝜑 ∣ 𝜑, Λ3 ⇒ Θ3
(3-Cut)
Γ1 , Γ 2 , Γ 3 ⇒ Δ 1 , Δ 2 , Δ 3 ∣ Λ 1 , Λ 2 , Λ 3 ⇒ Θ 1 , Θ 2 , Θ 3
Figure 7: Cut rules
for simplicity let us refer to the premisses of this cut as 𝑃𝑙 , 𝑃𝑚 , 𝑃𝑟 . Since the middle premiss 𝑃𝑚 may
be derived either by (𝚤 ⇒∣ 1) or (𝚤 ⇒∣ 2) and the rightmost premiss 𝑃𝑟 may be derived either by (⇒ 𝚤 ∣)
(on the left identity) or (∣ 𝚤 ⇒ 1) or (∣ 𝚤 ⇒ 2) (on the right identity) we have six subcases in total. The
leftmost premiss 𝑃𝑙 is derivable only by (∣⇒ 𝚤) hence we have always:
𝐷1 𝐷2
Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1 , 𝜑[𝑥/𝑐] 𝐸𝑎, 𝜑[𝑥/𝑎], Γ1 ⇒ Δ1 , ∣ Λ1 ⇒ Θ1 , 𝑐 = 𝑎
(∣⇒ 𝚤)
Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1 , 𝑐 = 𝚤𝑥𝜑
1. and let the middle premiss be derived as follows:
𝐷3
𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑐], Γ2 ⇒ Δ2 , ∣ Λ2 ⇒ Θ2
(𝚤 ⇒∣)
𝑐 = 𝚤𝑥𝜑, Γ2 ⇒ Δ2 ∣ Λ2 ⇒ Θ2
1.1. and the rightmost one:
𝐷4
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑐], Λ3 ⇒ Θ3
(∣ 𝚤 ⇒ 1)
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
let 𝐴1 stands for the following:
𝐷1
Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1 , 𝜑[𝑥/𝑐]
we transform the proof as follows:
𝐷4
𝑃𝑙 𝑃𝑚 𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑐], Λ3 ⇒ Θ3
𝐴1 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ 𝜑[𝑥/𝑐], Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
(3-Cut)
𝐸𝑐, Γ1 , Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ1 Δ2 , Δ3 ∣ Λ1 , Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ1 , Θ2 , Θ3
(I-Cut)
(𝐶)
𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
where (3 − 𝐶𝑢𝑡) is admissible by induction on the height and (𝐼 − 𝐶𝑢𝑡) by induction on the degree.
1.2. 𝑃𝑟 is derived as follows:
𝐴2 𝐴3
(∣ 𝚤 ⇒ 2)
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
where 𝐴2 stands for
57
𝐷4
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑏] ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
and 𝐴3 stands for
𝐷5
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, 𝑐 = 𝑏, Λ3 ⇒ Θ3
note that also 𝐸𝑏 must occur in Γ3 . We perform:
(3 − 𝐶𝑢𝑡) on 𝑃𝑙 , 𝑃𝑚 and 𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑏] ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3 yield 𝑆4 ∶= 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒
Δ1 , Δ2 , Δ3 , 𝜑[𝑥/𝑏] ∣ Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
(3 − 𝐶𝑢𝑡) on 𝑃𝑙 , 𝑃𝑚 and 𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, 𝑐 = 𝑏, Λ3 ⇒ Θ3 yield 𝑆5 ∶= 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒
Δ1 , Δ2 , Δ3 , ∣ 𝑐 = 𝑏, Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
both cuts are admissible by induction on the height. By substitution lemma on 𝐷2 we obtain a proof
of 𝑆2 ∶= 𝐸𝑏, 𝜑[𝑥/𝑏], Γ1 ⇒ Δ1 , ∣ Λ1 ⇒ Θ1 , 𝑐 = 𝑏. We finish with:
𝑆4 𝑆2
𝑆5 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ 𝑐 = 𝑏, Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
(O-Cut)(𝐶)
𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
(I-Cut)(𝐶)
1.3. 𝑃𝑟 is derived as follows:
where both cuts are admissible by induction on the degree.
𝐴4 𝐴5
(⇒ 𝚤 ∣)
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
where 𝐴4 stands for
𝐷4
𝐸𝑐, Γ3 ⇒ Δ3 , 𝜑[𝑥/𝑐] ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
and 𝐴5 stands for
𝐷5
𝐸𝑎′ , 𝐸𝑐, Γ 3 ⇒ Δ3 , 𝑐 = 𝑎 ∣ 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑎 ], Λ3 ⇒ Θ3
′ ′
where 𝑎′ is eigenvariable different from 𝑎. We perform:
𝐷4
Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1 , 𝑐 = 𝚤𝑥𝜑 𝐸𝑐, Γ3 ⇒ Δ3 , 𝜑[𝑥/𝑐] ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
𝐸𝑐, Γ1 , Γ3 ⇒ Δ1 , Δ3 , 𝜑[𝑥/𝑐] ∣ Λ1 , Λ3 ⇒ Θ1 , Θ3
(I-Cut)
and
Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1 , 𝑐 = 𝚤𝑥𝜑 𝐴6 𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
𝐸𝑐, 𝜑[𝑥/𝑐], Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3 (3 − 𝐶𝑢𝑡)
where 𝐴6 stands for
𝐷3
𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑐], Γ2 ⇒ Δ2 , ∣ Λ2 ⇒ Θ2
Both cuts are admissible by induction on the height and the resulting sequents by (𝑂 − 𝐶𝑢𝑡) lead to
desired result.
2. Now let the middle premiss be derived as follows:
𝐴7 𝐴8
(𝚤 ⇒∣)
𝐸𝑏, 𝑐 = 𝚤𝑥𝜑, Γ2 ⇒ Δ2 ∣ Λ2 ⇒ Θ2
where 𝐴7 stands for
58
𝐷3
𝐸𝑏, 𝑐 = 𝚤𝑥𝜑, Γ2 ⇒ Δ2 ∣ Λ2 ⇒ Θ2 , 𝜑[𝑥/𝑏]
and 𝐴8 stands for
𝐷4
𝐸𝑏, 𝑐 = 𝑏, 𝑐 = 𝚤𝑥𝜑, Γ2 ⇒ Δ2 ∣ Λ2 ⇒ Θ2
2.1. and the right premiss by:
𝐷5
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑐], Λ3 ⇒ Θ3
(∣ 𝚤 ⇒ 1)
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
and the sequent resulting by (3 − 𝐶𝑢𝑡) is:
𝐸𝑏, 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
we transform the proof as follows:
𝐷5
𝑃𝑙 𝑃𝑚 𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑐], Λ3 ⇒ Θ3
𝐴9 𝐸𝑏, 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ 𝜑[𝑥/𝑐], Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
(3-Cut)
𝐸𝑏, 𝐸𝑐, Γ1 , Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ1 Δ2 , Δ3 ∣ Λ1 , Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ1 , Θ2 , Θ3
(I-Cut)
(𝐶)
𝐸𝑏, 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
where 𝐴9 stands for
𝐷1
Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1 , 𝜑[𝑥/𝑐]
2.2. If the right premiss is derived:
𝐴10 𝐴11
(∣ 𝚤 ⇒ 2)
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
where 𝐴10 stands for
𝐷5
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑏 ′ ] ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
where 𝐴11 stands for
𝐷6
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, 𝑐 = 𝑏 ′ , Λ3 ⇒ Θ3
note that also 𝐸𝑏 ′ must occur in Γ3 (𝑏 ′ distinct from 𝑏).
(3 − 𝐶𝑢𝑡) on 𝑃𝑙 , 𝑃𝑚 and 𝐷5 yields 𝑆7 ∶= 𝐸𝑏, 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 , 𝜑[𝑥/𝑏 ′ ] ∣ Λ1 , Λ2 , Λ3 ⇒
Θ1 , Θ2 , Θ3
(3 − 𝐶𝑢𝑡) on 𝑃𝑙 , 𝑃𝑚 and 𝐷6 yields 𝑆8 ∶= 𝐸𝑏, 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ 𝑐 = 𝑏 ′ , Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
By substitution lemma on 𝐷2 we get 𝑆9 ∶= 𝐸𝑏 ′ , 𝜑[𝑥/𝑏 ′ ], Γ1 ⇒ Δ1 , ∣ Λ1 ⇒ Θ1 , 𝑐 = 𝑏 ′
with cuts admissible by induction on the height.
(𝐼 − 𝐶𝑢𝑡) and (𝑂 − 𝐶𝑢𝑡) made on these three sequents yield the desired result.
2.3. Finally let the right premiss be obtained by:
𝐴12 𝐴13
(⇒ 𝚤 ∣)
𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝚤𝑥𝜑 ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
where 𝐴12 stands for
𝐷5
𝐸𝑐, Γ3 ⇒ Δ3 , 𝜑[𝑥/𝑐] ∣ 𝑐 = 𝚤𝑥𝜑, Λ3 ⇒ Θ3
59
and 𝐴13 stands for
𝐷6
𝐸𝑎′ , 𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝑎′ ∣ 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑎′ ], Λ3 ⇒ Θ3
where 𝑎′ is eigenvariable different from 𝑎.
By substitution lemma on 𝐷6 we get 𝑆 ∶= 𝐸𝑏, 𝐸𝑐, Γ3 ⇒ Δ3 , 𝑐 = 𝑏 ∣ 𝑐 = 𝚤𝑥𝜑, 𝜑[𝑥/𝑏], Λ3 ⇒ Θ3 (the proof
has the same height). 𝑆 by (𝐼 − 𝐶𝑢𝑡) with 𝑃𝑙 gives 𝑆1 ∶= 𝐸𝑏, 𝐸𝑐, Γ1 , Γ3 ⇒ Δ1 , Δ3 , 𝑐 = 𝑏 ∣ 𝜑[𝑥/𝑏], Λ1 Λ3 ⇒
Θ1 , Θ3
(3 − 𝐶𝑢𝑡) on 𝑃𝑙 , 𝐷3 and 𝑃𝑟 yields 𝑆2 ∶= 𝐸𝑏, 𝐸𝑐, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3 , 𝜑[𝑥/𝑏]
(3 − 𝐶𝑢𝑡) on 𝑃𝑙 , 𝐷4 and 𝑃𝑟 yields 𝑆3 ∶= 𝐸𝑏, 𝐸𝑐, 𝑐 = 𝑏, Γ1 , Γ2 , Γ3 ⇒ Δ1 , Δ2 , Δ3 ∣ Λ1 , Λ2 , Λ3 ⇒ Θ1 , Θ2 , Θ3
𝑆1 , 𝑆2 , 𝑆3 by (𝐼 − 𝐶𝑢𝑡) and (𝑂 − 𝐶𝑢𝑡) yield the desired result.
All these cuts are admissible by induction on the height.
5. Conclusion
To the best of our knowledge this paper offers the first proof-theoretic study of NFL with identity and
DD. The most important task for the presented variant of NFL is to find a satisfactory solution which
is cut free and does not restrict the treatment of DD to terms which do not admit nesting of other
DD inside. Such terms like ‘the owner of the biggest diamond’ should be dealt with in a direct way.
Moreover, (𝐿) characterises only the behaviour of proper DD so the present system provides the weakest
theory of DD. Since, as we mentioned, NFL seems to be the most natural framework for developing
a satisfactory theory of improper DD, the most important task for the future is to develop stronger
theories of DD.
Our intention is also to explore alternative approaches to NFL (see [15, 21]) based on different
definitions of propositional connectives, viable options concerning the treatment of existence predicate,
identity, and alternative interpretations of quantifiers. Moreover, taking into account that careless
treatment of DD leads to contradictions, it is an important task to explore its behaviour as founded on
paraconsistent logics, in the framework of BSC.
The next step would be to explore the problems of proof search and automatisation for NFL and
related systems. It seems that the completeness proof of [19], allowing for building countermodels, can
be extended to cover identity and DD by using techniques applied in [10] or [8]. Preparation of analytic
tableau systems for this kind of logics and their implementation would be another welcome output,
when the theoretical foundations will be firmly established.
Acknowledgements. We would like to thank anonymous reviewers for their valuable comments
and suggestions. This research is 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] Fitting, M., Mendelsohn, R., L.: First-Order Modal Logic, 2nd edition, Springer, Cham (2024)
[2] Fjellstad, A.: Non-classical elegance for sequent calculus enthusiasts. Studia Logica, 105(1), 93–119
(2017)
[3] Fjellstad, A.: Structural proof theory for first-order weak Kleene logics. Journal of Applied Non-
Classical Logics, 30(3), 272–289 (2020)
[4] Indrzejczak, A.: Free Definite Description Theory — Sequent Calculi and Cut Elimination. Logic
and Logical Philosophy. 29, 505–539 (2020)
[5] Indrzejczak, A.: Free Logics are Cut-Free. Studia Logica. 109, 859–886 (2021)
60
[6] Indrzejczak, A.: Russellian Definite Description Theory — a Proof Theoretic Approach. Review of
Symbolic Logic, 16 (2): 624–649 (2023)
[7] Indrzejczak, A.: Bisequent Calculus for Four-Valued Quasi-Relevant Logics; Cut Elimination and
Interpolation. Journal of Automated Reasoning, 67: paper 37 (2023)
[8] 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)
[9] Indrzejczak, A. Petrukhin, Y.: A Uniform Formalisation of Three-Valued Logics in Bisequent Calcu-
lus. In: International Conference on Automated Deduction, CADE 2023: Automated Deduction —
CADE 29. pp. 325–343. Springer, Rome (2023)
[10] Indrzejczak, A., Zawidzki, M.: When Iota meets Lambda. Synthese 201/72 (2023), DOI:
10.1007/s11229-023-04048-y.
[11] Kleene, S. C.: On a notation for ordinal numbers. The Journal of Symbolic Logic. 3(1), 150–155
(1938)
[12] Kürbis, N., A binary quantifier for definite descriptions in intuitionist negative free logic: Natural
deduction and normalization. Bulletin of the Section of Logic. 48(2), 81–97 (2019)
[13] Kürbis, N., Two treatments of definite descriptions in intuitionist negative free logic. Bulletin of
the Section of Logic. 48(4), 299–317 (2019)
[14] Kürbis, N., Definite descriptions in intuitionist positive free logic. Logic and Logical Philosophy.
30(2), 327–358 (2021)
[15] Lehmann, S.: Strict Fregean Free Logic. Journal of Philosophical Logic. 23(3), 307–336 (1994)
[16] Maffezioli, P., Orlandelli, E.: Full cut elimination and interpolation for intuitionistic logic with
existence predicate. Bulletin of the Section of Logic. 48(2), 137–158 (2019)
[17] Orlandelli, E.: Labelled calculi for quantified modal logics with definite descriptions. Journal of
Logic and Computation 31(3) 923–946 (2021)
[18] Pavlović, E., Gratzl, N. A More Unified Approach to Free Logics. J Philos Logic 50, 117–148 (2021)
[19] Pavlović, E., Gratzl, N. Neutral Free Logic: Motivation, Proof Theory and Models. J Philos Logic
52, 519–554 (2023)
[20] Russell, B. On Denoting, Mind. 14, 479–493 (1905)
[21] Woodruff, P.: Logic and Truth Value Gaps, pages 121–142 in K. Lambert (ed.), Philosophical
Problems in Logic. Reidel, Dordrecht (1970)
61