Proof-Theory and Semantics for a Theory of Definite Descriptions

Abstract

This paper presents a sequent calculus and a dual domain semantics for a theory of definite descriptions in which these expressions are formalised in the context of complete sentences by a binary quantifier I. I forms a formula from two formulas. Ix[F, G] means ‘The F is G’. This approach has the advantage of incorporating scope distinctions directly into the notation. Cut elimination is proved for a system of classical positive free logic with I and it is shown to be sound and complete for the semantics. The system has a number of novel features and is briefly compared to the usual approach of formalising ‘the F’ by a term forming operator. It does not coincide with Hintikka’s and Lambert’s preferred theories, but the divergence is well-motivated and attractive.

The research in this paper was funded by the Alexander von Humboldt Foundation.

1 Introduction

A definite description is an expression of the form ‘the F’. Accordingly, the most popular formalisations of the theory of definite descriptions treat them as term forming operators: the operator $\iota$ binds a variable and turns an open formula into a singular term $\iota xF$. This treatment of definite descriptions goes back to Whitehead and Russell [34].¹ Whitehead and Russell, however, did not consider definite descriptions to be genuine singular terms: they only have meaning in the context of complete sentences in which they occur and disappear upon analysis: ‘The F is G’ is logically equivalent to ‘There is one and only one F and it is G’. Following the work of Hinitkka [12] and Lambert [25], many logicians prefer to formalise definite descriptions in a fashion where they are not straightforwardly eliminable. In such systems, $\iota$ is governed by what has come to be called Lambert’s Law:

The preferred logic of many free logicians is positive free logic, where formulas containing names that do not refer (to objects considered amongst those that exist) may be true. Then ‘The F is G’ is no longer equivalent to ‘There is one and only one F and it is G’. In negative free logic, all atomic formulas containing non-denoting terms are false, and the Russellian analysis is again appropriate.

There is agreement amongst free logicians that (LL) formalises the minimal theory of definite descriptions. Lambert himself prefers a stronger theory [26] that in addition has the axiom:²

There are a number of other axioms that have been considered, but these two will be the focus of the present investigation.³ The proof theory of the theory of definite descriptions has received close study from the hands of Andrzej Indrzejczak.⁴ In a series of papers, Indrzejczak has investigated various formalisations of theories of definite descriptions and provided cut free sequent calculi for them [14,15,16,17, 19]. A cut free system of positive free logic of his will form the background to the present paper. It is presented in the next section.

Whitehead and Russell also note the need for marking scope distinctions to formalise the difference between ‘The F is not G’ and ‘It is not the case that the F is G’. Free definite description theory in general ignores scope: the thought is that free logic says only very little about definite descriptions when they do not refer, and in case they do refer, scope distinctions no longer matter, as already pointed out by Whitehead and Russell.

Scope distinctions are, however, worth considering. The present paper proposes a proof-system and a semantics for a theory of definite descriptions in which scope distinctions are incorporated directly into the symbolism. ‘The F is G’ is formalised by a binary quantifier that takes two formulas and forms a formula Ix[F, G] out of them. The notation is taken from Dummett [5, p.162]. It is also found in the work of Neale [31] and Bostock [2, Sec. 8.4]. The external negation ‘It is not the case that the F is G’ is formalised by $\lnot Ix[F, G]$, the internal negation ‘The F is not G’ by $Ix[F, \lnot G]$. Natural deduction proof-systems for this approach have been investigated by the present author in the context of intuitionist non-free as well as negative and positive free logic [20, 21, 23]. Rules suitable for a sequent calculus for classical positive free logic were formulated in [22].⁵ The latter system and its intuitionist counterpart were devised with the intention to stay close to the systems of Hintikka and Lambert. The results are rather complicated: I is governed by six rules, one right or introduction rule and five left or elimination rules. Despite their complexities, the systems remain proof-theoretically satisfactory as cut elimination and normalisation theorems hold for them. The present paper severs the ties to Hintikka and Lambert and considers alternative rules for I within classical positive free logic. The account proposed here is rather simpler than the previous ones: I is governed by one right rule, the same as before, but only two left rules. The result is a rather different formal theory from the perspective of the validities provable from the rules and compared to Hintikka’s and Lambert’s: the rules enforce the uniqueness of F, if Ix[F, G] is true, but not its existence. The novelty of the present paper lies in the addition of these new rules for I to classical positive free logic,⁶ the ensuing alternative theory of definite descriptions, and the provision of a sound and complete dual domain semantics for it.

