this extended system. 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 There is a variety of logics called free logics (FL) and difering 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.
[16], Pavlović and Gratzl1[8], 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 W21o]oadnrduf [ Lehmann [15], where one may find some kind of natural deduction and tableau system, only Pavlović and Gratzl1[9] recently investigated SC for NFL based on strong and weak Kleene l1o1g]i.cs [
We are going to continue the research carried ou19t]iinn[two ways: first, we reformulate the results from1[9] using our own approach based on bisequent calculi (BSC), developed9i,n7][; 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 Mathematica’). Improper DD are very troublesome and it seems that NFL is quite natural place for exploring their behaviour. Usually, DD are formalised by means of term-for-mopinegrator applied to a variable and formula to obtain a ter m . It is worth noting that there is an alternative treatment of DD based on the application of binary quantifier and recently developed by K1ü2r,b1i3s,[14]. We follow here a more standa r-do,perator based approach.
The theories of DD in positive or negative free logics are usually based on Lambert a):xiom ( ∀ ( = ↔ ∀( ↔ = )) ( ) where
is closed and does not have any occurrence .oIft is the weakest principle characterising the behaviour of proper DD. In our research, devoted to NFL, we con(si)daesr well but to avoid usin↔g,
CEUR
ceur-ws.org 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 restricti on: 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 1[9], we examine two variants of NFL, based on strong and weak Klee1n1e]’sin[terpretation 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 Mendelso1h]n,O[ rlandelli 1[7] 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 diferent 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 f1r9o]mar[e 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 logic1s9)], [(SC for neutral free logics4)], [(SC for DD theories based on negative and positive free logics), a9n,d7][ (BSC for many-valued logics).
The structure of the paper is as follows. Sec2tciontains some preliminaries related to the language and semantics. Sectio3nis devoted to the introduction of the BSC for two variants of NFL based on strong and weak Kleene’s logic. Sectio4nis concerned with the constructive proof of cut admissibility.
Following [19], we consider the subsequent language but with added conjunction, for dealin(g )w.ith
Definition 2.1. [19, Definition 1.1] The alphabet of the language ℒ consists of:
(
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 languℒagaensdℒ = are defined by simultaneous recursion. Note that iℒn =, , represent arbitrary terms, including DD. Complexity of formulae and terms is measured by the number of logical symbols (including predicateasnd =). [ 1/ 2] is used for the operation of correct substitution of an arbitrar2yfoterramll occurrences of a variable/parame1tienr , and similarlyΓ[ 1/ 2] for a uniform substitution in all formulaΓe. Wine use a simplified semantics from [19, 18] to provide interpretation of this language. ,
, and any 1 ⩽ ⩽ .
Definition 2.3 (Neutral structur e ). [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 () = { 1 if ∈ ℐ (), 0 if otherwise ; (¬) = { 1/2 if () = 1/2, ( ( 1, … , )) = { 1/2 if for some 1 ⩽ ⩽ , ∉ ℐ (), • ℐ ( ) ⊆ ℐ () such that if ⟨, ⟩ ∈ ℐ (=) , then ⟨… , , …⟩ ∈ ℐ ( ) if ⟨… , , …⟩ ∈ ℐ ( ), for any
Note that identity is in principle treated as other predicates but it cannot be defined in this way since domains of models contain just parameters, so it should be defined as a condition on models lik1e8]i.n [ ℐ is extended to cover descriptio ns, where does not contain other DD, by partial mapping from the set of so restricted DDs t.oIn caseℐ () = assume that it satisfies the following condition: , for some ∈ ℐ () , we say that is defined and ℐ () = if
([/]) = 1 {otherwise it is undefined.
and their approach. According ly may be either weak =( ) or strong =( ), and is defined as follows: assignment on the structure ⟨ , ℐ ⟩ is defined as follows: Definition 2.4 (Weak valuatio n ). (An extended version of [19, Definition 4.2] ) The truth-value , closed under symmetry and transitivity, where Definition 2.5 (Strong valuatio n ). [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): 1 0 1 0 1 0 0 1 1 if ⟨ 1, … , ⟩ ∈ ℐ ( ), if otherwise ; if () = 0, if () = 1; if () = 1 and ( ) = 1, if otherwise ; if () = 1 and ( ) = 0, if otherwise ; if for every ∈ ℐ (), if for some ∈ ℐ (), ([/]) = 1, ([/]) = 0, ( ∧ ) =
{ 1/2 if () = 1/2 or ( ) = 1/2, ( → ) =
{ 1/2 if () = 1/2 or ( ) = 1/2, (∀) = { 0
1/2 if otherwise . ( ∧ ) =
0 { 1 if () = 0 or () = 1 and ( ) = 1,
( ) = 0, 1/2 if otherwise . 1/2 if otherwise . (5′)
For each of these valuations, we can obtain two diferent logics by taking the set of designated values either as{1} or{1,1/2}. However, we examine here only the first route, hence in what follows 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 Γ ⊧ if for any valuation : if (Γ) ⊆ , then () ∈ , where = {1} .
In what follows the strong Kleene’s logic will be referredKt3oaansd the weak one aKs 3w. Although propositionaKl 3 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 K3w. and
([/] ≠ ∈ ℐ () and and and
( = and ([/]
([/] → = ([/] → =
Proof. As an example, let us prove tha( t→) is valid inK3. Suppose that( →) is not valid inK3, that is = ) ) = 0. Consequently, ( =
) = 1 and (( →)) ≠ 1. Suppose that (( →)) = 0. Then for some ∈ ℐ () , ([/] ∧ ∀( → = ) ([/]) = 1 , we get (∀( → = ) ) = 0.
Then for some ∈ ℐ () , ([/] → = ) = 0. Hence, ([/] ) = 1 and
( = ) = 0. Since ( = → [/] ∧ ∀( → ) = 0. Therefore, Suppose tha t (( →)) = 1/2. Let ( →
) denote = → [/] ∧ ∀( → = ) we can infer that either ther∉e iℐs () and (( (( →)) = 1/2. Suppose that there i∉s ℐ () and (( →)) ∈ {1,1/2, 0} or there is∈ ℐ () such that →)) ∈ {1,1/2, 0}. However,ℐ (=) = ∪ and ⊆ ℐ () × ℐ ()
. Thus, it cannot be the case that th er∉eℐis() (( →)) ∈ {1,1/2, 0}. Hence, there is∈ ℐ () such tha t (( →)) = 1/2. It cannot be the case . Hence, ) = 1/2, otherwis e ∉ ℐ ()
or ∉ ℐ () ) = 1/2. Since ∈ ℐ () , butℐ (=) ⊆ ℐ () . Thus,
( = and ( = ) = 1, ([/]) = 1 ) = 1 ([/] ∧ ∀( → = ) properties oℐf (=), only the latter option holds. Siℐnc(e=) ⊆ ℐ () , ( = ) ≠ 1/2. Thus, since for every ≠ ∈ ℐ () . Since ([/]) = 1 and ([/] ∧ ∀( → = ) ∈ {1,1/2, 0} or there is∈ ℐ () such tha t ([/] → =
) = 1/2. Due to the ) = 1/2. Hence, we can infer that either the r∉eℐis() and ) = 1/2, we obtain ([/] ) = 1/2 and
for ever y≠ ∈ ℐ () , we infer tha t ( = ) = 0. Since , ∈ ℐ ()
, ≠ , ([/]) = 0 . But we already have that ) = 1/2. A contradiction.
Pavlović and Gratzl1[9] formalise NFL by means of some nonstandard SC, where sequents are of the form: Γ; Π ⇒ Σ; Δ. However we prefer to use for this aim bisequent calculus (BSC) which was already applied as a uniform basis for arbitrary three-valued logi9c]s. iSnim[ilar sequent system (but with a slightly diferent semantic interpretation) was applied also by Fjell2s,t3a]d. B[isequents are ordered pairs of sequentΓs ⇒ Δ ∣ Π ⇒ Σ, whereΓ, Δ, Π, Σ are finite (possibly empty) multisets of formulae. The correspondence of bisequents to nonstandard sequents 1f9r]oims i[ndicated by using the same metavariablesΓ, Δ, Π, Σ in both cases. and are used as metavariables for bisequents and sequents, respectively.
In both systems of NFL a bisequenΓt⇒ Δ ∣ Π ⇒ Σ is axiomatic if for some atomic formula (including identities an d), eithe r∈ Γ ∩ Σ or ∈ Γ ∩ Δ
or ∈ Π ∩ Σ . Moreover, bisequents of the form 1, … , , Γ ⇒ Δ, ( 1, … , ) ∣ ( 1, … , ), Π ⇒ Σ are also axiomatic.
As follows from 9[], propositional connectivesKo3f are characterised by the rules from 1F.igT.he propositional connectivesKo3fw are mostly as inK3, 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 predicate in the spirit of the rules given19i]n. [
Note that the application(s∀o⇒f∣) and(∣∀⇒) are restricted to parameters as instantiated terms, no DD are allowed as instantiated terms! It saves us from losing the subformula property.
In negative FL a standard identity is replaced by its weaker variant with restricted r→eflex=ivity. In NFL we treat identity similarly so it behaves like other predicates and this is why the four rules for from Fig.3 apply also to identities.
Notice that the ru(∣le⇒ =), required for proving the Leibniz Principle, is like the rule f4r]o.mWe[ lose unrestricted subformula property but not in the essential way; in fact o n,lyatnedrmastoms 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 efect. 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 in6][, with the separation of rules for diferent kinds of identities, but this leads to the proliferation of rules and, because of space restrictions, we present here a simpler form of the calculus. A generalisation of quantifier rules to variants admitting DD as instantiated terms is easily provable since∀, ⊢ [/] holds.
How BSC relates to the semantics from Sect2i?onFollowing [9, p. 331], we give the subsequent (⇒∀ ∣) (∀⇒∣) (⇒∣) (∣⇒) (⇒∣) , Γ ⇒ Δ, [/] ∣
Γ ⇒ Δ, ∀ ∣ , ∀, [/], Γ ⇒ Δ ∣
, ∀, Γ ⇒ Δ ∣ , [], Γ ⇒ Δ ∣ [], Γ ⇒ Δ ∣ (∣⇒∀) (∣∀⇒) , Γ ⇒ Δ ∣ Π ⇒ Σ, [/]
Γ ⇒ Δ ∣ Π ⇒ Σ, ∀ , Γ ⇒ Δ ∣ ∀, [/], Π ⇒ Σ
, Γ ⇒ Δ ∣ ∀, Π ⇒ Σ (∣⇒) , Γ ⇒ Δ ∣ Π ⇒ Σ, []
Γ ⇒ Δ ∣ Π ⇒ Σ, [] 1, … , , ( 1, … , ), Γ ⇒ Δ ∣ Π ⇒ Σ 1, … , , Γ ⇒ Δ ∣ ( 1, … , ), Π ⇒ Σ 1, … , , Γ ⇒ Δ ∣ Π ⇒ Σ, ( 1, … , ) 1, … , , Γ ⇒ Δ, ( 1, … , ) ∣ Π ⇒ Σ (
1) ( 2) , Γ ⇒ Δ ∣ Π ⇒ Σ Γ ⇒ Δ ∣ , Π ⇒ Σ Γ ⇒ Δ ∣ Π ⇒ Σ, Γ ⇒ Δ, ∣ Π ⇒ Σ 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.
Definition 3.1. ⊧ Γ ⇒ Δ ∣ Π ⇒ Σ if every valuation satisfies Γ ⇒ Δ ∣ Π ⇒ Σ. The latter holds for if for some : either ( ∈ Γ and () ≠ 1 ) or ( ∈ Δ and () = 1 ) or ( ∈ Π and () = 0 ) or ( ∈ Σ and () ≠ 0 ). Clearly ⊧ Γ̸ ⇒ Δ ∣ Π ⇒ Σ if 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.
As follows from9[], all axiomatic bisequents are valid and all the rules for connectives are both sound (validity-preserving) and invertible. The same holds for the rules fro3maFsigf.ollows from1[9]. It may be extended to the new rules from F4iga. nd5, hence it holds: Theorem 3.1 (Soundness). For any bisequent , if ⊢ , then ⊧ .
Proof. By induction of the height of the derivation, using the fact that all the rules are sound. As an
example, let us illustrate soundness of the r(u∣⇒le ). The proof holds both fKor3 andK3w. Recall that
is fresh.
(
(9) ℐ () ≠ , that is([/]) ≠ 1 or ([/]) ≠ 0 , for some ≠ ∈ ℐ () . (10) Since is fresh,([/]) ≠ 1 or( ([/]) ≠ 0 and ≠ ∈ ℐ () ). (11) Suppose tha t([/]) ≠ 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. (17) Contradiction. Thu⊧s,, Γ ⇒ Δ ∣ Π ⇒ Σ, = .
In fact, for the NFL without DD and identity, as defined by rules from1,F2i,g3., also completeness was proved in 1[9], and it may be extended in a straightforward way to cover identity, as was done for negative FL in1[8]. For DD we already demonstrated th( a)tis 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 o)f. (
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, related to definition of consequence relation, as defined in Sect2i.onThe definition of validity for bisequents shows that the entailment betwΓeaennd is expressed in BSC as provability oΓf⇒ ∣ ⇒ . Moreover, although in propositional Kleene’s logic the set of validities is empty it is not so in the ifrst-order NFL based on it. In particular, both forms )oafr(e 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: Lemma 3.1 (Substitution)I.f ⊢ Γ ⇒ Δ ∣ Θ ⇒ Λ is derivable (where denotes derivability with height bounded by ), then the sequent ⊢ Γ[/] ⇒ Δ[/] ∣ Θ[/] ⇒ Λ[/] is likewise derivable.
Lemma 3.2. ⊢ 1, … , , Γ ⇒ Δ, ( 1, … , ) ∣ ( 1, … , ), Π ⇒ Σ, where 1, … , are all terms occuring in
Lemma 3.3 (Leibniz Law). For any formula , it holds that ⊢ 1 = 2, [/ 1] ⇒ [/ 2] ∣ .
The proof o(f ←) in strong Kleene logic is as follows, where) s(tands for provable⇒ [/] ∣
: For ( →) let ( ′) stand for the following proof: Then: ( ) ⇒ [/] ∣ [/] ⇒
, ⇒ = ∣ = ⇒ , ⇒ = ∣ [/], [/] → = ⇒ , ⇒ = ∣ [/], ∀( → = ) ⇒ ⇒ = ∣ [/], ∀( → = ) ⇒ ⇒ = ∣ [/] ∧ ∀( → = ) ⇒ ⇒ [/] ∧ ∀( → = ) → = ∣⇒ ⇒ ∀([/] ∧ ∀( → = ) → = ) ∣⇒ (∣→⇒) (∣ ∀ ⇒)
Proofs in BSC for weak Kleene’s logic are more complex since the applicatio(n⇒s→of∣) and(∣ ∧ ⇒) introduce additional premisses. However, in all respective premisses we obtain simply sequents of the All rules for DD are derivable if we u(se→) or(
← form, Γ ⇒ Δ, () ∣ (), Π ⇒ Σ or, , Γ ⇒
Δ, (, ) ∣ (, ), Π ⇒ Σ proved admissible in the next section. Here is an example. From both premiss(e⇒s o∣f) we obtain: ) as additional axioms and use cuts which will be which are provable. , Γ ⇒ Δ, [/] ∣ Π ⇒ Σ , Γ ⇒ Δ, [/] ∧ ∀( → = ) ∣ Π ⇒ Σ , , Γ ⇒ Δ, = ∣ [/], Π ⇒ Σ , , Γ ⇒ Δ, [/] → = ∣ Π ⇒ Σ , Γ ⇒ Δ, ∀( → = ) ∣ Π ⇒ Σ (⇒→∣) (⇒ ∀ ∣) (∣⇒ ∧) = ) ∣⇒ provable. latter bisequent is proved by cuts on the axiomatic seq(ue←n)ti.e. ⇒ ∀([/] ∧ ∀( → = ) → which by cut wit h, [/] ∧ ∀( → = ) ⇒ = ∣⇒ yields the conclusion o(f⇒ ∣) . The with, ∀([/] ∧ ∀( → = ) → = ) ⇒ [/] ∧ ∀( → = ) → = ∣⇒ and [/] ∧ ∀( → = ) → = ), [/] ∧ ∀( → = ) ⇒ = ∣⇒ which are easily
Lemma 4.1 (Generalisation of axiomsF)o.r any formula , the following bisequents are derivable:
(
Here we present proofs of the admissibility of cut with all forms of cut1s9f].roBmut[ first we demonstrate the admissibility of structural rules, lik19e]i.n [ Lemma 4.2 (Admissibility of structural ruleSst)r.uctural rules from Fig. 6 are height-preserving admissible.
Lemma 4.3 (Invertibility)A.ll the rules of the bisequent calculi in question are height-preserving invertible.
Lemma 4.4 (Transfer).The following rules are height-preserving admissible: ( ) Γ ⇒ Δ ∣ , Π ⇒ Σ , Γ ⇒ Δ ∣ Π ⇒ Σ ( ) Γ ⇒ Δ, ∣ Π ⇒ Σ Γ ⇒ Δ ∣ Π ⇒ Σ,
Proof. Straightforward extension of the proof by induction on the height of the deriv1a9t]i.on from [ Theorem 4.1 (Cut admissibility).The rules (E-Cut), (L-Cut), (O-Cut), (I-Cut), (R-Cut), (3-Cut) are admissible.
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 prov1e9d] isnim[ultaneously, 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, = ∣ = ,Λ ,Γ 1,Γ2,Γ3 ⇒ Δ1,Δ2,Δ3 ∣ Λ1,Λ2,Λ3 ⇒ Θ1,Θ2,Θ3 1Notice that we considered just two cut rules on the propositiona9l].leHveolw[ever, the first-order case requires more options, which are actually the same as Pavlović and Gratzl 1h9a]v.eT[hey follow the strategy of Fjellst3a]din[ this respect.
for simplicity let us refer to the premisses of this c u, t a,s . Since the middle premis s may be derived either b(y ⇒∣ 1) or( ⇒∣ 2) and the rightmost premi ssmay be derived either b(y⇒ ∣) (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, = ∣ = , Λ let 1 stands for the following:
1 Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1, [/] we transform the proof as follows: 4 , Γ 3 ⇒ Δ3, = ∣ = , [/], Λ 3 ⇒ Θ3 (3-Cut) 1 , Γ 1, Γ2, Γ3 ⇒ Δ1, Δ2, Δ3 ∣ [/], Λ 1, Λ2, Λ3 ⇒ Θ1, Θ2, Θ3 (I-Cut) , Γ 1, Γ1, Γ2, Γ3 ⇒ Δ1, Δ1Δ2, Δ3 ∣ Λ1, Λ1, Λ2, Λ3 ⇒ Θ1, Θ1, Θ2, Θ3 ()
, Γ 1, Γ2, Γ3 ⇒ Δ1, Δ2, Δ3 ∣ Λ1, Λ2, Λ3 ⇒ Θ1, Θ2, Θ3 where(3 − ) is admissible by induction on the height a(n−d ) 1.2. is derived as follows: by induction on the degree. where 2 stands for
2 3 , Γ 3 ⇒ Δ3, = ∣ = , Λ and 3 stands for note that also must occur inΓ3. We perform: , Γ 3 ⇒ Δ3, = , [/] ∣ = , Λ desired result.
2. Now let the middle premiss be derived as follows: where 7 stands for where both cuts are admissible by induction on the degree. 1.3. is derived as follows: and 5 stands for where ′ is eigenvariable diferent fro m. We perform: (O-Cut)() Γ1 ⇒ Δ1 ∣ Λ1 ⇒ Θ1, = 6
, Γ 3 ⇒ Δ3, = ∣ = , Λ , [/], Γ 1, Γ2, Γ3 ⇒ Δ1, Δ2, Δ3 ∣ Λ1, Λ2, Λ3 ⇒ Θ1, Θ2, Θ3 both cuts are admissible by induction on the height. By substitution lem m2awoenobtain a proof of 2 ∶= , [/], Γ 1 ⇒ Δ1, ∣ Λ1 ⇒ Θ1, = . We finish with: 4 3 ⇒ Θ3 (I-Cut) and where 6 stands for = , [/], Γ
2 ⇒ Δ2, ∣ Λ2 ⇒ Θ2 Both cuts are admissible by induction on the height and the resulting sequ(en−ts)by lead to 5 4 5 3 and 8 stands for
, = , = , Γ 2.1. and the right premiss by: and the sequent resulting (b3y− ) is: , , Γ 1, Γ2, Γ3 ⇒ Δ1, Δ2, Δ3 ∣ Λ1, Λ2, Λ3 ⇒ Θ1, Θ2, Θ3 we transform the proof as follows: where 10 stands for where 11 stands for
10 11 , Γ 3 ⇒ Δ3, = ∣ = , Λ 6 , Γ 3 ⇒ Δ3, = ∣ = , = ′, Λ3 ⇒ Θ3 note that also ′ must occur inΓ3 ( ′ distinct fro m).
(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 with cuts admissible by induction on the height.
By substitution lemma on2 we get 9 ∶= ′, [/ ′], Γ1 ⇒ Δ1, ∣ Λ1 ⇒ Θ1, = ′ ( − ) and( − ) made on these three sequents yield the desired result. 2.3. Finally let the right premiss be obtained by: where 12 stands for
12 13 , Γ 3 ⇒ Δ3, = ∣ = , Λ and 13 stands for
To the best of our knowledge this paper ofers 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 NF1L5,(s2e1e])[based on diferent 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 proo1f9]o,fa[llowing for building countermodels, can be extended to cover identity and DD by using techniques applie1d0]inor[ [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. [6] Indrzejczak, A.: Russellian Definite Description Theory — a Proof Theoretic Approach. Review of
Symbolic Logic, 16 (
[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.
[9] Indrzejczak, A. Petrukhin, Y.: A Uniform Formalisation of Three-Valued Logics in Bisequent
Calculus. 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 L3o(1g)i,c1.50–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 4L8o(g2i)c, .81–97 (2019)
[13] Kürbis, N., Two treatments of definite descriptions in intuitionist negative free logic. Bulletin of
the Section of Logi4c8.(
30(
Logic and Computatio3n1(