2 Positive free logic without and with $\iota $

The language is standard, and as in [Reference Kürbis20, sec. 2.1], and so is the definition of deduction and $\vdash _S$ , which essentially follows Troelstra and Schwichtenberg [Reference Troestra and Schwichtenberg38, sec. 2.1.1]. Recall that $A_t^x$ is the formula that results when x is replaced in A by t and that $\exists !$ is the existence predicate. The systems modify rules given by Tennant for negative free logic to suit positive free logic (see [Reference Tennant36, sec. 7.10] and [Reference Tennant37]). The system IPF of intuitionist positive free logic has the following rules:

where in $(\forall I)$ and $(\exists E)\ a$ does not occur in $\forall xA$ , $\exists xA$ , C, nor in any undischarged assumptions of $\Pi $ except for those in the assumption classes of $A_a^x$ or of $\exists ! a$ .

Classical positive free logic $\mathbf {CPF}$ has the rules for $\rightarrow $ , $\forall $ and $=$ of $\mathbf {IPF}$ and $(\bot E)$ is replaced by

Vacuous discharged being permitted, $(\bot E)$ is a special case of $(\bot E_C)$ , and such applications of the latter are treated as if they were applications of the former.

Comparing $\mathbf {IPF}$ and $\mathbf {CPF}$ to $\mathbf {INF}$ and $\mathbf {CNF}$ of [Reference Kürbis20], note the absence of the rule $(AD)$ of atomic denotationFootnote ⁴ and of the premise $\exists !t$ in $(=I)$ .Footnote ⁵ This means sequences of application of these rules that gave rise to segments that count as maximal in negative free logic cannot arise (maximal $=$ -, $\exists !$ - and the first two cases of maximal $(=E)$ -segments [Reference Kürbis20, sec. 3.3]). The absence of $(AD)$ also means that sequences of applications of $(=E)$ with minor premises formed from $\exists !$ and a term cannot be removed from deductions and hence are not detours and do not count as maximal. This has some philosophical interest, on which I comment at the end of this section.

The $\iota $ operator is governed by the following rulesFootnote ⁶ :

where a is neither free in F nor in t and does not occur in any undischarged assumptions in $\Xi $ and $\Pi $ except those in the assumption classes displayed;

Compared to the rules for $\iota $ of [Reference Kürbis20], note first the existence formulas that may be above the middle premise of $(\iota I)$ and that are added as premises in $(\iota E_1)$ nd $(\iota E_2)$ . This is all due to the absence of $(AD)$ : in negative free logic, these formulas may be derived from identities that occur in the rules. Secondly, $\iota $ does not have the third elimination rule that in negative free logic is a special case of $(AD)$ . This, too, has some philosophical interest, on which I’ll comment at the end of this section.

$\mathbf {IPF}^{\iota }$ is $\mathbf {IPF}$ with $\iota $ and its rules added. Similarly for $\mathbf {CPF}^{\iota }$ .

Lambert formalises his minimal theory of definite descriptions by adding the following axiom to CPF (see [Reference Lambert26, 30] and [Reference Lambert27, 90f]):

1. (LA) ${\forall z (\iota xA=z\leftrightarrow \forall y(A_y^x\leftrightarrow y=z))}$

Call the systems that arise from $\mathbf {IPF}$ and $\mathbf {CPF}$ by adding ( $LA$ ) $\mathbf {IPF}^{LA}$ and $\mathbf {CPF}^{LA}$ .

( $LA$ ) is equivalent to the rules for $\iota $ above, showing that they are indeed the intended ones for positive free logic.

Proof. It is useful to appeal to rules for the biconditional:

(a) We have:

So by $(\iota I)$ : $(\ast )$ $\exists !b, \forall y(A_y^x\leftrightarrow y=b)\vdash \iota xA=b$ . Furthermore:

So by $(\leftrightarrow I)$ from $(\ast )$ : $\exists !b\vdash \iota xA=b\leftrightarrow \forall y(A_y^x\leftrightarrow y=b)$ . $(LA)$ follows by $(\forall I)$ .

(b) Given deductions $\Xi $ of $A_a^x$ from $a=t$ and $\exists !a$ and $\Sigma $ of $a=t$ from $A_a^x$ and $\exists !a$ satisfying the condition of $(\iota I)$ , derive $\forall y(A_y^x\leftrightarrow y=t)$ by $(\leftrightarrow I)$ and $(\forall I)$ , discharging the assumptions listed. Apply $(\forall E)$ with $\exists !t$ to derive $\iota xA=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=t)$ from $(LA)$ , apply $(\leftrightarrow E_1)$ to derive $\iota xA=t$ . The derivability of $(\iota E_1)$ and $(\iota E_2)$ is equally straightforward.

$\mathbf {CPF}^{\iota }$ is equivalent to Lambert’s minimal free theory of definite descriptions $\mathbf {MFD}$ . It contains, so to speak, only what is generally agreed upon: if a unique A exists, $\iota xA$ refers to it.Footnote ⁷ If this is not the case, $\mathbf {MFD}$ says nothing specifically to do with definite descriptions about $\iota xA$ , although it does, of course, say things about $\iota xA$ that follow from the laws of positive free logic without $\iota $ . According to Lambert, $\mathbf {MFD}$ is too minimal as ‘an important principle evidently not deducible from [( $LA$ )] is the principle of Cancellation’ [Reference Lambert26, 30]:

1. (CA) $\iota x (x=t)=t$ .

Lambert’s system $\mathbf {FD1}$ results from adding (CA) to $\mathbf {MFD}$ (see [Reference Lambert, Morscher and Hieke25, 44] and [Reference Lambert27, 90f]).

The strongest of Lambert’s systems, $\mathbf {FD2}$ , is formalised by adding the following axiom to $\mathbf {CPF}$ (see [Reference Lambert23, 87] and [Reference van Fraassen and Lambert6, 237])Footnote ⁸ :

1. (FD2) $\iota xA=t\leftrightarrow \forall x (x=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=x)).$

(FD2) implies both ( $LA$ ) and (CA), but is not implied by them. A consequence of (FD2) is

1. (CO) $(\neg \exists ! t_1\land \neg \exists !t_2)\rightarrow t_1=t_2$ .