The plan of this paper is as follows. The next section expounds Indrzejczak’s sequent calculus formulation of classical positive free logic extended by rules governing the binary quantifier I. Section 3 discusses consequences of the theory and compares it to Hintikka’s and Lambert’s. Due to the absence of scope distinctions in axiomatisations of $\iota$ based on (LL), a direct comparison between the system proposed here and standard formalisations of definite descriptions is not very illuminating: $G(\iota xF)$ has no direct and natural correspondent, as $\lnot G(\iota xF)$ corresponds to two formulas, the internal and the external negation of Ix[F, G]. Nonetheless, it is worth examining how the binary fares with respect to analogues of(LL) and (FL), when $\iota xA=y$ is rendered as a binary quantification $Ix[A, x=y]$. The latter formalises ‘The A is identical to y’, or ‘The A is y’ for short, which is exactly the reading one may give of $\iota xA=y$. To anticipate, while an analogue of (FL) is derivable in the system proposes here, only half of an analogue of (LL) is. Section 4 proves that cut is still eliminable from the extended system. Section 5 gives a formal semantics for classical positive free logic extended by I. Section 6 proves the soundness and completeness of the system. Some details of the completeness proof are relegated to the appendix for the online version of this paper [24]. Section 7 gives rules tableaux proof system.

2 A Deductive Calculus for Classical Positive Free Logic with a Binary Quantifier

Indrzejczak has provided a formalisation of classical positive free logic CPF in sequent calculus with desirable proof-theoretic properties: cut is eliminable from the system [18]. The definition of the language is standard. I will only consider $\rightarrow$, $\lnot$, $\forall$ and a distinguished predicate symbol $\exists !$, the existence predicate, as primitives.⁷ $\wedge$, $\vee$, $\exists$ are defined as usual. Free variables are distinguished from bound ones by the use of parameters $a, b, c\ldots$ for the former and $x, y, z \ldots$ for the latter. $t_1, t_2, t_3\ldots$ range over the terms of the language, which are the parameters, constants, and complex terms formed from them and function symbols. For brevity I will write F or A instead of F(x) or A(x) etc., except in the case of the existence predicate, where I’ll write $\exists !x$ etc. $A_t^x$ is the result of substituting t for x in A, where it is assumed that no variable free in t becomes bound in $A_t^x$, i.e. that t is free for x in A. $\varGamma , \varDelta$ denote finite multisets of formulas. The rules of CPF are as follows:

where in $(R\forall )$, a does not occur in the conclusion, and in $(L\forall )$, t is substitutable for x in A. In $(=I)$, A is atomic. The general case follows by induction.

To these we add rules for the binary quantifier I:

where in (RI) and $(LI^1)$, a does not occur in the conclusion, and in $(LI^2)$ C is an atomic formula. The general case follows by induction.

Vacuous quantification with I is allowed. If x is not free in A, then the truth of Ix[A, B] requires or imposes a restriction on the domain: if there is only one object (existing or not), then, if A is true and B is true (of the object in the domain, if x is free in B), then Ix[A, B] is true; and if Ix[A, B] is true, then, if A is true, then there is only one object in the domain and B is true (of it, if x is free in B). If x is not free in B, then Ix[A, B] is true if and only if a unique object (existing or not) is A and B is true.

Call the resulting system $\mathbf {CPF}^I$. Deductions are defined as usual, as certain trees with axioms at the top-nodes or leaves and the conclusion at the bottom-node or root. If a sequent $\varGamma \Rightarrow \varDelta$ is deducible in $\mathbf {CPF}^I$, we write $\vdash \varGamma \Rightarrow \varDelta$.

3 Consequences of the Formalisation

Call two formulas $\iota xA=y$ and $Ix[A, x=y]$ analogues of each other. They both formalise the same sentence ‘The A is identical to y’. Similarly for $B(\iota xA)$ and Ix[A, B], where we restrict B to atomic formulas to avoid complications regarding scope. Let $\mathbf {CPF}^\iota$ be $\mathbf {CPF}$ plus (LL) and (FL). Analogues provide a convenient means for comparisons between $\mathbf {CPF}^I$ and $\mathbf {CPF}^\iota$.

First we state the obvious. The Law of Identity $\Rightarrow t=t$ and Leibniz’ Law $t_1=t_2, A_{t_2}^x \Rightarrow A_{t_1}^x$ are derivable in CPF:

$t_1=t_2, A_{t_1}^x \Rightarrow A_{t_2}^x$ of course also holds, as established by step two of the left deduction through interchanging $t_1$ and $t_2$.

Leibniz’ Law is no longer applicable to definite descriptions in the present framework, as definite descriptions are not analysed as singular terms but only in the context of complete sentences in which they occur. We can, however, mimic its use, as we can derive the sequents $Ix[A, x=t], B_t^x\Rightarrow Ix[A, B]$, $Ix[A, x=t], Ix[A, B],\Rightarrow B_t^x$ and $Ix[A, Iy[B, x=y]], Ix[A, C]\Rightarrow Ix[B, C]$. Using analogues, these correspond to instances of Leibniz’ Law: $\iota xA=t, B_t^x\Rightarrow B(\iota xA)$, $\iota xA=t, B(\iota xA),\Rightarrow B_t^x$ and $\iota xA=\iota yB, C(\iota xA)\Rightarrow C(\iota yB)$. We’ll prove the first for purposes of illustration. Double lines indicate applications of structural rules, in particular those needed to make the contexts of the rules identical by Thinning. Let $\varPi$ be the following deduction in $\mathbf {CPF}^I$:

