Labelled Calculi for Quantified Modal Logics with Non-rigid and Non-denoting Terms Eugenio Orlandelli and Giovanna Corsi University of Bologna, Bologna, Italy {eugenio.orlandelli,giovanna.corsi}@unibo.it Abstract We introduce labelled sequent calculi for quantified modal logics with non-rigid and and non-denoting terms. We prove that these calculi have the good structural properties of G3-style calculi. In particular, all rules are height-preserving invertible, weakening and contraction are height-preserving admissible and cut is admissible. Finally, we show that each calculus gives a proof-theoretic characterization of validity in the corresponding class of models. 1 Introduction The proof-theoretic study of propositional modal logics has been a very active field of research in the last few decades thanks to the introduction of generalizations of Gentzen-style sequent calculi such as display calculi [1], hypersequents [1], and labelled sequent calculi [10]. Nev- ertheless, the proof-theoretic study of quantified modal logics (QMLs) has remained rather underdeveloped. One notable exception is [10, Chap. 12.1], where labelled sequent calculi for QMLs are introduced. More specifically, the labelled calculi for the propositional modal logics in the cube of normal modalities – i.e. the minimal normal modal logic K and its extensions with axioms D, T, 4, 5 – are extended with quantifiers based on varying, increasing, decreasing and constant domains. One interesting aspect of QMLs that has not been considered in [10] is the study of logics based on a language containing the identity predicate and non-rigid as well as non-denoting terms, see [6, 7]. We introduce labelled calculi for these logics and we study their structural properties. As it is convincingly argued in [6, 7], the need for non-rigid and non-denoting terms origi- nates from problems already touched upon in the classical works of Frege [8] and Russell [12]. First, as Frege noticed, even if ‘Hesperus’ and ‘Phosphorus’ are both names of Venus and the ancient knew that objects are self-identical, the Babylonians did not know that Hesperus is Phosphorus. Despite this, in quantified epistemic logics based on rigid terms, we can prove that the Babylonians knew it. Moreover, Russell showed that the sentence ‘The present king of France is not bald’ is ambiguous since it might either mean that the sentence ‘the present king of France is bald’ is false, or that the present king of France is such that he is non-bald. Given that the expression ‘The present king of France’ does not actually denote anyone, the first reading is, in fact, true and the second false. If we exclude non-denoting terms, we cannot account for these two readings of that sentence (unless we explain away the term expressing the definite description ‘the present king of France’). As the two examples above show, it is interesting to consider QMLs with non-rigid and/or non-denoting terms, but their addition to the language of QMLs is not trivial [6, 7]. The problem, roughly, is that if t is a non-rigid (or non-denoting) term, the formal sentence 3P t becomes ambiguous. When it is evaluated in a possible world w of some model, it might either mean that the object denoted by t in w satisfies the unary predicate P is some world v that is accessible from w, or that there is a world u that is accessible from w and such that the ARQNL 2018 64 CEUR-WS.org/Vol-2095 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi formal sentence P t is true therein. For rigid terms these two readings are equivalent. For non- rigid terms neither reading entails the other, and, therefore, we need some scoping mechanism to disambiguate the formula 3P t. The solution proposed in [6, 7] is that of extending the language with the operator of predicate abstraction λ. The two readings of 3P t can thus be expressed, respectively, by the (semantically independent) formal sentences: λx.3P x.t and 3(λx.P x.t) . (1) We will extend the labelled sequent calculi for QMLs presented in [10] to handle non-rigid and non-denoting terms based on the predicate abstraction operator λ. We will study the structural properties of these extensions, and we will show that, as for the calculi in [10], all the rules of inference are height-preserving invertible, the structural rules of weakening and contraction are height-preserving admissible, and the rule of cut is admissible. Finally, we will prove that each calculus considered characterizes validity in the appropriate class of models. The paper is organized as follows. Section 2 sketches the labelled calculi for QMLs presented in [10]. In particular, the language and semantics of QMLs without non-rigid and non-denoting terms are introduced in Section 2.1. Labelled calculi for these logics and their main meta- theoretical properties are outlined in Section 2.2. In Section 3, we extend the labelled approach to QMLs with identity and non-rigid and non-denoting terms. We once again start by outlining the syntax and the semantics (Section 3.1). Then, we introduce labelled calculi for these logics (Section 3.2), and we prove: (i) that they have the good structural properties that are distinctive of G3-style calculi (Section 3.2.1) and (ii) that they are sound and complete with respect to the appropriate classes of quantified modal models (Section 3.2.2). We conclude in Section 4. 2 Quantified Modal Logics without Individual Constants In this section, we present QMLs based on a varying domain semantics defined over a signature not containing individual constants nor the identity symbol, and we present labelled calculi for these logics. Apart from some minor adjustment, the semantics is as in [7, Chap. 4.7], and the calculi are as in [10, Chap. 12.1]. This section is needed to make the paper self-contained and it might be skipped by readers already familiar with QMLs and labelled calculi. 2.1 Syntax and Semantics Let S be a signature containing, for every n ∈ N, an at most denumerable set of n-ary predicate letters P1n , P2n , . . . ; let V AR be an infinite set of variables x1 , x2 , . . . ; and let the primitive logical symbols be ¬, ∧, ∀, 2. The language L is given by the grammar: A ::= P n y1 , . . . , yn | ¬A | A ∧ A | ∀yA | 2A (L) where Pn ∈ S and y, y1 , . . . , yn ∈ V AR. In this paper we use the following metavariables: • P, Q, R for predicate letters; • x, y, z for variables; • p, q, r for atomic formulas; • A, B, C for formulas. 2 65 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi We follow the standard conventions for parentheses. The formulas ⊥, >, A ∨ B, A ⊃ B, ∃yA, and A are defined as expected. The notions of free and bound occurrences of a variable in a formula are the usual ones. Given a formula A, we use A[y/x] to denote the formula obtained by replacing each free occurrence of x in A with an occurrence of y, provided that y is free for x in A – i.e., if no one of the new occurrences of y would be bound by a quantifier. The weight of a formula is the number of nodes of its generation tree. A model (over the signature S) is a tuple: M =< W, R, D, V > (2) where • W= 6 ∅ is a nonempty set of (possible) worlds (to be denoted by w, v, u . . . ); • R ⊆ W × W is a binary accessibility relation between worlds; • D : W −→ 2D is a function S mapping each world to a possibly empty set of objects Dw (its domain), where D = w∈W Dw is nonempty and disjoint from W; n • V : S × W −→ 2D is an interpretation function mapping, at each world w, each n-ary predicate P (∈ S) to a subset of Dn . Given a model M =< W, R, D, V >, an assignment (over M ) is a function σ : V AR −→ D mapping each variable x to an element of the union of the domains of the model. Moreover, for a ∈ D, σ x.a denotes the assignment behaving like σ save for x that is mapped to the object a. Definition 1 (Satisfaction). Given a model M , an assignment σ over it, and a world w of that model, we define the notion of satisfaction of an L -formula A as follows: σ |=M w P x1 , . . . xn iff < σ(x1 ), . . . , σ(xn ) >∈ V(P, w) σ |=M w ¬B iff σ 6|=M w B σ |=M w B∧C iff σ |=M M w B and σ |=w C σ |=M w ∀xB iff for all a ∈ Dw , σ x.a |=M w B σ |=M w 2B iff for all v ∈ W, wRv implies σ |=M v B The notions of truth in a world w of a model (|=M w A), truth in a model (|= M A), and validity in a class of models (C |= A) are defined as usual. As it is well known, some notable formulas, such as the Barcan Formulas, are valid in classes of models defined by properties of the accessibility relation and/or of the domains. By an L - logic Q.L we mean the set of all L -formulas that are valid in a class of models defined by some combination of the properties given in Table 1. We use standard names for L -logics – e.g., Q.K stands for the set of L -formulas valid in the class of all models, and Q.S4⊕BF stands for the set of L -formulas valid in the class of all reflexive and transitive models with decreasing domains. We say that M is a model for Q.L whenever |=M A for all A ∈ Q.L. 2.2 Labelled Sequent Calculi Labelled sequent calculi for L -logics have been introduced in [10, Chap. 12.1]. These calculi are based on an extension of the modal language in order to internalize the semantics of QMLs as follows. First of all, we introduce a set LAB of fresh variables, called labels. Labels will be denoted by w, v, u, . . . and will be used to represent worlds. Then, we extend the set of formulas 3 66 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi Table 1: Modal axioms and corresponding semantic properties T := 2A ⊃ A reflexivity:=∀w ∈ W(wRw) D := 2A ⊃ 3A seriality:=∀w ∈ W∃u ∈ W(wRu) 4 := 2A ⊃ 22A transitivity:=∀w, v, u ∈ W(wRv ∧ vRu ⊃ wRu) 5 := 3A ⊃ 23A Euclideaness:=∀w, v, u ∈ W(wRv ∧ wRu ⊃ vRu) N E := ∀xA ⊃ ∃xA nonempty domains:=∀w ∈ W∃a ∈ D(a ∈ Dw ) U I := ∀xA ⊃ A[y/x] constant domains:=∀w ∈ W∀a ∈ D(a ∈ Dw ) CBF := 2∀xA ⊃ ∀x2A increasing domains:=∀w, v ∈ W∀a ∈ D(a ∈ Dw ∧ wRv ⊃ a ∈ Dv ) BF := ∀x2A ⊃ 2∀xA decreasing domains:=∀w, v ∈ W∀a ∈ D(a ∈ Dv ∧ wRv ⊃ a ∈ Dw ) by adding atomic formulas of shape x ∈ w – expressing that (the object assigned to) x is in the domain of quantification of (the world represented by) w – and of shape wRv – expressing that v is accessible from w. Lastly, we replace each L -formula A with the labelled formulas w : A – expressing that A holds at w. A labelled sequent is an expression: Ω; Γ ⇒ ∆ where Ω is a multiset of atomic formulas of shape x ∈ w or wRv, and Γ and ∆ are multisets of labelled formulas. Given a formula E of this extended language, E[w/v] is the formula obtained by substituting each occurrence of v in E with an occurrence of w. Substitution of variables is extended to formulas of the extended language as expected, and both kinds of substitution are extended to sequents by applying them componentwise. The rules of the calculus G3Q.K, for the minimal L -logic Q.K, are given in Table 2. For each logic Q.L extending Q.K, the calculus G3Q.L is obtained by extending G3Q.K with the non-logical rules of Table 3 that express proof-theoretically the semantic properties that define Q.L (cf. Table 1). Whenever a calculus contains rule Eucl, it contains also all its contracted instances Euclc . Observe that CBF (BF ) is not derivable in calculi where rule Incr (Decr) is not primitive nor admissible (given Proposition 2.8, this can be checked semantically). A G3Q.L-derivation of a sequent Ω; Γ ⇒ ∆ is a tree of sequents, whose leaves are initial sequents, whose root is Ω; Γ ⇒ ∆, and which grows according to the rules of G3Q.L. As usual, we consider only derivations of pure sequents – i.e., sequents where no variable has both free and bound occurrences. The height of a G3Q.L-derivation is the number of nodes of its longest branch. We say that Ω; Γ ⇒ ∆ is G3Q.L-derivable (with height n), and we write G3Q.L `(n) Ω; Γ ⇒ ∆, if there is a G3Q.L-derivation (of height at most n) of Ω; Γ ⇒ ∆. A rule is said to be (height-preserving) admissible in G3Q.L, if, whenever its premisses are G3Q.L-derivable (with height at most n), also its conclusion is G3Q.L-derivable (with height at most n). In each rule depicted in Tables 2 and 3, Ω, Γ and ∆ are called contexts, the formulas occurring in the conclusion are called principal, and the formulas occurring in the premisses only are called active. The following proposition presents the main meta-theoretical properties of G3Q.L. The proofs can be found in [10, Chap. 12.1]. Proposition 2 (Properties of G3Q.L). 1. Sequents of shape Ω; w : A, Γ ⇒ ∆, w : A (with A non-atomic) are G3Q.L-derivable. 4 67 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi Table 2: Rules of G3Q.K initial sequents: Ω; w : p, Γ ⇒ ∆, w : p, with p atomic logical rules: Ω; Γ ⇒ ∆, w : A Ω; w : A, Γ ⇒ ∆ L¬ R¬ Ω; w : ¬A, Γ ⇒ ∆ Ω; Γ ⇒ ∆, w : ¬A Ω; w : A, w : B, Γ ⇒ ∆ Ω; Γ ⇒ ∆, w : A Ω; Γ ⇒ ∆, w : B L∧ R∧ Ω; w : A ∧ B, Γ ⇒ ∆ Ω; Γ ⇒ ∆, w : A ∧ B y ∈ w, Ω; w : A[y/x], w : ∀xA, Γ ⇒ ∆ z ∈ w, Ω; Γ ⇒ ∆, w : A[z/x] L∀ R∀, z fresh y ∈ w, Ω; w : ∀xA, Γ ⇒ ∆ Ω; Γ ⇒ ∆, w : ∀xA wRv, Ω; v : A, w : 2A, Γ ⇒ ∆ wRu, Ω; Γ ⇒ ∆, u : A L2 R2, u fresh wRv, Ω; w : 2A, Γ ⇒ ∆ Ω; Γ ⇒ ∆, w : 2A Table 3: Non-logical rules wRw, Ω; Γ ⇒ ∆ vRu, wRv, wRu, Ω; Γ ⇒ ∆ vRv, wRv, Ω; Γ ⇒ ∆ RefW Eucl Eucl c Ω; Γ ⇒ ∆ wRv, wRu, Ω; Γ ⇒ ∆, wRv, Ω; Γ ⇒ ∆, wRu, Ω; Γ ⇒ ∆ wRu, wRv, vRu, Ω; Γ ⇒ ∆ Ser , u fresh Trans Ω; Γ ⇒ ∆, wRv, vRu, Ω; Γ ⇒ ∆ z ∈ w, Ω; Γ ⇒ ∆ x ∈ v, x ∈ w, wRv, Ω; Γ ⇒ ∆ NonEm, z fresh Incr Ω; Γ ⇒ ∆ x ∈ w, wRv, Ω; Γ ⇒ ∆ x ∈ w, Ω; Γ ⇒ ∆ x ∈ w, x ∈ v, wRv, Ω; Γ ⇒ ∆ Cons Decr Ω; Γ ⇒ ∆ x ∈ v, wRv, Ω; Γ ⇒ ∆ 2. The rule of α-conversion is height-preserving admissible: if G3Q.L `n Ω; Γ ⇒ ∆, then G3Q.L `n Ω; Γ0 ⇒ ∆0 , where Γ0 (∆0 ) is obtained from Γ (∆) by renaming bound variables. 3. The following rules of substitution are height-preserving admissible in G3Q.L: Ω; Γ ⇒ ∆ Ω; Γ ⇒ ∆ [y/x ] [w /v ] Ω[y/x]; Γ[y/x] ⇒ ∆[y/x] Ω[w/v]; Γ[w/v] ⇒ ∆[w/v] where y is free for x in each formula occurring in Γ, ∆ for rule [y/x]. 4. The following rules of weakening are height-preserving admissible in G3Q.L: Ω; Γ ⇒ ∆ Ω; Γ ⇒ ∆ Ω; Γ ⇒ ∆ LWΩ LW RW Ω0 , Ω; Γ ⇒ ∆ Ω; Γ0 , Γ ⇒ ∆ Ω; Γ ⇒ ∆, ∆0 5. Each rule of G3Q.L is height-preserving invertible. 6. The following rules of contraction are height-preserving admissible in G3Q.L: Ω0 , Ω0 , Ω; Γ ⇒ ∆ Ω; Γ0 , Γ0 , Γ ⇒ ∆ Ω; Γ ⇒ ∆, ∆0 , ∆0 LCΩ LC RC Ω0 , Ω; Γ ⇒ ∆ Ω; Γ0 , Γ ⇒ ∆ Ω; Γ ⇒ ∆, ∆0 5 68 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi 7. The following rule of Cut is admissible in G3Q.L: Ω; Γ ⇒ ∆, w : A Ω0 ; w : A, Γ0 ⇒ ∆0 Cut Ω, Ω0 ; Γ0 , Γ ⇒ ∆, ∆0 8. G3Q.L is sound and complete with respect to the class of all models for Q.L. 3 Quantified Modal Logics with Individual Constants Now we move to QMLs based on a language containing also non-rigid and non-denoting indi- vidual constants and the identity predicate. Given that constants will have a world-dependent interpretation, we will introduce the operator λ as a scoping mechanism. This allows us to distinguish between the formula λx.2P x.c (that is interpreted by first determining the object o denoted by c in w, and then by moving to worlds accessible from w to see whether o satisfies P therein) and the formula 2(λx.P x.c) (interpreted by first moving to each world v accessible from w, and then by determining the object denoted by c in each v and checking if it satisfies P ). The semantics is analogous to the varying domain semantics considered in [7, Chap. 11] and in [6]. Lastly, we introduce labelled sequent calculi for logics based on this semantics and we study their meta-theoretical properties. 3.1 Syntax and Semantics The language of Lλ is obtained by extending the signature S with an at most denumerable set CON of individual constants c1 , c2 , . . . ; functions of higher arity are omitted for simplicity. Let us call S λ the extended signature. Moreover, we extend the set of logical symbols with the operator λ of predicate abstraction and with the logical predicate =. The term-forming operator [7, Chap. 12] is omitted for simplicity. The set T ER of terms is the union of V AR ι and CON . The set of Lλ -formulas is generated by the grammar: A ::= P n y1 , . . . , yn | y1 = y2 | ¬A | A ∧ A | ∀yA | 2A | λy.A.t (Lλ ) where y, y1 , . . . , yn ∈ V AR, P n ∈ S λ , and t ∈ T ER. We will use for Lλ -formulas the same definitions introduced in Sect 2.1 for L-formulas; the only novelty being that, in λx.A.y, the occurrences of x are bound by λ and the displayed instance of y is free. Note that individual constants cannot occur in atomic Lλ -formulas: they can only be applied to a formula via λ. A model (over the signature S λ ) is a tuple: M =< W, R, D, V > (3) where W, R and D are defined as for M , see 2, and V is defined as: n • V : S λ × W −→ 2D is a partial interpretation function such that: 1. for each predicate P n and each w ∈ W, V(P n , w) ⊆ Dn ; 2. for each individual constants c and for some, possibly not all, w ∈ W, V(c, w) ∈ D. Assignments are defined as before as (total) functions σ : V AR −→ D. With an abuse of notation, we use σw (t) for the object denoted by the term t in M under σ – i.e., σw (t) stands for σ(t) if t is a variable and for V(t, w) if t is an individual constant. Notice that, if t is a constant, the fact that V(t, w) = o does not entail that V(t, v) = o nor that V(t, v) is defined. 6 69 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi Table 4: Additional modal axioms and corresponding properties RG := λx.2A.t ⊃ 2(λx.A.t) rigidity:=∀w, v ∈ W, ∀t ∈ CON (wRv&σw (t) ∈ D ⊃ σv (t) = σw (t)) T T := λx.x = x.t totality:=∀w ∈ W∀t ∈ CON (σw (t) ∈ D) Definition 3 (Satisfaction). Satisfaction of an Lλ -formula A at a world w of a model M under an assignment σ is defined as in Definition 1 with the addition of the following clauses: σ |=M w x=y iff σ(x) = σ(y) σ |=M w λx.B.t iff σw (t) is defined and σ x.σw (t) |=M w B The notions of truth and of validity are defined as in Sect. 2.1. An Lλ -logic Qλ.L is defined as the set of all formulas valid in some class of models M that is obtained by some combination of the semantic properties in Tables 1 and 4. We end the presentation of the semantics by emphasizing the effects of non-denoting and non-rigid constants. First, since c may not denote at a world w of a model M, it might happen that c satisfies no predicate at w, not even self-identity. Second, since constants might denote different objects at different worlds, we cannot use the information that the constants h and p denote the same object in w (say, h and p stand, respectively, for the names ‘Hesperus’ and ‘Phosphorus’, and both denote Venus in w) to conclude that they denote the same object in worlds accessible from w. The sentence λx.λy.x = y.p.h ⊃ 2(λx.λy.x = y.p.h) is not valid in models with non-rigid designators. This might seem incompatible with the fact that an unrestricted rule of replacement holds for identity. But identity atoms express a relation between variables and not between constants, which may only be applied to an identity via the operator λ. Thus, the rule of replacement allows only to substitute variables that denote the same object. The operator λ might be looked at as a device to block the permutation of substitutions and modalities for non-rigid constants, as is witness by axiom RG in Table 4. Finally, note that for y ∈ V AR, the formulas λx.A.y and A[y/x] are semantically equivalent. This holds because variables are rigid and always denoting terms. 3.2 Labelled Sequent Calculi In order to introduce labelled sequent calculi for QMLs with non-rigid and non-denoting indi- vidual constants, we extend the language of labelled calculi with ternary atomic expressions of w shape x ≈ t, which will be used to express that the variable x picks the object denoted in w by the term t. From now on, a sequent Ω; Γ ⇒ ∆ is an expression where Ω is a multiset of atomic w formulas of shape x ≈ t, x ∈ w or wRv; and Γ and ∆ are multisets of labelled Lλ -formulas. The rules of the calculus G3Qλ.K are the rules of G3Q.K, see Table 2, plus the rules for identity and the rules for λ of Table 5. Observe that the rules for identity contain the labelled version of the universal rules first introduced in [9]. When w : y = x holds, by Repl we can replace x with y in any atomic formula that, so to say, talks about w. The universal rule RigV ar implies that if x and y denote the same object in some world, they do so in each world. Thus, variables behave as rigid designators and labels could be omitted from identities. We choose to keep them in order to have a more uniform notation. The satisfaction clause for λx.A.t in a world w is similar to that for ∃xA, the only difference being that A has to be satisfied not by some arbitrary object of Dw , but by the one and only 7 70 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi Table 5: Additional rules for G3λ.L rules for identity: Ω; w : x = x, Γ ⇒ ∆ Ω; v : y = z, w : y = z, Γ ⇒ ∆ Ref= RigVar Ω; Γ ⇒ ∆ Ω; w : y = z, Γ ⇒ ∆ Ω, E[z/x], E[y/x], w : y = z, Γ ⇒ ∆ w Repl E is either xi ≈ t or xi ∈ w or w : p Ω, E[y/x], w : y = z, Γ ⇒ ∆, rules for λ: w w y ≈ t, Ω; Γ ⇒ ∆, w : λx.A.t, w : A[y/x] z ≈ t, Ω; w : A[z/x], Γ ⇒ ∆ Rλ Lλ, z fresh w Ω; w : λx.A.t, Γ ⇒ ∆ y ≈ t, Ω; Γ ⇒ ∆, w : λx.A.t w w y ≈ x, Ω; w : x = y, Γ ⇒ ∆ x ≈ x, Ω; Γ ⇒ ∆ DenId DenVar w Ω; Γ ⇒ ∆ y ≈ x, Ω; Γ ⇒ ∆ non-logical rules: v w w x ≈ t, x ≈ t, wRv, Ω; Γ ⇒ ∆ z ≈ t, Ω; Γ ⇒ ∆ Rig Tot, z fresh w Ω; Γ ⇒ ∆ x ≈ t, wRv, Ω; Γ ⇒ ∆ object of D that is denoted by t in that world of that model. Therefore the rules for λ are like w the ones for ∃, see [10], save that they are restricted by atomic formulas of shape y ≈ t instead of y ∈ w. The universal rule DenId ensures that if y in w picks the object denoted by x, then x and y denote the same object. Finally, the universal rule DenV ar ensures that variables denote at every world. The calculus G3Qλ.L is obtained by extending G3Qλ.K with the non-logical rules from Tables 3 and 5 that express the semantic properties defining Qλ.L. Example 4 (Derivation of axioms in Table 4). We show here that RG is derivable in calculi containing rule Rig (where rule R⊃ is admissible) and that T T is derivable in calculi containing rule T ot. These derivations also show that these formulas are not derivable in calculi without these rules when t is an individual constant. If t is a variable, T T is always derivable thanks to RigV ar, and RG is always derivable thanks to DenV ar, DenId, RigV ar, and Repl. Lem.5 v w y ≈ t, wRv, y ≈ t; v : A[y/x], w : 2A[y/x] ⇒ v : λx.A.t, v : A[y/x] Rλ v w y ≈ t, wRv, y ≈ t; v : A[y/x], w : 2A[y/x] ⇒ v : λx.A.t Rig w wRv, y ≈ t; v : A[y/x], w : 2A[y/x] ⇒ v : λx.A.t L2 w wRv, y ≈ t; w : 2A[y/x] ⇒ v : λx.A.t R2 w y ≈ t; w : 2A[y/x] ⇒ w : 2(λx.A.t) Lλ w : λx.2A.t ⇒ w : 2(λx.A.t) R⊃ ⇒ w : λx.2A.t ⊃ 2(λx.A.t) 8 71 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi w y ≈ t; w : y = y ⇒ w : λx.x = x.t, w : y = y Ref= w y ≈ t ⇒ w : λx.x = x.t, w : y = y Rλ w y ≈ t ⇒ w : λx.x = x.t Tot ⇒ w : λx.x = x.t 3.2.1 Structural Properties Lemma 5 (Initial sequents). Sequents of shape Ω; w : A, Γ ⇒ ∆, w : A (with A arbitrary Lλ -formula) are G3Qλ.L-derivable. Proof. By induction on the weight of A; for the inductive steps it is enough to apply, root first, the rules for the principal operator of A and then the inductive hypothesis (IH). Lemma 6 (α-conversion). G3Qλ.L `n Ω; Γ ⇒ ∆ entails G3Qλ.L `n Ω; Γ0 ⇒ ∆0 , where Γ0 (∆0 ) is obtained from Γ (∆) by renaming some bound variable (without capturing variables). Proof. The proof is by induction on the height of the G3Qλ.L-derivation D of Ω; Γ ⇒ ∆. To illustrate, suppose we know that G3Qλ.L `n Ω; w : λx.A.t, Γ ⇒ ∆, and we want to show that G3Qλ.L `n Ω; w : λy.A[y/x].t, Γ ⇒ ∆. If w : λx.A.t is not principal in the last step of D, the proof is straightforward. Else, we transform w z ≈ t, Ω; w : A[z/x], Γ ⇒ ∆ w w ? z ≈ t, Ω; w : A[z/x], Γ ⇒ ∆ z ≈ t, Ω; w : (A[y/x])[z/y], Γ ⇒ ∆) Lλ Lλ Ω; w : λx.A.t, Γ ⇒ ∆ into Ω; w : λy.A[y/x].t, Γ ⇒ ∆ where the step ? is height-preserving admissible since, having assumed that the renaming cannot capture variables, w : (A[y/x])[z/y] is just a cumbersome notation for w : A[z/x]. Lemma 7 (Substitutions). The following rules are height-preserving admissible in G3Qλ.L: Ω; Γ ⇒ ∆ Ω; Γ ⇒ ∆ [y/x ] [w /v ] Ω[y/x]; Γ[y/x] ⇒ ∆[y/x] Ω[w/v]; Γ[w/v] ⇒ ∆[w/v] where y is free for x in each formula occurring in Γ, ∆ for rule [y/x]. Proof. Both proofs are by induction on the height of the derivation D of the premiss Ω; Γ ⇒ ∆. The base cases and the inductive steps where the last rule is not a rule from Table 5 are proved in [10, Lemma 12.4]. Of the new cases, the only nontrivial one is the one for rule [y/x] where the last step is by Lλ and the substitution [y/x] clashes with its variable condition. E.g., the last step of D is w y ≈ t, Ω; w : A[y/x], Γ0 ⇒ ∆ Lλ Ω; w : λx.A.t, Γ0 ⇒ ∆ with x occurring free in Ω, Γ0 , ∆. We apply IH twice to the premiss of the last step of D, the first time to replace y with z, for some fresh variable z, and the second time to replace x with y. We finish by applying rule Lλ. We have thus transformed D into D[y/x]: 9 72 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi w y ≈ t, Ω; w : A[y/x], Γ0 ⇒ ∆ IH w z ≈ t, Ω; w : A[z/x], Γ0 ⇒ ∆ IH w z ≈ (t[y/x]), Ω[y/x]; w : A[z/x], Γ0 [y/x] ⇒ ∆[y/x] Lλ Ω[y/x]; w : λx.A.(t[y/x]), Γ0 [y/x] ⇒ ∆[y/x] which has the same height as D because the steps by IH are height-preserving admissible. Theorem 8 (Weakening). The following rules are height-preserving admissible in G3Qλ.L: Ω; Γ ⇒ ∆ Ω; Γ ⇒ ∆ Ω; Γ ⇒ ∆ LWΩ LW RW Ω0 , Ω; Γ ⇒ ∆ Ω; Γ0 , Γ ⇒ ∆ Ω; Γ ⇒ ∆, ∆0 Proof. The proofs are by induction on the height of the derivation D of the premiss Ω; Γ ⇒ ∆. The base cases and the inductive cases where the last step of D is not by a rule from Table 5 are proved in [10, Thm. 12.5]. The proofs of the inductive cases when the last step of D is by Lλ or by Rλ are analogous to the ones in [10, Thm. 12.5] with last step of D by rules L∃ and R∃, respectively. The remaining cases are similar to the other ones with last step by a geometric rule and can, therefore, be omitted. Lemma 9 (Invertibility). Each rule of G3Qλ.L is height-preserving invertible. Proof. We prove only the case of Lλ (Rλ is ‘Kleene’-invertible thanks to the repetition of the principal formulas in the premiss). The proof is by induction on the height of the derivation D of Ω; w : λx.A.t, Γ ⇒ ∆. If the height of D is 0 or if w : λx.A.t is principal in the last step of D, the lemma holds trivially. In the other inductive cases we obtain a derivation of w y ≈ t, Ω; w; A[y/x], Γ ⇒ ∆ (where y is any variable) by first applying to the premiss(es) of the last step of D an height-preserving admissible instance of substitution to avoid problems with variable conditions on the last step of D, if this is needed. Then, we apply IH to the sequent(s) just obtained and we finish by applying the last rule applied in D. Theorem 10 (Contraction). The following rules are height-preserving admissible in G3Qλ.L: Ω0 , Ω0 , Ω; Γ ⇒ ∆ Ω; Γ0 , Γ0 , Γ ⇒ ∆ Ω; Γ ⇒ ∆, ∆0 , ∆0 LCΩ LC RC Ω0 , Ω; Γ ⇒ ∆ Ω; Γ0 , Γ ⇒ ∆ Ω; Γ ⇒ ∆, ∆0 Proof. The proof is handled by a simultaneous induction on the height of the derivations of the premisses of LCw , LC and RC. Without loss of generality, we assume the multiset we are contracting is made of only one formula E. The base cases hold, and the inductive cases depend on whether zero, one, or two instances of E are principal in the last step R of the derivation D of the premiss. If zero instances are principal in R, we apply IH to the premiss(es) of R and then R, and we are done. If one instance is principal and R is by one of L¬, R¬, L∧, R∧, R∀, R2 and Lλ, we proceed by first applying invertibility to that rule, then we apply IH as many times as needed, and we conclude by applying an instance of that rule. Else, R is by a rule with repetition of the principal formula(s) in the premiss and we don’t even need invertibility. If two instances are principal, R is one of Euclid, T rans, and Repl. The case of Euclid is taken care by the presence of its contracted instances Euclidc . For T rans, we have three occurences of wRw in the premiss of this rule instances: two principal and one active. We apply IH twice and we are done. For Repl, the active formula of the last rule instance must be of shape w : x = x, and, after having applied IH, we can get rid of it by applying Ref= . 10 73 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi Theorem 11 (Cut). The following rule of Cut is admissible in G3Q.L: Ω; Γ ⇒ ∆, w : A Ω0 ; w : A, Γ0 ⇒ ∆0 Cut Ω, Ω0 ; Γ0 , Γ ⇒ ∆, ∆0 Proof. The proof, which extends that of [10, Thm. 12.9], considers an uppermost instance of Cut which is handled by a principal induction on the weight of the cut-formula w : A with a sub-induction on the sum of the heights of the derivations D1 and D2 of the two premisses of cut (cut-height, for shortness). The proof can be organized in four exhaustive cases: in case 1 one of the two premisses is an initial sequent. In case 2 the cut formula is not principal in the left premiss only and in case 3 it is not principal in the right premiss. Finally, in case 4, the cut formula is principal in both premisses. In case 1, the conclusion of Cut is an initial sequent and, therefore, we can dispense with that instance of Cut. In case 2, we transform the derivation by: (i) applying, if the last rule applied in D1 has a variable condition, an height-preserving admissible substitution to rename its eigenvariable with a fresh one; then, (ii) we apply one or two instances of Cut on each premiss of D1 with the conclusion of D2 . These instances of Cut are admissible by IH because they have a lesser cut-height. We finish (iii) by applying an instance of the last rule applied in D1 and, if needed, some instances of contraction. Case 3 is similar to case 2. To illustrate, suppose the last step of D2 is by Lλ, we transform v y ≈ t, Ω0 ; w : A, v : B[y/x], Γ0 ⇒ ∆0 Lλ Ω; Γ ⇒ ∆, w : A Ω0 ; w : A, v : λx.B.t, Γ0 ⇒ ∆0 Cut Ω, Ω0 ; v : λx.B.t, Γ0 , Γ ⇒ ∆, ∆0 into v y ≈ t, Ω0 ; w : A, v : B[y/x], Γ0 ⇒ ∆0 [z /y] v Ω; Γ ⇒ ∆, w : A z ≈ t, Ω0 ; w : A, v : B[z/x], Γ0 ⇒ ∆0 Cut v z ≈ t, Ω, Ω0 ; v : B[z/x], Γ, Γ0 ⇒ ∆, ∆0 Lλ Ω, Ω0 ; v : λx.B.t, Γ0 , Γ ⇒ ∆, ∆0 In case 4, we have subcases according to the principal operator of w : A. We consider only the case where w : A is of shape w : λx.B.t (for w : A of shape either w : B ∧ C or w : ∀xB or w : 2B, see [10, Thm. 12.9]; when it is of shape w : ¬B there is no problem). We transform v v z ≈ t, Ω; Γ ⇒ ∆, v : λx.B.t, v : B[z/x] y ≈ t, Ω0 ; v : B[y/x], Γ0 ⇒ ∆0 Rλ Lλ v z ≈ t, Ω; Γ ⇒ ∆, v : λx.B.t Ω0 ; v : λx.B.t, Γ0 ⇒ ∆0 cut v z ≈ t, Ω, Ω0 ; Γ0 , Γ ⇒ ∆, ∆0 into v v z ≈ t, Ω; Γ ⇒ ∆, v : B[z/x], v : λx.B.t Ω0 ; v : λx.B.t, Γ0 ⇒ ∆0 y ≈ t, Ω0 ; v : B[y/x], Γ0 ⇒ ∆0 Cut1 [z /y] v v z ≈ t, Ω, Ω0 ; Γ ⇒ ∆, ∆0 , v : B[z/x] z ≈ t, Ω0 ; v : B[z/x], Γ0 ⇒ ∆0 Cut2 v v z ≈ t, z ≈ t, Ω, Ω0 , Ω0 , ; Γ0 , Γ ⇒ ∆, ∆0 , ∆0 LCΩ +LC +RC v z ≈ t, Ω, Ω0 ; Γ0 , Γ ⇒ ∆, ∆ where Cut1 is admissible because it has a lesser cut-height, and Cut2 is admissible because its cut-formula has a lower weight. 11 74 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi 3.2.2 Soundness and Completeness Definition 12. Given a model M =< W, R, D, V >, let f : LAB ∪ V AR −→ W ∪ D be a function mapping labels to worlds of the model and mapping variables to objects of the union of the domains of the model. We say that: M satisfies w : A under f iff f |=Mf (w) A M satisfies x ∈ w under f iff f (x) ∈ Df (w) M satisfies wRv under f iff f (w)Rf (v)  w V (t, f (w)) = f (x) if t is an individual constant; M satisfies x ≈ t under f iff f (t) = f (x) if t is a variable; Given a sequent Ω; Γ ⇒ ∆ we say that it is Qλ.L-valid iff for every pair M, f where M is a model for Qλ.L, if M satisfies under f all formulas in Ω, Γ then M satisfies under f some formula in ∆. Theorem 13 (Soundness). If a sequent Ω; Γ ⇒ ∆ is G3Qλ.L-derivable, then it is Qλ.L-valid. Proof. The proof is by induction on the height of the G3Qλ.L-derivation of Ω; Γ ⇒ ∆. The base case holds since Γ and ∆ have one formula in common, and it is easy to see that the propositional rules, the rules for ∀, and the rules for 2 preserve validity on every model. For rule Lλ, let the last step of D be: w y ≈ t, Ω; w : A[y/x], Γ ⇒ ∆ Lλ Ω; w : λx.A.t, Γ ⇒ ∆ Let M and f be such that M satisfies under f all formulas in Ω, Γ and the formula w : λx.A.t. We have to prove that M satisfies under f also some formula in ∆. Since f |=M f (w) λx.A.t, y.a M we know that, in f (w), the term t denotes some object a ∈ D and that f |=f (w) A[y/x], where y does not occur in Ω, Γ, A. This implies that M satisfies under f y.a all formulas in w y ≈ t, Ω; w : A[y/x], Γ, and therefore, by IH, M satisfies under f y.a also some formula in ∆. Since y does not occur in ∆, we conclude that M satisfies under f some formula in ∆. For rule Rλ, let the last step of D be: w y ≈ t, Ω; Γ ⇒ ∆, w : λx.A.t, w : A[y/x] Rλ w y ≈ t, Ω; Γ ⇒ ∆, w : λx.A.t w We consider an arbitrary pair M, f satisfying all formulas in y ≈ t, Ω, Γ. By IH we know that they satisfy also some formula in ∆, w : λx.A.t, w : A[y/x]. If they satisfy some formula in ∆, w : λx.A.t there is nothing to prove. Else, M satisfies under f the formulas w : A[y/x] and w y ≈ t, in this case it is easy to see that M satisfies under f also λx.A.t. The rules for identity preserves validity on every model: the proof is standard for rules Ref= and Repl, and for RigV ar, it depends on the fact that variables are rigid designators. Also the rules DenV ar and DenId preserves validity on every model. For DenV ar this depends on the fact that variables denote in every world. For DenId, this holds because the fact that M w satisfies y ≈ x under f means that f (x) = f (y). Therefore, M must also satisfy under f the formula w : x = y. If the last step in D is by a non-logical rule R of G3Qλ.L, we can show that R preserves Qλ.L-validity. To illustrate, if R is Rig, we consider a model M where constants are rigid designators, see Table 4. Given a generic f such that M satisfies under f all formulas in 12 75 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi w wRv, x ≈ t, Ω, Γ. We have to prove that M satisfies under f also some formula in ∆. By v rigidity, M satisfies under f also x ≈ t and, by IH, we conclude that it satisfies some formula in ∆. Theorem 14 (Completeness). If a sequent Ω; Γ ⇒ ∆ is Qλ.L-valid, it is G3Qλ.L-derivable. Proof. The proof is organized in four main steps. First, in Def. 15, we sketch a root-first G3Qλ.L-proof-search procedure. Second, in Def. 16, we define the notion of saturation for a branch of a G3Qλ.L-proof-search tree and, in Proposition 17, we show that, for every sequent, a G3Qλ.L-proof-search either gives us a G3Qλ.L-derivation of that sequent, or it has a saturated branch. Third, in Def. 19, we define a model MB out of a saturated branch B. Finally, in Lemma 20, we prove that MB is a model for Qλ.L that falsifies Ω; Γ ⇒ ∆. Definition 15. A G3Qλ.L-proof-search tree for a sequent Ω; Γ ⇒ ∆ is a tree of sequents generated according to the following inductive procedure. At step 0 we write the one node tree Ω; Γ ⇒ ∆. At step n + 1, if all leaves of the tree generated at step n are initial sequents, the procedure ends. Else, we continue the bottom-up construction by applying, to each leaf that is not an initial sequent, each applicable instance of a rule of G3Qλ.L or, if no rule instance is applicable, we copy the leaf on top of itself. For rules Ref= , RefW , Ser, N onEm, Cons, DenV ar and T ot, we consider applicable only instances where, save for eigenvariables, all terms and labels occurring in the active formula of that instance already occur in the leaf. See [10, Thm. 12.14] for the details of the inductive procedure. Definition 16 (Saturation). A branch B of a G3Qλ.L-proof-search tree for a sequent is QλL- saturated if it satisfies the following conditions, where Γ (∆) is the union of the antecedents (succedents) occurring in that branch, 1. no w : p occurs in Γ ∩ ∆; 2. if w : ¬A is in Γ, then w : A is in ∆; 3. if w : ¬A is in ∆, then w : A is in Γ; 4. if w : A ∧ B is in Γ, then both w : A and w : B are in Γ; 5. if w : A ∧ B is in ∆, then at least one of w : A and w : B is in ∆; 6. if both w : ∀xA and y ∈ w are in Γ, then w : A(y/x) is in Γ; 7. if w : ∀xA is in ∆, then, for some z, w : A(z/x) is in ∆ and z ∈ w is in Γ; 8. if both w : 2A and wRv are in Γ, then v : A is in Γ; 9. if w : 2A is in ∆, then, for some u, u : A is in ∆ and wRu is in Γ; w 10. if w : λx.A.t is in Γ, then, for some z, both z ≈ t and w : A[z/x] are in Γ; w 11. if w : λx.A.t is in ∆ and y ≈ t is in Γ, then w : A[y/x] is in ∆; 12. if the principal formulas of some instance of one of Ref= , Repl, RigV ar, DenV ar, and DenId is in Γ, then also the corresponding active formulas are in Γ. 13R . if R is a non-logical rule of G3tm.L, then for each set of principal formulas of R that are in Γ also the corresponding active formulas are in Γ (for some eigenvariable of R, if any). 13 76 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi Proposition 17. Let us consider a G3Qλ.L-proof-search tree for a sequent S, two cases are possible: either the tree is finite or not. If the tree is finite, given that all of its leaves are initial sequents and that it grows by applying rules of G3Qλ.L, it is a G3Qλ.L-derivation of S and, by Theorem 13, S is Qλ.L-vaild. Else, by König’s Lemma, the tree has an infinite branch B that is Qλ.L-saturated since every applicable rule instance has been applied at some step of the construction of the tree. Proposition 18. It is immediate to notice that, by saturation under rule Ref= and Repl the set of variables x, y such that w : x = y is in Γ form an equivalence class and that, by saturation under RigV ar, the same equivalence class holds with respect to each label v occurring in Γ, ∆. Definition 19. Let B be a saturated branch of a G3Qλ.L-proof-search tree for a sequent. The model MB =< W B , RB , DB , V B > is defined from B as follows: • W B is the set of all labels occurring in B; • RB is such that wRv iff wRv occurs in B; • DB is such that, for each w ∈ W B , Dw is the set containing, for each variable x such that x ∈ w occurs in B, the equivalence class [x] of all x, y such that w : x = y occurs in B; • V M is defined as follows: – for every predicate P n ∈ S λ , V (P n , w) is the set of all n-tuples of equivalence classes of variables < [x1 ], . . . , [xn ] > such that w : P x1 , . . . , xn occurs in Γ; w – for every constant c ∈ S λ , V (c, w) is [x] if x ≈ c occurs in Γ, else it is undefined. Lemma 20. If MB is the model defined from a saturated branch B of a G3Qλ.L-proof-search tree for a sequent Ω; Γ ⇒ ∆ and σ is the assignment defined by σ(x) = [x], then, for each labelled formula w : A occurring in B, B 1. σ |=M w A iff w : A occurs in Γ 2. MB is a model for Qλ.L. Proof. The proof of claim 1 is by induction on the weight of w : A. The base case holds thanks to the definition of V B , and the inductive cases depends on the construction of MB and on properties 2–12 of the definition of saturated branch. To illustrate, suppose w : A ≡ w : λxB.t. If w : A occurs in Γ, then, by Def. 16.10, for some w z, z ≈ t and w : B[z/x] are in Γ. This implies that σw (t) = [z] and, by IH, that σ x.[z] |=B w B. w Thus, σ |=B w λx.B.t. Else, w : λx.B.t is in ∆ and, for each t such that y ≈ t is in Γ (if any), Def. 16.11 entails that w : B[y/x] is in ∆. By construction we have that that σw (t) = [y] and, B B thanks to IH (and 16.1), σ x.[y] 6|=Mw B. We conclude that σ 6|=Mw λx.B.t. Claim 2 holds thanks to property 13R of saturated branch: if a non-logical rule R is in G3Qλ.L, then we have to show that MB satisfies the semantic property corresponding to R. This holds by construction of MB since B is saturated with respect to rule R. For example, for rule Rig, we have to prove that wRB v and sw (t) ∈ DB – i.e., sw (t) is defined in MB – implies that sv (t) = σw (t). Suppose that wRv is in Γ, if t is a variable, then, 16.12 entails that, for all w v y, if y ≈ t is in Γ, then, also y ≈ t is in Γ (by saturation under DenV ar, DenId, RigV ar, and w Repl). Else, t is a constant and if, for some y, y ≈ t is in Γ, saturation under rule Rig entails v that y ≈ t is in Γ. In both cases MB behaves as desired. 14 77 Labelled calculi for QMLs with non-rigid and non-denoting terms Orlandelli and Corsi 4 Conclusion We have introduced labelled sequent calculi that characterize the QMLs with non-rigid and non- denoting terms introduced in [6, 7], and we have studied their structural properties. To the best of our knowledge, this is the first proof-theoretic study of these logics. In [6, 7] prefixed tableaux for these logics have been considered, but there is no study of their structural properties. Notice that, even if we have considered only the Qλ-extensions of propositional modal logics L in the cube of normal modalities, the present approach can be extended, in a modular way, to the Qλ-extensions of any propositional modal logic whose class of models is defined by first-order definable modal logics (by applying, if needed, the geometrisation technique introduced in [5]). For example, we can introduce a calculus characterizing validity in the class of all constant domain models satisfying confluence: ∀w, v, u ∈ W(wRv ∧ wRu ⊃ ∃w0 ∈ W(vRw0 ∧ uRw0 ). From [4], we know that confluence corresponds to Geach’s axiom 2 := 32A ⊃ 23A and that the quantified modal axiomatic system Q.2 ⊕ BF is incomplete with respect to the class of all confluent constant domain models. Nevertheless, confluence is a geometric property, and it can be expressed in labelled calculi by the rule: vRw0 , uRw0 , wRv, wRu, Ω; Γ ⇒ ∆ Conf , w 0 fresh wRv, wRu, Ω; Γ ⇒ ∆ It can be proved that the labelled calculus G3Qλ.K+{Cons, Conf } is sound and complete with respect to the class of confluent constant domain models. The calculi introduced here are somehow related to the ones we gave in [3] for the indexed epistemic logics studied in [2]. The QMLs studied here are less general than the ones in [2], but they have the advantage of being simpler and of involving no major departure from the standard modal language. Therefore the present approach to non-rigid and non-denoting terms can easily be extended to most variants of QMLs. For example, it carries over to labelled calculi for term-modal logics [11]. References [1] Agata Ciabattoni, Revantha Ramanayake, and Heinrich Wansing. Hypersequent and display cal- culi - a unified perspective. Studia Logica, 102(6):1245–1294, 2014. [2] Giovanna Corsi and Eugenio Orlandelli. Free quantified epistemic logics. Studia Logica, 101(6):1159–1183, 2013. [3] Giovanna Corsi and Eugenio Orlandelli. Sequent calculi for indexed epistemic logics. In Proceedings of ARQNL 2016, pages 21–35. CEUR-WS, 2016. [4] Max Cresswell. Incompleteness and the barcan formula. J. Phil. Logic, 24(4):379–403, 1995. [5] Roy Dyckhoff and Sara Negri. Geometrisation of first-order logic. Bulletin of Symbolic Logic, 21(2):123–163, 2015. [6] Melvin Fitting. On quantified modal logic. Fundamenta Informaticae, 39(1–2):105–121, 1999. [7] Melvin Fitting and Richard L. Mendelsohn. First-Order Modal Logic. Springer, 1998. [8] Gottlob Frege. Über sinn und bedeutung. Zeitschrift für Philosophie Und Philosophische Kritik, 100(1):25–50, 1892. [9] Sara Negri and Jan von Plato. Cut elimination in the presence of axioms. Bullettin of Symbolic Logic, 4(4):418–435, 1998. [10] Sara Negri and Jan von Plato. Proof Analysis. Cambridge University Press, 2011. [11] Eugenio Orlandelli and Giovanna Corsi. Decidable term-modal logics. In Proceedings of EUMAS 2017 and AT 2017, pages 1–15. Springer, Forthcoming. [12] Bertrand Russell. On denoting. Mind, 14(56):479–493, 1905. 15 78