Semantically speaking, $\mathbf {FD2}$ has the consequence that, if improper definite descriptions are declared to refer to something, then they all to refer to the same thing.Footnote ⁹ Similarly for constants. This is Carnap’s chosen object theory of ‘non-denoting’ terms, a version of which was also endorsed by Frege in some of his writings (see [Reference Frege7, 41] and [Reference Carnap3, secs. 7 and 8]).Footnote ¹⁰

After establishing normalisation results for $\mathbf {IPF}$ , $\mathbf {CPF}$ , $\mathbf {IPF}^{\iota }$ and $\mathbf {CPF}^{\iota }$ , I’ll consider $\mathbf {FD1}$ and $\mathbf {FD2}$ and their intuitionist versions. I will then also consider three alternatives. They raise philosophical questions, on which I shall comment briefly in the next and later sections.

3 Philosophical comments

The differences in the rules of positive and negative free logic merit philosophical reflection, but I’ll only hint at some thoughts here.

1. Sequences of applications of $(=E)$ the minor premises of which are existence formulas (maximal $(=E)$ -segments of [Reference Kürbis20]) cannot be removed from deductions in positive free logic. Whereas, due to the normalisation theorem, in negative free logic, only the last two terms in such a sequence must denote for the conclusion of the deduction to be derivable from (some of) its open assumptions, in positive free logic, this is the case for all terms in the sequence. This is a little surprising. From the semantic perspective usually taken by free logicians, positive free logic permits truth without reference even in the case of atomic formulas, in particular identities. Negative free logic does not. In general, negative free logic requires more existence assumptions for truth than positive free logic. Here we have a situation where it is the other way round. When the terms are $\iota $ terms, they may even involve predicates that do not occur in the conclusion nor in undischarged assumptions above the last major premise of $(=E)$ in the sequence: thus in positive free logic, the proof requires more conceptual resources that the corresponding proof in negative free logic.

2. The lacking third elimination rule of $\iota $ introduces a certain misbalance that is problematic from the perspective of proof-theoretic semantics and the requirement of harmony. Harmony consists in a balance between introduction and elimination rules for a logical expression. Roughly, the grounds for deriving a formula with a logical expression required by its introduction rules can be retrieved from the formula by its elimination rules. In the rules for $\iota $ above, one such ground, the premise $\exists !t$ of $(\iota I)$ , cannot be retrieved from $\iota xF=t$ by an elimination rule. According to proof-theoretic semantics, harmony is necessary for rules governing an expression to define its meaning. It may be that the misbalance can be justified independently, for instance from the nature of reference, or it may be concluded that $\iota $ is not an expression the meaning of which is defined by its rules of inference. I’m not going to investigate whether such an independent justification can be given. Instead, assuming that the meaning of $\iota $ may be defined by the rules governing it, I shall consider two options of remedying the misbalance now and there’ll be further reflections on this topic later in this paper.Footnote ¹¹

One option would be to add the third elimination rule for $\iota $ of negative free logic to positive free logic, i.e., $\iota xF=t\vdash \exists !t$ . However, not only would this be against the spirit of positive free logic, it would also be inconsistent. The motivation for positive free logic is that, for which reasons ever, formulas containing constants may be true or assertible even if some terms occurring in them do not refer. This is supposed to extend to singular terms in general. With the additional rule, for any definite description $\iota xF,$ it follows that $\exists !\iota xF$ , as from $(=I)\ \iota xF=\iota xF$ . And so, replacing t and u by $\iota xF$ in $(\iota E_1)$ , $F(\iota xF)$ , for any F. Now replace F by an inconsistent predicate, say $Ax\land \neg Ax$ . Then $A(\iota x(Ax\land \neg Ax))\land \neg A(\iota x(Ax\land \neg Ax))$ . Contradiction.

The second option results in an alternative theory of definite descriptions: do not require the premise $\exists !t$ in $(\iota I)$ and instead adopt the rule:

where a is neither free in F nor in t and does not occur in any undischarged assumptions in $\Xi $ and $\Pi $ except those in the assumption classes displayed.

The resulting theory is no longer equivalent to Lambert’s. ( $LA$ ) is derivable from $(\iota I')$ , $(\iota E_1)$ and $(\iota E_2)$ , but $(\iota I')$ is not derivable from ( $LA$ ). The new set of rules is equivalent to two axioms:

1. (HA ^rl ) For any term t: $\forall y(A_y^x\leftrightarrow t=y)\rightarrow \iota xA=t$ .

2. (LA ^lr ) $\forall z (\iota xA=z\rightarrow \forall y(A_y^x\leftrightarrow z=y)).$

The label ( $HA^{rl}$ ) was chosen because this axiom is the right to left direction of an axiom I’m naming after Hintikka in a later section.

( $HA^{rl}$ ) says that if t is the unique existing A, then it is the A. An easy consequence is $\forall x(A\leftrightarrow x=t)\vdash \exists xA\leftrightarrow \exists !t$ , hence $\forall x(A\leftrightarrow x=t), \exists !t\vdash A_t^x$ . Furthermore, letting A be $x=t$ , $\vdash \iota x (x=t)=t$ , which is the second axiom of Lambert’s preferred free theory of definite descriptions, on which more below.