Then the following establishes the analogue of our instance of Leibniz’ Law:

To assess whether (LL) is provable, it is useful to have rules for the biconditional:

These are derivable from the rules for $\rightarrow$ given the usual definition of $\leftrightarrow$.

Next we derive one half of an analogue of (LL) in $\mathbf {CPF}^I$:

The left and rightmost leaves are derivable by Leibniz’ Law.

The other half of (LL) is not derivable in $\mathbf {CPF}^I$. Intuitively, there being a unique existing A is not sufficient for Ix[A, B], as there may also be non-existing As in addition. It is straightforward to give a countermodel with the semantics of Sect. 5.

$\Rightarrow Ix[x=t, x=t]$ follows by twice the Law of Identity and one application of (RI), where both A and B are $x=t$:

Thus the analogue of (FL) is derivable in $\mathbf {CPF}^I$. This is worth noting: Lambert calls (FL) ‘an important theorem in traditional description theory’ [26, p. 58], and, not being derivable in the minimal theory, is forced to add it as a further axiom.

The present theory of definite descriptions is thus not comparable to Hintikka’s and Lambert’s minimal theory: it contains only one half of the analogue (LL), but also the analogue of (FL). The first respect provides a sense in which the present theory is weaker than Lambert’s preferred theory, the second one in which it is stronger, because the rules for I and $=$ yield the analogue of (FL) immediately, while in Lambert’s theory, (FL) needs to be added as an extra axiom governing the definite description operator $\iota$. The novelty of the present theory is shown by these features. In particular, the failure of the right to left half of (LL) is, arguably and pace Hintikka and Lambert, desirable, for the reason stated.

The theory does not allow the derivation of the analogue of $\iota xF=\iota xF$, $Ix[F, Iy[F, x=y]]$. This is a tolerable loss. As Russell is not identical to Whitehead, it is not difficult to accept that ‘The author of Principia Mathematica $=$ the author of Principia Mathematica’ is not logically true. Reasons normally given for accepting $\iota xF=\iota xF$ is that it is an instance of the Law of Identity. These reasons, however, are not conclusive, as the example shows. $Ix[F, Iy[F, x=y]]$ is not an instance of the Law of Identity, and hence accepting that law does not force us to accept it. If more than two objects satisfy F, then it is false.

Its differences to Hintikka’s and Lambert’s theory of definite descriptions are advantages of the present proposal. It allows us to reject the claim that the author of Principia Mathematica is identical to the author of Principia Mathematica and to declare ‘The author of Principia Mathematica smokes a pipe’ to be false. If there is more than one A, existing or not, then Ix[A, B] is false, whatever B may be: an identity, a predicate letter, a complex formula. The present theory provides principled reasons for declaring certain sentences containing definite descriptions to be false on which Hintikka and Lambert prefer to remain silent and for not having to accept some sentences they pronounce as logically true on grounds which one may well want to reject.

4 Cut Elimination for $\mathbf {CPF}^I$

We’ll continue Indrzejczak’s proof of cut elimination for $\mathbf {CPF}$ by adding the cases covering I. Let d(A) be the degree of the formula A, that is the number of connectives occurring in it. $\exists ! t$ is atomic, that is of degree 0. $d(\mathcal {D})$ is the degree of the highest degree of any cut formula in deduction $\mathcal {D}$. $A^k$ denotes k occurrences of A, $\varGamma ^k$ k occurrences of the formulas in $\varGamma$. The height of a deduction is the largest number of rules applied above the conclusion, that is the number of nodes of a longest branch in the deduction. The proof appeals to the Substitution Lemma:

Lemma 1

If $\vdash _k \varGamma \Rightarrow \varDelta$, then $\vdash _k \varGamma _t^a\Rightarrow \varDelta _t^a$.

Its proof goes through as usual. Consequently, we can always rewrite deductions so that each application of $(R\forall )$, (RI) and $(LI^1)$ has its own parameter that occurs nowhere else in the proof. In the following, it will be tacitly assumed that deductions have been treated accordingly.

Lemma 2

(Right Reduction). If $\mathcal {D}_1\vdash \varTheta \Rightarrow \varLambda , A$, where A is principal, and $\mathcal {D}_2\vdash A^k, \varGamma \Rightarrow \varDelta$ have degrees $d(\mathcal {D}_1), d(\mathcal {D}_2)<d(A)$, then there is a proof $\mathcal {D}\vdash \varTheta ^k, \varGamma \Rightarrow \varLambda ^k, \varDelta$ with $d(\mathcal {D})<d(A)$.

Proof. By induction over the height of $\mathcal {D}_2$. The basis is trivial: if $d(\mathcal {D}_2)=1$, then $A^k, \varGamma \Rightarrow \varDelta$ is an axiom and hence $k=1$, $\varGamma$ is empty, and $\varDelta$ consists of only one A; we need to show $\varTheta \Rightarrow \varLambda , A$, but that is already proved by $\mathcal {D}_1$.

For the induction step, we consider the rules for I:

(I) The last step of $\mathcal {D}_2$ is by (RI). Then the occurrences $A^k$ in the conclusion of $\mathcal {D}_2$ are parametric and occur in all three premises of (RI): apply the induction hypothesis to them and apply (RI) afterwards. The result is the desired proof $\mathcal {D}$.

(II) The last step of $\mathcal {D}_2$ is by $(LI^1)$. There are two options:

(II.a) If the principal formula Ix[F, G] of $(LI^1)$ is not one of the $A^k$, then apply the induction hypothesis to the premises of $(LI^1)$ and then apply $(LI^1)$.

(II.b) If the principal formula Ix[F, G] of $(LI^1)$ is one of the $A^k$, then $\mathcal {D}_2$ ends with:

By induction hypothesis there is a deduction of $F_a^x, G_a^x, \varTheta ^{k-1}, \varGamma \Rightarrow \varLambda ^{k-1}, \varDelta$ with cut degree less than d(A), and by the Substitution Lemma:

(1) $F_t^x, G_t^x, \varTheta ^{k-1}, \varGamma \Rightarrow \varLambda ^{k-1}, \varDelta$

A, i.e. Ix[F, G], is principal in $\mathcal {D}_1$, so it ends with an application of (RI):

Apply two cuts with (1) and the first and second premise, and conclude by contraction $\varTheta ^k, \varGamma \Rightarrow \varLambda ^k, \varDelta$.

(III) The last step of $\mathcal {D}_2$ is by $(LI^2)$. In this case the succedent of the conclusion of $\mathcal {D}_2$ is $\varDelta , C_{t_1}$, where $C_{t_1}$ is an atomic formula. There are two cases.

(III.a) The principal formula Ix[F, G] of $(LI^2)$ is not one of the $A^k$: apply the induction hypothesis to the premises of $(LI^2)$ and then apply the rule.

(III.b) The principal formula Ix[F, G] of $(LI^2)$ is one of the $A^k$. Then $\mathcal {D}_2$ ends with:

By induction hypothesis, we have:

• (1) $\varTheta ^{k-1}, \varGamma \Rightarrow \varLambda ^{k-1}, \varDelta , F_{t_1}^x$

• (2) $\varTheta ^{k-1}, \varGamma \Rightarrow \varLambda ^{k-1}, \varDelta , F_{t_2}^x$

• (3) $\varTheta ^{k-1}, \varGamma \Rightarrow \varLambda ^{k-1}, \varDelta , C_{t_2}^x$

A, i.e. Ix[F, G], is principal in $\mathcal {D}_1$, so it ends with an application of (RI):

The Substitution Lemma applied to the third premise gives

• (5) $F_{t_1}^x, \varTheta \Rightarrow \varLambda , t_1=t$

• (6) $F_{t_2}^x, \varTheta \Rightarrow \varLambda , t_2=t$

To show: $\vdash \varTheta ^k, \varGamma \Rightarrow \varLambda ^k, \varDelta , C_{t_1}$ with $d(\mathcal {D})<d(Ix[F, G])$. Leibniz’ Law gives

• (7) $t_1=t, t_2=t\Rightarrow t_1=t_2$

• (8) $C_{t_2}, t_1=t_2\Rightarrow C_{t_1}$

Cuts with (1) and (5) and with (2) and (6) give $\varTheta ^k, \varGamma \Rightarrow \varLambda ^k, \varDelta , t_1=t$ and $\varTheta ^k, \varGamma \Rightarrow \varLambda ^k, \varDelta , t_2=t$, whence by Cut with (7) and contraction $\varTheta ^k, \varGamma \Rightarrow \varLambda ^k, \varDelta , t_1=t_2$, and from the latter by Cuts with (3) and (8) and contraction $\varTheta ^k, \varGamma \Rightarrow \varLambda ^k, \varDelta , C_{t_1}$. As $C_{t_2}$ in $(LI^2)$ is restricted to atomic formulas, the degree of the ensuing deduction is less than d(A), i.e. d(Ix[F, G]), which was to be proved.

This completes the proof of the Right Reduction Lemma.

Lemma 3

(Left Reduction). If $\mathcal {D}_1\vdash \varGamma \Rightarrow \varDelta , A^k$ and $\mathcal {D}_2\vdash A, \varTheta \Rightarrow \varLambda$ have degrees $d(\mathcal {D}_1), d(\mathcal {D}_2)<d(A)$, then there is a proof $\mathcal {D}\vdash \varGamma , \varTheta ^k\Rightarrow \varDelta , \varLambda ^k$ with $d(\mathcal {D})<d(A)$.

Proof by induction over the height of $\mathcal {D}_1$. The basis is trivial, as then $\mathcal {D}_1$ is an axiom, and $\varGamma$ consists of one occurrence of A and $\varDelta$ is empty. What needs to be shown is that $A, \varTheta \Rightarrow \varLambda$, which is already given by $\mathcal {D}_2$.

For the induction step, we distinguish two cases, and again we continue Indrzejczak’s proof by adding the new cases arising through the addition of I.