Call the theory of definite descriptions axiomatised by ( $HA^{rl}$ ) and ( $LA^{lr}$ ) $\mathbf {FDA}$ . In §8 of this paper it is observed that a normalisation theorem for the system resulting by replacing $(\iota I)$ by $(\iota I')$ can be proved.

3. Questions regarding proof-theoretic semantics and harmony also motivate the discussion of systems of natural deduction equivalent to Lambert’s $\mathbf {FD1}$ and $\mathbf {FD2}$ and two further alternative theories of definite descriptions later in this paper. One will be based on the axiom of Hintikka’s already mentioned, the other on an axiom that contained a typo in a paper of Lambert’s. While harmony is problematic in the former two systems, the rules of the latter two do appear to be in harmony. This raises a number of philosophical questions.

4 Simplifying lemmas and preliminaries

I’ll repeat definitions, lemmas, theorems and corollaries, the latter without proof, from [Reference Kürbis20] for convenience, distinguishing them by an N from those of the present paper.

Definitions 1 and 2 (of $\vdash _S$ ) of [Reference Kürbis20] stay the same. Hintikka’s Law $\exists !t\leftrightarrow \exists x \ x=t$ is derivable in positive free logic. As their proofs do not appeal to $(AD)$ or $(=I^n)$ , Lemmas 1 and 2 of [Reference Kürbis20] carry over to $\mathbf {IPF}$ , $\mathbf {IPF}^{\iota }$ and $\mathbf {CPF}$ , and as before, in $\mathbf {CPF}^{\iota }$ , $(\bot E_C)$ can be restricted only to atomic, but not prime, conclusions.

Applications of $(=E)$ , $(\bot E)$ and $(\bot E_C)$ are from now of assumed to be restricted as stated.

Definitions 3–6 carry over unchanged, and those of Definition 5 are all the maximal segments that need to be considered. Definitions 12 and 13 stay the same, too.

(i) $\bot $ , then $d(A)=1$ ;

(ii) $\neg B$ , then $d(A)=d(B)+1$ ;

(iii) $B\land C$ , $B\supset C$ or $B\lor C$ , then $d(A)=d(B)+d(C)+1$ ;

(iv) $\forall xB$ or $\exists xB$ , then $d(A)=d(B)+2.$

Maximal I/E-segments are those arising from introduction and elimination rules, which are all the maximal segments in positive free logic.

Definitions 7–16, Lemma 3 and Corollaries 1–6 to Theorem 1, the normalisation theorem for $\mathbf {INF}$ , of [Reference Kürbis20] were concerned with maximal segments specific to negative free logic, the form of normal deduction and the subformula property. For brevity I won’t consider the subformula property in the present paper, but, due to the standard theory of identity and the absence of $(AD)$ , it is rather simpler in positive than in negative free logic. As before it would be possible to reformulate the systems in Jaśkowski-style to improve on the subformula property [Reference Kürbis20, sec. 5]. Doing so for $\mathbf {CPF}$ would result in a system equivalent to Jaśkowski [Reference Gentzen9]. I won’t consider this option here.

5 Normalisation for positive free logic without definite descriptions

Normalisation for deductions in $\mathbf {IPF}$ follows straightforwardly from normalisation for those in $\mathbf {INF}$ [Reference Kürbis20, sec. 4.1]. The reduction procedures for the propositional connectives and the quantifiers are the same, the former as given by Prawitz, the latter repeated here for convenience. Replace the inferences on the left by those on the right:

Applications of $(=E)$ with major premise of form $t=t$ remain vacuous and are simply deleted from deductions.

Corresponding to Theorem 5 of [Reference Kürbis20, sec. 7] is the following, which is also proved by a standard, but slightly simpler, induction over the rank of deductions.

6 Normalisation for positive free logic with definite descriptions

With definite descriptions, arbitrarily complex terms may be used as the instantiating terms in $(\exists I)$ and $(\forall E)$ . This is a problem for normalisation, as in the reduction procedures for the quantifiers parameters are replaced by the instantiating terms, which increases the complexity of formulas if the term is complex. As in the case of negative free logic, the problem is solved by adding Indrzejczak’s rule $(=I^n)$ to positive free logic [Reference Indrzejczak14, sec. 4]:

where the parameter a occurs neither in t, nor in C, nor in any open assumptions of $\Pi $ other than those of the assumption class of $a=t$ .

As Hintikka’s Law is valid, the rule is derivable. $(=I)$ is not derivable from $(=I^{nG})$ ,Footnote ¹² so the systems $\mathbf {IPF}{'}^{\iota }$ and $\mathbf {CPF}{'}^{\iota }$ are $\mathbf {IPF}^{\iota }$ + $(=I^{nG})$ and $\mathbf {CPF}^{\iota }$ + $(=I^{nG})$ , respectively.

The proof of Lemma 7 of [Reference Kürbis20] appeals to $(AD)$ , so requires a slightly different proof.

Proof. Replace an application of $(\forall E)$ in which t is complex by the following:

Similarly for $(\exists I)$ .

Note that the deduction contains what in negative free logic counts as a maximal segment, i.e., the upper application of $(=E)$ : there is no way around this in positive free logic, because we cannot deduce the minor premise $\exists !a$ of $(\forall E)$ from $a=t$ alone, and no other assumptions are given from which it could be derived.

Comment. As in the case of negative free logic, we may ask a philosophical question regarding the addition of $(=I^{nG})$ . As noted in the previous paper in response to a referee’s comment, this rule hides a maximal formula. In positive free logic, this may look even worse, as it is an additional rule, not one that permits economies by replacing another rule. Further discussion must be left for another occasion.

As the rules for $\iota $ are slightly different from those for negative free logic, the reduction procedures are also slightly different. They are as follows:

(1) $(\iota I)$ followed by $(\iota E_1)$ :

(2) $(\iota I)$ followed by $(\iota E_2)$ :

Comment. In the second reduction procedure the minor premise $\exists !t$ of $(\iota E_2)$ is not used. We could reformulate $(\iota I)$ so as to permit the discharge of $\exists !t$ above the rightmost subdeduction, and then the minor premise would be used in the reduction procedure. However, as $\exists !t$ follows from $a=t$ and $\exists !a$ , there is no need to do so, and the rule as stated is slightly more economical.Footnote ¹³

As in negative free logic, we face the problem that u may be complex, and so replacing it for the parameter a may increase the complexity of formulas. Once more an observation of Indrzejczak’s solves the problem [Reference Indrzejczak15]: the rules for $\iota $ may be restricted to one occurrence of an $\iota $ term, where it is displayed in the rules. Lemma 8 of [Reference Kürbis20] appeals to $(AD)$ , so the corresponding result for positive free logic requires a slightly different proof.

Proof. Double lines mark inferences by symmetry of identity, which is derivable from $(=I)$ and $(=E)$ .

(1) Replace an application of $(\iota I)$ where t is a complex term $\iota yG$ by

where a and b are fresh parameters.

(2) Replace an application of $(\iota E_1)$ where t is a term $\iota yG$ and u atomic by

where a is a fresh parameter.

If u is a complex term $\iota zH$ , replace u by a fresh parameter b; deduce $b=\iota yG$ from $\iota zH=\iota yG$ and $b=\iota zH$ , $\exists !b$ from $b=\iota zH$ and $\exists !\iota zH$ , and $F_{\iota zH}^x$ from $b=\iota zH$ and $F_b^x$ , all by $(=E)$ ; discharge $b=\iota zH$ by $(=I^{nG})$ with premise $\exists !\iota zH.$

(3) Replace an application of $(\iota E_2)$ where t is a term $\iota yG$ and u atomic by

where a is a fresh parameter.

If u is a complex term $\iota zH$ , replace u by a fresh parameter b; deduce $F_b^x$ from $b=\iota zH$ and $F_{\iota zH}^x$ , $\exists !b$ from $b=\iota zH$ and $\exists !\iota zH$ , and $\iota zH=\iota yG$ from $b=\iota zG$ and $b=\iota zH$ , all by $(=E)$ ; discharge $b=\iota zH$ by $(=I^{nG})$ with premise $\exists !\iota zH$ .

Applications of the $\iota $ rules in $\mathbf {IPF}{'}^{\iota }$ and $\mathbf {CPF}{'}^{\iota }$ are therefore restricted accordingly to only one occurrence of an $\iota $ term where it is displayed in the rules. The following is immediate from the foregoing.

Definition 4N is modified as in Definition 18 of [Reference Kürbis20]: insert ‘or $(=I^{nG})$ ’ after $(\exists E)$ . Definition 5N stays the same.

Concerning $\mathbf {CPF}$ , Definitions 20 and 22 of [Reference Kürbis20] stay the same, Definition 21 contains a redundancy ‘or the premise of $(AD)$ ’, and Lemma 10 goes through as before.

The slightly different rules for $\iota $ require slightly a different adaptation of Andou’s method to prove normalisation [Reference Andou1]. The reduction procedures are as follows:

(1) $(\bot E_C)$ followed by $(\iota E_1)$ :

(2) $(\bot E_C)$ followed by $(\iota E_2)$ :

7 Lambert’s stronger systems

7.1 FD1

Call the systems that result from $\mathbf {IPF}{'}^{\iota }$ and $\mathbf {CPF}{'}^{\iota }$ by adding (CA) (with an inference line over it to indicate its derivation from no premisses) $\mathbf {IPF}{'}^{\iota 1}$ and $\mathbf {CPF}{'}^{\iota 1}$ . These systems raise interesting questions regarding harmony.

(CA) is an introduction rule for $\iota $ : it licences the derivation of identities flanked by an $\iota $ term, as does $(\iota I)$ . It also licences new inferences, in particular, its instances, which were not derivable in $\mathbf {IPF}{'}^{\iota }$ and $\mathbf {CPF}{'}^{\iota }$ . But the new formulas are never derived at the cost of maximal formulas.

Theorem 7. Deductions in $\mathbf {IPF}{'}^{\iota 1}$ and $\mathbf {CPF}{'}^{\iota 1}$ can be brought into normal form.

Proof. Mutatis mutandis the proof proceeds as for Theorems 5 and 6, by noting the following. (1) Using (CA) as the major premise in $(\iota E_1)$ and $(\iota E_2)$ is redundant:

In both cases, keep only $\Sigma $ and continue the deduction with the rule applied to the lower $u=t$ . Due to the restriction on $(\iota E_1)$ and $(\iota E_2)$ , t is an atomic term, so this is the only case that needs to be considered. (2) Deriving $\iota x (x=t)=t$ by $(\bot E_C)$ is also redundant. Anything above this conclusion can be deleted and $\iota x (x=t)=t$ derived by (CA) instead. If the conclusion of $(\bot E_C)$ is $t=\iota x(x=t)$ , derive it from (CA) by symmetry, deleting all the rest. The situation considered in Andou’s method to prove normalisation for the classical systems then reduces to the two cases displayed above.

(CA) affords new grounds for the derivation of formulas with $\iota $ terms. It does not, however, afford any new consequences of such formulas that are specifically to do with $\iota $ . This points to a misbalance and a lack of harmony: $(\iota E_1)$ and $(\iota E_2)$ are too weak relative to (CA). In Dummett’s terminology the rules are not stable. We’d expect further elimination rules to balance (CA) and permit the derivation of new consequences that do have something to do with the meaning of $\iota $ rather than just positive free logic without it. There are, of course, new consequences to do with identity. In particular, using (CA) as the major premise of $(=E)$ , formulas of the form $A_{\iota x(x=t)}^y$ can be simplified to $A_t^y$ . A number of philosophical questions arise. Is this misbalance in the rules problematic for an account in which the meaning of $\iota $ is supposed to be defined by the rules of inference governing it? If it is, what would a suitable additional elimination rule be? Or rather, as from a proof-theoretic perspective rules are preferable to axioms, what would additional introduction and elimination rules for $\iota $ be that permit us to prove (CA)? Is there a misbalance between the rules for $\iota $ and $=$ ? If so, how to balance it out? I shall leave these questions as suggestions for further work.

In the light of the previous restrictions on $\iota $ rules, it is worth observing that if we add the rule $(\exists i)$ of §8.1, (CA) can be restricted to atomic t. Choosing a fresh parameter a, by $(=E)\, a=\iota xA, \iota x(x=a)=a\vdash \iota x(x=\iota xA)=\iota xA$ , hence by $(\exists i)$ and the fact that (CA) follows from no premises, $\vdash \iota x(x=\iota xA)=\iota xA$ . It can then also be established that (CA) need never be the major premise of $(=E)$ . To illustrate with one case, instead of using $\iota x(x=t)=t$ , take a fresh parameter a to derive $a=t, \iota x(x=t)=t\vdash \iota x(x=t)=a$ , then by two applications of $(=E)$ from $A_{\iota x(x=t)}^y$ derive $A_t^y$ , discharge $a=t$ by $(\exists i)$ . But (CA) has been used as a minor premise directly above a major premise of $(=E)$ , so this looks to me like cheating and I am not sure about the significance of the result.

7.2 FD2

Recall (FD2): $\iota xA=t\leftrightarrow \forall x (x=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=x))$ . One half of (FD2) follows from ( $LA$ ).