(A) No $A^k$ in the succedent of the conclusion of $\mathcal {D}_1$ is principal. Then we apply the induction hypothesis to the premises of the final rule applied in $\mathcal {D}_1$ and apply the final rule once more.

(B) Some $A^k$ in the succedent of the conclusion of $\mathcal {D}_1$ is principal. Two options:

(I) The final rule applied in $\mathcal {D}_1$ is (RI):

By induction hypothesis, we have

• (1) $\varGamma , \varTheta ^{k-1} \Rightarrow \varDelta , \varLambda ^{k-1}, F_t^x$

• (2) $\varGamma , \varTheta ^{k-1}\Rightarrow \varDelta , \varLambda ^{k-1}, G_t^x$

• (3) $F_a^x, \varGamma , \varTheta ^{k-1}\Rightarrow \varDelta , \varLambda ^{k-1}, a=t$

Apply (RI) with (1) to (3) as premises to conclude

• (4) $\varGamma , \varTheta ^{k-1} \Rightarrow \varDelta , \varLambda ^{k-1}, Ix[F, G]$

Here Ix[F, G] is principal, so apply the Right Reduction Lemma to the deduction concluding (4) and $\mathcal {D}_2$ (where $k=1$) to conclude $\varGamma , \varTheta ^k \Rightarrow \varDelta , \varLambda ^k$.

(II) The final rule applied in $\mathcal {D}_1$ is $(LI^2)$:

By induction hypothesis, we have

• (1) $\varGamma , \varTheta ^{k-1}\Rightarrow \varDelta , \varLambda ^{k-1}, F_{t_1}^x$

• (2) $\varGamma , \varTheta ^{k-1}\Rightarrow \varDelta , \varLambda ^{k-1}, F_{t_2}^x$

• (3) $\varGamma , \varTheta ^{k-1}\Rightarrow \varDelta , \varLambda ^{k-1}, C_{t_2}^x$

Apply $(LI^2)$ with (1) to (3) as premises to conclude:

• (4) $Ix[F, G], \varGamma , \varTheta ^{k-1}\Rightarrow \varDelta , \varLambda ^{k-1}, C_{t_1}^x$

Here $C_{t_1}^x$ is principal, so apply the Right Reduction Lemma to the deduction concluding (4) and $\mathcal {D}_2$ (where $k=1$) to conclude $Ix[F, G], \varGamma , \varTheta ^k \Rightarrow \varDelta , \varLambda ^k$.

This completes the proof of the Left Reduction Lemma.

Theorem 1

(Cut Elimination). For every deduction in $\mathbf {CPF}^I$, there is a deduction that is free of cuts.

Proof. The theorem follows from the Right and Left Reduction Lemmas by induction over the degree of the proof, with subsidiary inductions over the number of cut formulas of highest degree, as in Indrzejczak’s paper.

5 Semantics for $\mathbf {CPF}^I$

For the purposes of providing a semantics for $\mathbf {CPF}^I$ it is convenient to modify the system slightly in the following way: free variables $x, y, z \ldots$ are allowed to occur in formulas, parameters are treated like constants, and constants may play the role of parameters if they occur parametrically in a deduction, that is, they fulfil the restrictions imposed in $(R\forall )$, (RI) and $(LI^1)$. The restrictions for free variables in these rules are as for the parameters. Furthermore, for the purposes of this section, I take $\Rightarrow$ to have sets of sentences rather the multisets to its left and right. I’ll write $\varGamma , A$ to abbreviate $\varGamma \cup \{A\}$, $A, B, C\in \varDelta$ for $\{A, B, C\}\subseteq \varDelta$. The resulting modified system is evidently equivalent to the original formulation.

It is fairly obvious that the rules governing I enforce the uniqueness of A, if it is the case that Ix[A, B], but not its existence. Arguing informally, it is immediate from $(LI^2)$ that $Ix[A, B], A_a^x, A_b^x\Rightarrow a=b$, hence any As are identical; and if $A_a^x$ is false, whatever a might be, then $A_a^x\Rightarrow \bot$, so by $(LI^1)$, $Ix[A, B]\Rightarrow \bot$. But the rules do not permit us to determine whether the unique A exists or not. Conversely, to derive Ix[A, B], we need a unique A that is B, but it is not required that it exists. Nonetheless, we will prove it rigorously by providing a sound and complete semantics for $\mathbf {CPF}^I$. I follow the popular proposal by [3, 28] and [29], where two domains are considered, an inner one and an outer one, the former the domain of existing objects, over which the universal quantifier ranges and of which $\exists !$ is true, and the latter the domain of ‘non-existent’ objects. I shall take the inner domain to be a subset of the outer domain.

The exposition of the formal semantics for $\mathbf {CPF}^I$ and the soundness and completeness proofs in the next section follow Enderton closely, with necessary adjustments to be suitable to free logic. Most of the following is well known and not new, but I’ll be explicit about the details in order to demonstrate the semantics of I explicitly and precisely.