Lemma 4. $(\mathrm {LA}) \vdash \iota xA=t\rightarrow \forall x (x=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=x)).$

Proof. Where a is a fresh parameter, positive free logic gives ( $LA$ ), $\iota xA=a,\exists !a\vdash \forall y(A_y^x\leftrightarrow y=a))$ and $\iota xA=t, a=t\vdash \iota xA=a$ , so ( $LA$ ), $\iota xA=t, a=t, \exists ! a\vdash \forall y(A_y^x\leftrightarrow y=a))$ . Conversely, ( $LA$ ), $\exists !a, \forall y(A_y^x\leftrightarrow y=a))\vdash \iota xA=a$ , and also $\iota xA=a, \iota xA=t\vdash a=t$ , hence ( $LA$ ), $\iota xA=t, \exists !a, \forall y(A_y^x\leftrightarrow y=a))\vdash a=t$ . The result follows by $(\leftrightarrow I)$ and $(\forall I)$ .

This means that formalising $\mathbf {FD2}$ in natural deduction requires no further elimination rules besides $(\iota E_1)$ and $(\iota E_2)$ . It only requires either further introduction rules or a strengthening of $(\iota I)$ that permits the deduction of its other half:

1. (FD2 ^rl ) $\forall x (x=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=x))\rightarrow \iota xA=t.$

Transposing this half of (FD2) into a rule of natural deduction produces the following monstrosityFootnote ¹⁴ :

Although it is difficult to spell out the notion of harmony precisely, it is an educated guess that most philosophers working in the field will agree that this rule is not in harmony with $(\iota E_1)$ and $(\iota E_2)$ . The problem is the nested biconditional of ( $FD2^{lr}$ ), which is responsible for the discharge of $\forall y(A_y^x\leftrightarrow y=a)$ above the deduction of $a=t$ . I see no way of avoiding this. This is unfortunate for those who were hoping to develop a proof-theoretic semantics for $\mathbf {FD2}$ , fortunate for those wish to exclude it. And indeed: the motivation for the chosen object theory is decidedly model-theoretic. That it may have to be set aside from the proof-theoretic perspective may thus not come as a surprise.

8 Alternative theories of definite descriptions

8.1 FDA

With $(\iota I')$ instead of $(\iota I)$ , the restriction to a single occurrence of an $\iota $ term can no longer be established as in Lemma 3, as $(=I^{nG})$ requires the existence premise that is lacking. This can, however, be achieved by an alternative rule equivalent to one given by Garson [Reference Garson8, 259f]:

where a is neither free in t, nor in C, nor in any undischarged assumptions it depends on except those of the assumption class of $a=t$ .

Garson requires this rule to prove the completeness of some systems of quantified modal logic. It is not required for the completeness of $\mathbf {CPF}$ relative to its standard semantics. The following is the case.

Theorem 8. $(\exists i)$ is (a) admissible but (b) not derivable in $\mathbf {CPF}^{\iota }$ .

Proof. (a) That $(\exists i)$ is admissible is easily seen: deleting any application of $(\exists i)$ and replacing a by t results in a correct deduction. (b) Proof sketch for those familiar with the dual domain semantics for $\mathbf {CPF}^{\iota }$ . Consider a semantics that is like the standard one (outer domain $\mathfrak {D}$ and inner domain $\mathfrak {E}\subseteq \mathfrak {D}$ over which $\exists !$ is interpreted), but with an additional element $\ast $ not in the outer domain. The interpretation of constants and $\iota $ terms stays untouched, i.e., they are interpreted in the outer domain, but variables ranger over $\mathfrak {D}\cup \{\ast \}$ . Then all rules of $\mathbf {CPF}^{\iota }$ preserve validity. But $a=t$ is false, if $v(a)=\ast $ , for any closed term t, and so $(\exists i)$ does not preserve validity.Footnote ¹⁵

A fortiori $(\exists i)$ is admissible but not derivable in $\mathbf {IPF}^{\iota }$ .

$(\exists i)$ permits the restriction of $(\exists I)$ and $(\forall E)$ to atomic instantiating terms.

Lemma 5. Given $(\exists i)$ , $(\exists I)$ and $(\forall E)$ may be restricted to atomic terms.

Proof. Replace an application of $(\exists I)$ in which t is complex by the following:

Similarly for $(\forall E)$ .

The restrictions of the $\iota $ rules can also be established.

Lemma 6. Given $(=I)$ , $(=E)$ and $(\exists i)$ , $(\iota I')$ , $(\iota E_1)$ and $(\iota E_2)$ can be restricted to the single occurrence of an $\iota $ term where it is displayed in the rules.

Proof. Modify the deductions that prove Lemma 3: change applications of $(=I^{nG})$ to $(\exists i)$ by deleting its left premise and anything above it.

Let $\mathbf {IPF}^{\iota A}$ be the system that results from $\mathbf {IPF}{'}^{\iota }$ by replacing $(\iota I)$ by $(\iota I')$ and $(=I^{nG})$ by $(\exists i)$ . Similarly for $\mathbf {CPF}^{\iota A}$ . Permutative reduction procedures work for $(\exists i)$ as for $(=I^{nG})$ , and the reduction procedures for the rules for $\iota $ are almost the same: observe that in the latter the leftmost premise of $(\iota I)$ is idle, and so that it is missing altogether in $(\iota I')$ makes no essential difference.

Theorem 9. Deductions in $\mathbf {IPF}^{\iota A}$ and $\mathbf {CPF}^{\iota A}$ can be brought into normal form.

Proof. Mutatis mutandis the proofs proceed as for $\mathbf {IPF}{'}^{\iota }$ and $\mathbf {CPF}{'}^{\iota }$ .

$(\exists i)$ could have been used for the systems of the previous sections, too. It has the advantage over $(=I^{nG})$ that it cannot so easily be objected that it hides a maximal formula. However, as it is admissible but not derivable, while $(=I^{nG})$ is derivable, it seemed preferable to use the latter in the systems with $(\iota I)$ , so that the formalised theory of definite descriptions is Lambert’s, not a variation thereof. It is also not clear whether $(\exists i)$ really is preferable over $(=I^{nG})$ from the philosophical perspective. Its intuitive content is that for any object picked out by a definite description, I can introduce an ad hoc proper name and reason with that instead of the description. In Kripke’s words, I can baptise the object picked out by the description. Arguably I can only do that with things that exist: what doesn’t exist cannot be baptised. So for philosophical reasons there remains a hidden existence assumption in $(\exists i)$ that is made explicit in $(=I^{nG})$ . An examination of these matters must await another occasion.

8.2 Lambert’s serendipitous theory

At one point Lambert writes that the following axiomatises $\mathbf {FD2}$ [Reference Lambert26, 32]:

1. (FDS) $\iota xA=t\leftrightarrow \forall x (x=t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y=t)))$ .

Note the subtle difference from $\iota xA=t\leftrightarrow \forall x (x=t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y=x)))$ ,Footnote ¹⁶ the latter being equivalent to (FD2). This is a typo. (FD2) and (FDS) are not equivalent. (FDS), however, does not face the difficulties of casting it into rules of natural deduction that (FD2) faced. For the purposes of proof-theoretic semantics, Lambert’s typo proves to be serendipitous.