A structure $\mathfrak {A}$ is a function from the expressions of the language $\mathcal {L}$ of $\mathbf {CPF}^I$ to elements, a (possibly empty) subset, the sets of n-tuples of and operations on a non-empty set $|\mathfrak {A}|$, called the domain of $\mathfrak {A}$, such that:

• 1. $\mathfrak {A}$ assigns to the quantifier $\forall$ a (possibly empty) set $|\mathfrak {A}^\forall |\subseteq |\mathfrak {A}|$ called the inner domain or the domain of quantification of $\mathfrak {A}$.

• 2. $\mathfrak {A}$ assigns to the predicate $\exists !$ the set $|\mathfrak {A}^\forall |$.

• 3. $\mathfrak {A}$ assigns to each n-place predicate symbol P an n-ary relation $P^\mathfrak {A}\subseteq |\mathfrak {A}|^n$.

• 4. $\mathfrak {A}$ assigns to each constant symbol c an element $c^\mathfrak {A}$ of $|\mathfrak {A}|$.

• 5. $\mathfrak {A}$ assigns to each n-place function symbol f an n-ary operation $f^\mathfrak {A}$ on $|\mathfrak {A}|$, i.e. $f^\mathfrak {A}:|\mathfrak {A}|^n\rightarrow |\mathfrak {A}|$.

Next we define the notion of satisfaction of a formula B by a structure $\mathfrak {A}$. To handle free variables we employ a function $s:V\rightarrow |\mathfrak {A}|$ from the set of variables V of $\mathcal {L}$ to the domain of the structure. Suppose x occurs free in B. Informally, we say that $\mathfrak {A}$ satisfies B with s, if and only if the object of the domain of $\mathfrak {A}$ that s assigns to the variable x satisfies B, that is, if s(x) is in the set $\mathfrak {A}$ assigns to B. We express this in symbols by $\vDash _\mathfrak {A}A\ [s]$. $\nvDash _\mathfrak {A}A\ [s]$ means that $\mathfrak {A}$ does not satisfy A with s. The formal definition of satisfaction is as follows.

First, s is extended by recursion it to a function $\overline{s}$ that assigns objects of $|\mathfrak {A}|$ to all terms of the language:

• 1. For each variable x, $\overline{s}(x)=s(x)$

• 2. For each constant symbol c, $\overline{s}(c)=c^\mathfrak {A}$.

• 3. For terms $t_1\ldots t_n$, n-place function symbols f, $\overline{s}(ft_1\ldots t_n)=f^\mathfrak {A}(\overline{s}(t_1)\ldots \overline{s}(t_n))$

Satisfaction is defined explicitly for the atomic formulas of $\mathcal {L}$:

• 1. $\vDash _\mathfrak {A} t_1 = t_2 \ [s]$ iff $\overline{s}(t_1)=\overline{s}(t_2)$.

• 2. $\vDash _\mathfrak {A} \exists ! t \ [s]$ iff $\overline{s}(t)\in |\mathfrak {A}^\forall |$.

• 3. For n-place predicate parameters P, $\vDash _\mathfrak {A} Pt_1\ldots t_n \ [s]$ iff $\langle \overline{s}(t_1)\ldots \overline{s}(t_n)\rangle \in P^\mathfrak {A}$.

For the rest of the formulas, satisfaction is defined by recursion. Let s(x|d) be like s, only that it assigns the element d of $|\mathfrak {A}|$ to the variable x:

• 1. For atomic formulas, as above.

• 2. $\vDash _\mathfrak {A} \lnot A \ [s]$ iff $\nvDash _\mathfrak {A} A \ [s]$.

• 3. $\vDash _\mathfrak {A} A \rightarrow B \ [s]$ iff either $\nvDash _\mathfrak {A} A \ [s]$ or $\vDash _\mathfrak {A} B\ [s]$.

• 4. $\vDash _\mathfrak {A} \forall x A \ [s]$ iff for every $d\in |\mathfrak {A}^\forall |$, $\vDash _\mathfrak {A} A \ [s(x|d)]$.

This gives a semantics for $\mathbf {CPF}$. For $\mathbf {CPF}^I$, we add a clause for I:

• 5. $\vDash _\mathfrak {A} Ix [A, B] \ [s]$ iff there is $d\in |\mathfrak {A}|$ such that: $\vDash _\mathfrak {A} A \ [s(x|d)]$, there is no other $e\in |\mathfrak {A}|$ such that $\vDash _\mathfrak {A} A \ [s(x|e)]$, and $\vDash _\mathfrak {A} B \ [s(x|d)]$.

In other words, $\vDash _\mathfrak {A} Ix [F, G] \ [s]$ iff there is exactly one element in the domain of $\mathfrak {A}$ such that $\mathfrak {A}$ satisfies A with s modified to assign that element to x, and $\mathfrak {A}$ satisfies B with the same modified s.

We could define notions of validity, truth and falsity applicable to formulas, if we like, but won’t need them in the following. A formula A is valid iff for every $\mathfrak {A}$ and every $s:V\rightarrow |\mathfrak {A}|$, $\vDash _\mathfrak {A} A \ [s]$. Call a formula with no free variables a sentence. A structure $\mathfrak {A}$ either satisfies a sentence $\sigma$ with every function $s:V\rightarrow |\mathfrak {A}|$ or with none. If the former, $\sigma$ is true in $\mathfrak {A}$, if the latter, $\sigma$ is false in $\mathfrak {A}$. If the former, we may write $\vDash _\mathfrak {A} \sigma$ and say that $\mathfrak {A}$ is a model of $\sigma$.

More important are notions applicable to the sequents of the deductive system of $\mathbf {CPF}^I$. A sequent $\varGamma \Rightarrow \varDelta$ is satisfied by a structure $\mathfrak {A}$ with a function $s:V\rightarrow |\mathfrak {A}|$ if and only if, if for all $A\in \varGamma$, $\vDash _\mathfrak {A} A \ [s]$, then for some $C\in \varDelta$, $\vDash _\mathfrak {A} C \ [s]$. We symbolise this by $\vDash _\mathfrak {A} \varGamma \Rightarrow \varDelta \ [s]$. A sequent $\varGamma \Rightarrow \varDelta$ is valid iff it is satisfied by every structure with every function $s:V\rightarrow |\mathfrak {A}|$. In this case we write $\vDash \varGamma \Rightarrow \varDelta$.

Sequents have finite sets to the left and right of $\Rightarrow$. We also need notions that apply to finite and infinite set.

A set of formulas $\varGamma$ is satisfiable iff there is some structure $\mathfrak {A}$ and some function $s:V\rightarrow |\mathfrak {A}|$ such that $\mathfrak {A}$ satisfies every member of $\varGamma$ with s.

A set of formulas $\varGamma$ deductively implies a formula A, iff for some finite $\varGamma _0\subseteq \varGamma$, $\vdash \varGamma \Rightarrow A$. If $\varGamma$ deductively implies A, we record this fact by $\varGamma \vdash A$.

A set of formulas $\varGamma$ semantically implies a formula A, iff for every structure $\mathfrak {A}$ and every function $s:V\rightarrow |\mathfrak {A}|$ such that $\mathfrak {A}$ satisfies every member of $\varGamma$ with s, $\mathfrak {A}$ satisfies A with s. If $\varGamma$ semantically implies A, we record this fact by $\varGamma \vDash A$.

6 Soundness and Completeness

I’ll prove two pairs of soundness and completeness theorems: one pair shows that deducibility and validity of sequents coincide, and another that deductive and semantic implication coincide.

A formula $A'$ is an alphabetic variant of a formula A if A and $A'$ differ only in the choice of bound variables.

Lemma 4

(Existence of Alphabetic Variants). For any formula A, term t and variable x, there is a formula $A'$ such that $A\Rightarrow A'$ and $A'\Rightarrow A$ and t is substitutable for x in $A'$.

Proof. Mutatis mutandis Enderton’s proof goes through for $\mathbf {CPF}^I$, too [6, p. 126f].

Alphabetic variants are semantically equivalent: if A and $A'$ are alphabetic variants, then $A\vDash A'$ and $A'\vDash A$.

Lemma 5

(The Substitution Lemma). $\vDash _\mathfrak {A} A^x_t \ [s] \text { iff } \vDash _\mathfrak {A} A \ [s(x|\overline{s}(t))]$, if t is free for x in A.

Proof. See [6, p. 133f] and adjust.

Theorem 2

(Soundness for Sequents). If $\vdash \varGamma \Rightarrow \varDelta$, then $\vDash \varGamma \Rightarrow \varDelta$.

Proof. Standard, by induction over the complexity of deductions and observing that the axioms are valid and all rules preserve validity. In the appendix of [24], the soundness of the rules for the $\forall$ and I is proved.

Theorem 3

(Soundness for Sets). If $\varGamma \vdash A$, then $\varGamma \vDash A$.

Proof. If $\varGamma \vdash A$, then for some finite $\varGamma _0\subseteq \varGamma$, $\vdash \varGamma _0\Rightarrow A$. So by Theorem 2, $\vDash \varGamma _0\Rightarrow A$. Suppose some structure $\mathfrak {A}$ satisfies all formulas of $\varGamma$ with a function $s:V\rightarrow |\mathfrak {A}|$. Then $\mathfrak {A}$ satisfies $\varGamma _o$ with s, hence, as $\vDash \varGamma _0\Rightarrow A$, $\mathfrak {A}$ satisfies A with s, and so $\varGamma \vDash A$.

Some more definitions. Let $\bot$ represent an arbitrary contradiction. A set of formulas $\varGamma$ is inconsistent iff $\varGamma \vdash \bot$. $\varGamma$ is consistent iff it is not inconsistent. A set of formulas $\varGamma$ is maximal iff for any formula A, either $A\in \varGamma$ or $\lnot A\in \varGamma$. A set of formulas $\varGamma$ is deductively closed iff, if $\varGamma \vdash A$, then $A\in \varGamma$.

Lemma 6