Instead of adding (FDS) to $\mathbf {CPF}$ , I’ll consider a slightly different axiomatisation of the resulting theory.

One half of (FDS) follows from the left to right half of ( $LA$ ).

Lemma 7. $(\mathrm {LA}) \vdash \iota xA=t\rightarrow \forall x (x=t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y=t)))$ .

Proof. By positive free logic ( $LA$ ), $\iota xA=t, \exists !a, \vdash \forall y(A_y^x\leftrightarrow y=a)$ , and so ( $LA$ ), $\iota xA=t, \exists !a\vdash A_a^x\land \forall y(A_y^x\rightarrow y=a)$ . By $(=E)$ , ( $LA$ ), $\iota xA=t, \exists !a, a=t\vdash A_a^x\land \forall y(A_y^x\rightarrow y=t)$ . Conversely, $\exists !a, A_a^x\land \forall y(A_y^x\rightarrow y=t)\vdash a=t$ , so by $(\leftrightarrow I)$ , ( $LA$ ), $\iota xA=t, \exists !a\vdash a=t\leftrightarrow (A_a^x\land \forall y(A_y^x\rightarrow y=t))$ and the result follows by $(\forall I)$ and $(\rightarrow I)$ .

As $\exists !a, A_a^x\land \forall y(A_y^x\rightarrow y=t)\vdash a=t$ just by positive free logic, it is possible to weaken the antecedent of the right to left half of (FDS). The following suffices:

1. (FDS′) $\forall x (x=t\rightarrow (A\land \forall y(A_y^x\rightarrow y=t)))\rightarrow \iota xA=t$ .

Lemma 8. ( $FDS'$ ) implies the right to left half of ( $LA$ ).

Proof. $\forall y(A_z^x\leftrightarrow y=a), \exists !a\vdash A_a^x\land \forall y(A_z^x\rightarrow y=a)$ . Apply $(=E)$ to derive $\forall y(A_z^x\leftrightarrow y=a), \exists !a, b=a\vdash A_b^x\land \forall y(A_z^x\rightarrow y=a)$ , hence by $(\rightarrow I)$ and $(\forall I)\, \forall y (A_z^x\leftrightarrow y=a), \exists !a\vdash \forall x(x=a\rightarrow (A\land \forall y(A_z^x\rightarrow y=a))$ . Apply ( $FDS'$ ) to derive ( $FDS'$ ), $\forall y(A_z^x\leftrightarrow y=a), \exists !a\vdash \iota xA=a$ . The result follows by $(\rightarrow I)$ and $(\forall I)$ .

Thus let $\mathbf {FDS}$ be the system that results from adding ( $LA^{lr}$ ) and ( $FDS'$ ) to $\mathbf {CPF}$ .

Next we’ll show that $\mathbf {FDS}$ is weaker than $\mathbf {FD2}$ . The right hand side of (FD2) implies the right hand side of (FDS).

Lemma 9. $\forall x(x=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=x))\vdash \forall x(x=t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y=t)))$ .

Proof. $\forall x(x=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=x)), \exists !a\vdash a=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=a)$ . Furthermore $\forall y(A_y^x\leftrightarrow y=a), \exists !a\vdash A_a^x$ and $\forall y(A_y^x\leftrightarrow y=a), a=t\vdash \forall y(A_y^x\rightarrow y=t)$ , hence (1) $\forall x(x=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=x)), \exists !a, a=t\vdash A_a^x\land \forall y(A_y^x\rightarrow y=t)$ . Also (2) $\exists !a, A_a^x\land \forall y(A_y^x\rightarrow y=t)\vdash a=t$ . Hence by $(\leftrightarrow I)$ from (1) and (2) $\forall x(x=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=x)), \exists !a\vdash a=t\leftrightarrow (A_a^x\land \forall y(A_y^x\rightarrow y=t)$ , and so by $(\forall I)$ , $\forall x(x=t \leftrightarrow \forall y(A_y^x\leftrightarrow y=x))\vdash \forall x(x=t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y=t))$ .

Lemma 10. $(\textit {FD2})\vdash (\textit {FDS})$ .

Proof. From Lemmas 7 and 9.

The two systems are close. The right hand side of (FDS) implies the left to right direction of the right hand side of (FD2).

Lemma 11. ${\forall x(x=t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y=t)))\vdash \forall x(x=t\rightarrow \forall y(A_y^x\leftrightarrow y=x))}$ .

Proof. ${\forall x(x\kern1.5pt{=}\kern1.5pt t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y\kern1.5pt{=}\kern1.5pt t))), \exists !a\vdash a\kern1.5pt{=}\kern1.5pt t\leftrightarrow (A_a^x\land \forall y(A_y^x\rightarrow y = t)}$ , so $\forall x(x\hspace{-0.5pt}=\hspace{-0.5pt}t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y\hspace{-0.5pt}=\hspace{-0.5pt}t)), \exists !a, a\hspace{-0.5pt}=\hspace{-0.5pt}t\vdash A_a^x\land \forall y(A_y^x\rightarrow y\hspace{-0.5pt}=\hspace{-0.5pt}t)$ . Use $(=E)$ to derive $\forall x(x=t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y=t), \exists !a, a=t\vdash A_a^x\land \forall y(A_y^x\rightarrow y=a)$ . As $A_a^x\land \forall y(A_y^x\rightarrow y=a)\vdash \forall y(A_y^x\leftrightarrow y=x))$ , the result follows.

But they are not the same. The right hand side of (FDS) does not imply the right to left direction of the right hand side of (FD2).

Lemma 12. $\forall x(x\hspace{-0.5pt}=\hspace{-0.5pt}t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y\hspace{-0.5pt}=\hspace{-0.5pt}t)))\not \vdash \forall x(\forall y(A_y^x\leftrightarrow y\hspace{-0.5pt}=\hspace{-0.5pt}x)\rightarrow x\hspace{-0.5pt}=\hspace{-0.5pt}t)$ .

Proof. Sketch for those familiar with the dual domain semantics for $\mathbf {CPF}$ . Suppose t refers to an object in the outer domain, and there is exactly one A in the inner domain. Then $\forall x(\forall y(A_y^x\leftrightarrow y=x)\rightarrow x=t)$ is false. $\forall y(A_y^x\rightarrow y=t)$ is also false. Whenever x is assigned an object in the inner domain, $x=t$ is not satisfied. Hence $x=t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y=t))$ is satisfied, whenever x is assigned an object in the inner domain, and hence $\forall x(x=t\leftrightarrow (A\land \forall y(A_y^x\rightarrow y=t)))$ is true.

Theorem 10. If $\Gamma \vdash _{\mathbf {FDS}} A$ , then $\Gamma \vdash _{\mathbf {FD2}} A$ , but not conversely.

Proof. From Lemmas 10 and 12.

( $FDS'$ ) is easily cast into rule form:

where a and b are not free in F nor in t and does not occur in any undischarged assumptions in $\Xi $ and $\Pi $ except those in the assumption classes displayed.

Lemma 13. (a) ( $FDS'$ ) and $(\iota I^S)$ are interderivable. (b) The right to left half of ( $LA$ ) is derivable from $(\iota I^S)$ , the other half from $(\iota E_1)$ and $(\iota E_2)$ .

Proof. Exercise.

As for $\mathbf {CPF}^{\iota A}$ , we need Garson’s $(\exists i)$ to prove normalisation. Theorem 8 goes through as before.Footnote ¹⁷ So does Lemma 5. Concerning Lemma 6, it suffices to consider $(\iota I^S)$ , the elimination rules staying put. If t is a complex term, replace it by a fresh parameter c, deduce $\iota xF=t$ from $\iota xF=c$ and $c=t$ , then apply $(\exists i)$ to discharge the latter.

We therefore get systems with the same neat properties as $\mathbf {IPF}^{\iota A}$ and $\mathbf {CPF}^{\iota A}$ if we replace $(\iota I')$ by $(\iota I^S)$ , and, as before, restrict occurrences of $\iota $ terms in $\iota $ rules to where they are displayed in the rules. Call the resulting systems $\mathbf {IPF}^{\iota S}$ and $\mathbf {CPF}^{\iota S}$ .

Theorem 11. $\Gamma \vdash _{\mathbf {CPF}^{\iota S}} A$ iff $\Gamma \vdash _{\mathbf {FDS}} A$ .

Proof. From Lemma 13.

Theorem 12. (a) If $\Gamma \vdash _{\mathbf {CPF}^{\iota A}} A$ , then $\Gamma \vdash _{\mathbf {CPF}^{\iota 'S}} A$ . (b) If $\Gamma \vdash _{\mathbf {IPF}^{\iota A}} A$ , then $\Gamma \vdash _{\mathbf {IPF}^{\iota 'S}} A$ .

Proof. $(\iota I')$ is the special case of $\iota I^S)$ where a and b are the same parameter and $a=t$ above the right premise discharged vacuously. Replacing $(\iota I')$ by $(\iota I^S)$ therefore results in a stronger system, as $(\iota I^S)$ permits the discharge of more assumptions, and so consequences are derivable with it that are not derivable without it.

Now for what we are here for, the normalisation theorem.

Theorem 13. Deductions in $\mathbf {IPF}^{\iota S}$ and $\mathbf {CPF}^{\iota S}$ can be brought into normal form.

Proof. The new rule being an introduction, it suffices to consider maximal formulas that are concluded by $(\iota I^S)$ and eliminated by $(\iota E_1)$ and $(\iota E_2)$ . The former case is as for $\mathbf {CPF}^{\iota A}$ . The latter case goes as follows:

The proof now proceeds mutatis mutandis as in the previous cases.

$\mathbf {IPF}^{\iota S}$ and $\mathbf {CPF}^{\iota S}$ raise questions concerning harmony. They have the same elimination rules for $\iota $ as do $\mathbf {IPF}{'}^{\iota }$ and $\mathbf {CPF}{'}^{\iota }$ , but a different introduction rule. There is a thought in proof-theoretic semantics that one and the same collection of elimination rules should not be harmonious with different, non-equivalent introduction rules (and analogously for introduction rules).

The reason the normalisation procedure works for $\mathbf {IPF}^{\iota S}$ and $\mathbf {CPF}^{\iota S}$ is that $\vdash t=t$ . Even if $t=t$ required $\exists !t$ , as in negative free logic, the procedure would work, as the latter is given as a premise. Once more, questions concerning the relation between $\iota $ and $=$ arise, and the dependence of the meaning of $\iota $ on that of $=$ . However, it strikes me as if an appeal to rules for $=$ in the normalisation procedure can hardly be objectionable, as the rules for $\iota $ appeal to $=$ . That the meaning of the former can only be defined in terms of the latter supplies no valid objection to defining its meaning in terms of rules of inference.

8.3 Hintikka’s system

Hintikka and Lambert proposed similar theories of definite descriptions around the same time. To honour them both with an axiom, I shall name the following Hintikka’s Axiom Footnote ¹⁸ :

1. (HA) $\iota xA=t\leftrightarrow \forall y(A_y^x\leftrightarrow y=t)$ .

As t is any term, (HA) requires fewer existence assumptions than ( $LA$ ) in its use in deductions, because t need not exist, and so to formalise Hintikka’s theory of definite descriptions in natural deduction, a correspondingly weakened elimination rule is required:

Lemma 14. $(\iota I')$ , $(\iota E_1)$ , $(\iota E_2')$ and (HA) are interderivable.

Proof. Exercise.

t and u can be restricted to atomic terms, for the same reasons as in the case of $\mathbf {IPF}^{\iota A}$ and $\mathbf {CPF}^{\iota A}$ . Call the systems that result by replacing $(\iota E_2)$ by $(\iota E_2')$ in them $\mathbf {IPF}^{\iota H}$ and $\mathbf {CPF}^{\iota H}$ .

Theorem 14. Deductions in $\mathbf {IPF}^{\iota H}$ and $\mathbf {CPF}^{\iota H}$ can be brought into normal form.

Proof. The reduction procedure for maximal formulas arising from $(\iota I')$ and $(\iota E_2')$ is evidently:

The proof now proceeds mutatis mutandis as in the previous cases.

We are now faced with a rather interesting situation. Only two formulas are discharged above the right premise of $(\iota I')$ , and these correspond precisely to the two minor premises of $(\iota E_2')$ . An assumption corresponding to the third premise of $(\iota E_2)$ , however, could be discharged above the right premise of $(\iota I')$ , as $\exists !t$ is derivable from $\exists !a$ and $a=t$ . The theories of definite descriptions of $\mathbf {IPF}^{\iota A}$ and $\mathbf {CPF}^{\iota A}$ and of $\mathbf {IPF}^{\iota H}$ and $\mathbf {CPF}^{\iota H}$ are not the same. The instance of (HA) for a term t is not derivable from ( $LA$ ) unless t exists, which is the additional assumption in $(\iota E_2)$ . This points to a disharmony somewhere. The question is where. Which set of rules is harmonious, those of $\mathbf {IPF}^{\iota A}$ and $\mathbf {CPF}^{\iota A}$ or those of $\mathbf {IPF}^{\iota H}$ and $\mathbf {CPF}^{\iota H}$ ?

One may be inclined to solve this conundrum by declaring that so much the worse for both: neither set of rules satisfies the criteria of proof-theoretic semantics. That option, however, isn’t really on the table. There is the thought that introduction rules can be laid down as we please: they are self-justifying, as Dummett says [Reference Dummett4, 251]. Harmony determines the elimination rules. Others prefer to see matters the other way round and treat elimination rules as self-justifying, and introduction rules determined by harmony from them.

I shan’t attempt to address this question here, and merely note it as a further philosophical issue that arises for a proof-theoretic semantics for the $\iota $ operator.

9 Concluding philosophical remarks

Positive free logic is the preferred logic of many free logicians. It is decidedly un-Russellian, while negative free logic remains near to the Russellian paradigm. The proof theory of positive free logic is simpler than that of negative free logic. It is in this sense closer to non-free classical and intuitionist logic in that it merely restricts the rules for the quantifiers.

Proving a normalisation theorem for $\mathbf {IPF}$ and $\mathbf {CPF}$ was straightforward, but when it comes to definite descriptions, the systems had to be modified by adding the rule $(=I^{nG})$ and normalisation was proved for $\mathbf {IPF}{'}^{\iota }$ and $\mathbf {CPF}{'}^{\iota }$ . This meant that $(\forall E)$ and $(\exists I)$ can be restricted to atomic instantiating terms and furthermore, the $\iota $ rules can be restricted to a single occurrence of an $\iota $ term where it is displayed in the rules, all other terms being atomic. This may be of philosophical relevance, if the rules governing $\iota $ are to define its meaning.

Considerations from proof-theoretic semantics suggested a misbalance between the introduction and elimination rules for the $\iota $ operator that formalises Lambert’s minimal theory of definite descriptions in positive free logic, i.e., $\mathbf {IPF}{'}^{\iota }$ and $\mathbf {CPF}{'}^{\iota }$ . The problem is solved by dropping an existence premise from $(\iota I)$ .

The rule $(\iota I')$ is arguably in perfect harmony with $(\iota E_1)$ and $(\iota E_2)$ . Normalisation theorems were proved for $\mathbf {IPF}^{\iota A}$ and $\mathbf {CPF}^{\iota A}$ in which $(=I^{nG})$ is replaced by $(\exists i)$ , which incidentally drops an existence premise from the former, just as $(\iota I')$ drops an existence premise from $(\iota I)$ . The result is a new theory of definite descriptions conforming to principles of proof-theoretic semantics.

The matter is not so easily settled, however, and proof-theoretic considerations raise a number of questions.

It was observed that normalisation theorems are provable for $\mathbf {IPF}{'}^{\iota 1}$ and $\mathbf {CPF}{'}^{\iota 1}$ , arising from $\mathbf {IPF}{'}^{\iota }$ and $\mathbf {CPF}{'}^{\iota }$ by adding (CA) as an axiom. These systems, equivalent to Lambert’s $\mathbf {FD1}$ , therefore satisfy a necessary condition for proof-theoretic semantics. But the rules exhibit a misbalance, as (CA) affords grounds for deriving formulas with $\iota $ to which there are no corresponding elimination rules. The question arises whether alternative rules can be formulated that rectify this and rebalance the rules. (CA) is provable in $\mathbf {IPF}^{\iota A}$ and $\mathbf {CPF}^{\iota A}$ , but these systems are stronger than $\mathbf {IPF}{'}^{\iota 1}$ and $\mathbf {CPF}{'}^{\iota 1}$ .

No proof-theoretically satisfactory rules have been found for Lambert’s $\mathbf {FD2}$ , which formalises a chosen object theory of improper definite descriptions and ‘non-denoting’ names. It was suggested that this is fair enough, as the motivation for this theory is model-theoretic in spirit: there is, after all, a crucial claim concerning reference at its heart.

Four further theories of definite descriptions were considered. $\mathbf {IPF}^{\iota S}$ and $\mathbf {CPF}^{\iota S}$ have as their source a serendipitous typo in a paper of Lambert’s. $\mathbf {IPF}^{\iota H}$ and $\mathbf {CPF}^{\iota H}$ have their origin in a charitable reading of an axiom of Hintikka’s.

In the latter, an existence assumption is dropped from $(\iota E_2)$ of $\mathbf {IPF}^{\iota A}$ and $\mathbf {CPF}^{\iota A}$ . The puzzle now is that the collection of rules $(\iota I'), (\iota E_1), (\iota E_2)$ of $\mathbf {IPF}^{\iota A}$ and $\mathbf {CPF}^{\iota A}$ and the collection $(\iota I'), (\iota E_1), (\iota E_2')$ of $\mathbf {IPF}^{\iota H}$ and $\mathbf {CPF}^{\iota H}$ appear to be equally harmonious. No significant difference can be discerned, as the dropped existence assumption of $(\iota E_2')$ corresponds to a discharged hypothesis above the right hand premise of $(\iota I')$ that it is unnecessary to mention explicitly, because it is derivable from the other two assumptions discharged there.

$(\iota I^S)$ of $\mathbf {IPF}^{\iota S}$ and $\mathbf {CPF}^{\iota S}$ permits a more complex pattern of discharge than $(\iota I')$ . Yet this does not appear to upset harmony in any way. Adding a corresponding premises to $(\iota E_2)$ would amount to adding $t=t$ , which is redundant. As before, omissions of redundancies can hardly upset harmony.

These observations point, I think, to an issue that has been underinvestigated in proof-theoretic semantics: the discharge of assumptions. The question is how to accommodate different patterns of discharge, while premises and conclusions of rules stay the same, within the notion of harmony. As far as I can see there is no literature at all on this issue, although it is of some importance, seeing that classical logic requires rules that discharge assumptions with negation or implication as main operator.

It is my contention that these considerations open up a fruitful field of enquiry for the proof-theoretic semantics for $\iota $ and term-forming operators, and, indeed, proof-theoretic semantics in general.