Any maximally consistent set is deductively closed.

Proof. Suppose $\varGamma$ is maximal and $\varGamma \vdash A$ but $A\not \in \varGamma$. Then for some finite $\varGamma _0\subseteq \varGamma$, $\vdash \varGamma _0\Rightarrow A$. By maximality of $\varGamma$, $\lnot A\in \varGamma$, hence for some finite $\varGamma _1\subseteq \varGamma$, $\vdash \varGamma _1\Rightarrow \lnot A$. Hence $\vdash \varGamma _0, \varGamma _1\Rightarrow A\wedge \lnot A$, and so $\varGamma \vdash \bot$. Contradiction.

Theorem 4

Any consistent set of formulas $\varDelta$ can be extended to a maximally consistent set $\varDelta ^+$ such that:

(a) for any formula A and variable x, if $\lnot \forall xA\in \varDelta ^+$, then for some constant c, $\exists !c\in \varDelta ^+$ and $A_c^x\not \in \varDelta ^+$;

(b) for any formulas A and B and variable x, if $Ix[A, B]\in \varDelta ^+$, then for some constant c, $A_c^x, B_c^x\in \varDelta ^+$ and for all constants d, if $A_d^x\in \varDelta ^+$, then $d=c\in \varDelta ^+$.

(c) for any formulas A and B and variable x, if $\lnot Ix[A, B]\in \varDelta ^+$, then for all constants c, either $A_c^x\not \in \varDelta ^+$, or for some constant d, $A_d^x\in \varDelta ^+$ and $d=c\not \in \varDelta ^+$, or $B_c^x\not \in \varDelta ^+$.

Proof is in the appendix of the online version [24].

Theorem 5

If $\varDelta$ is a consistent set of formulas, then $\varDelta$ is satisfiable.

Proof is in the appendix of the online version [24].

Theorem 6

(Completeness for Sequents). If $\vDash \varGamma \Rightarrow \varDelta$, then $\vdash \varGamma \Rightarrow \varDelta$.

Proof. Let $\lnot \varDelta$ be the negation of all formulas in $\varDelta$. If $\vDash \varGamma \Rightarrow \varDelta$, then $\varGamma , \lnot \varDelta$ is not satisfiable. Hence by Theorem 5 it is inconsistent, and as they are both finite, $\vdash \varGamma , \lnot \varDelta \Rightarrow \bot$. Hence by the properties of negation $\vdash \varGamma \Rightarrow \varDelta$.

Theorem 7

(Completeness for Sets). If $\varGamma \vDash A$, then $\varGamma \vdash A$.

Proof. Suppose $\varGamma \vDash A$. Then $\varGamma , \lnot A$ is not satisfiable, hence by Theorem 5 it is inconsistent and $\varGamma , \lnot A\vdash \bot$. So for some finite $\varSigma \subseteq \varGamma , \lnot A$, $\varSigma \Rightarrow \bot$. If $\lnot A\in \varSigma$, then by the deductive properties of negation, $\varSigma -\{\lnot A\}\Rightarrow A$, and as $\varSigma -\{\lnot A \}$ is certain to be a subset of $\varGamma$, $\varGamma \vdash A$. If $\lnot A\not \in \varSigma$, then $\varSigma \Rightarrow A$ by the properties of negation, and again $\varGamma \vdash A$.

7 Tableaux Rules

In this section, we’ll extend Priest’s tableaux system for classical positive free logic [32, Ch 13] by rules for I. His rules give a system equivalent to $\mathbf {CPF}$:

where t is any term on the branch (or a new one if there is none yet), a is new to the branch and $t_3$ is any term.

The binary quantifier I has the following rules:

where a is new to the branch and t is any term on the branch (or a new one if there is none yet).

8 Conclusion

The theory of definite descriptions formulated here has some novel and attractive features. The proof-theory is simple and has desirable consequences. It differs from Hintikka’s and Lambert’s preferred theories in a well-motivated way. It lends itself to applications of formalisations in which scope distinctions are of importance. The distinction between internal and external negation has been mentioned in the introduction. Other, and particularly interesting, cases are found in modal discourse. There is a significant difference between ‘It is possible the that present King of France is bald’ and ‘The present King of France is possibly bald’. In the present framework, the former is formalised by a formula such as $\Diamond Ix[Kx, Bx]$, the latter by $Ix[Kx, \Diamond Bx]$. The importance of scope distinctions in the context of modal logic was first pointed out by Smullyan [33]. His account was further developed by Hughes and Cresswell [13, p. 323ff]. Elaborate systems catering for definite descriptions in modal logic have been provided by Fitting and Mendelsohn [7] and Garson [10]. In both of the latter systems, an operator for predicate abstraction is used to mark scope, but it serves no further purpose. Future research will investigate the addition of the binary quantifier I to quantified modal logic and compare the result to existing systems. In particular, as the present system incorporates scope distinctions directly into the formalism for representing definite descriptions, there is no need for additional means to mark scope. This promises economy and clarity in the formalism for representing definite descriptions where scope distinctions matter.