Necessities and Necessary Truths. Proof-Theoretically.

Abstract

In his seminal “Outline of a Theory of Truth” Kripke (1975) proposed understanding modal predicates as complex expressions defined by a suitable modal operator and a truth predicate. In the case of the alethic modality of logical or metaphysical necessity, this proposal amounts to understanding the modal predicate ‘is necessary’ as the complex predicate ‘is necessarily true’. In this piece we work out the details of Kripke’s proposal, which we label the Kripke reduction, from a proof-theoretic perspective. To this end we construct a theory for the modal predicate and a theory of truth formulated in a language with a modal operator and show that the modal predicate theory is interpretable in the theory of truth where the interpretation translates the modal predicate ‘N’ by the complex predicate ‘☐T’, the truth predicate modified by the modal operator. In addition, we show that our work can be viewed as the proof-theoretic counterpart to the semantic Kripke reduction recently carried out by Halbach and Welch (2009), which is based on Kripke’s theory of truth.

1. Introduction

In his seminal “Outline of a Theory of Truth” Kripke (1975) proposed understanding modal predicates by appeal to a corresponding modal operator and the truth predicate. He writes:

Kripke’s suggestion is thus to define the modal predicate in a language containing a truth predicate and a modal operator. The hope would be that by defining the modal predicate in such a way, one arrives at a workable predicate approach to modality that combines the advantages of the operator approach with the benefits of the predicate approach. It is often thought that the predicate approach to modality is preferable to the operator approach because of its greater expressive strength. For example, within the predicate approach it is possible to quantify over the argument position of the modality at stake where nothing of the like is possible within the operator approach without moving to some restricted form of second-order logic. Another advantage of the predicate approach is that it ties well with the so-called relational analysis of propositional attitudes, which views propositional attitudes as relations between agents and propositions.

Kripke’s proposal lends itself to two possible interpretations. On the one hand it may serve as a defense of the predicate approach against the backdrop of Montague’s theorem.[1]

Montague’s theorem shows that the standard principles of modal operator logic cannot be adopted within the predicate setting for otherwise inconsistency arises. This result has often been viewed as a knock-down argument against predicate approaches to modality because it allegedly shows that no intuitive and philosophically satisfactory account of modalities qua predicates is available. Yet with Kripke’s proposal we possess a strategy for providing such, arguably, intuitive and philosophically satisfactory predicate approaches to modality.

On the other hand, an alternative understanding of Kripke’s proposal reconstructs it as an argument in favor of operator approaches to modality. According to this interpretation, reducing the modal predicate to a modal operator and the truth predicate shows that the expressive strength of the predicate approach (to modality) can be accounted for within the operator setting, i.e., we can dispense with primitive modal predicates and stick to modal operators. Halbach and Welch (2009) view Kripke’s proposal in this way and, accordingly, take Kripke’s proposal to show that the expressive strength of the predicate approach can be recovered within the operator setting. Halbach and Welch strengthen their argument by— instead of defining the modal predicate in the modal operator language—reducing a semantic theory of the modal predicate to a semantic theory of truth formulated in a modal operator language. That is, they show that understanding the modal predicate ‘N’ as the complex predicate ‘☐T’ results in a truth preserving translation with respect to the two semantics they put forward.

Reducing a semantic theory of a modal predicate to a semantic theory of truth formulated in a modal operator language has the advantage over simply defining a modal predicate in the latter language that it may serve as a defense of operator approaches to modality against proponents of the predicate approach. By using this strategy one may show that we can recover the modal predicate within the operator language. The modal predicate therefore proves to be dispensable. In contrast, if we define a modal predicate in the operator language we only show that we may define some sentential predicate that need not be of any appeal to the proponent of the predicate approach to modality. Indeed she may not even consider this predicate to be a modal predicate. In case of the reduction strategy, if the semantic theory of the modal predicate is accepted and if, in addition, we consider the expressive strength to be the sole argument in favor of the predicate approach, then the modal predicate is dispensable and we may stick to the operator approach. Obviously, the fact that it is possible to carry out a reduction does not imply that we must, but considering the fact that modal operator logic is well entrenched in philosophical and mathematical logic while the predicate approach is a niche phenomenon from this perspective, there seems to be good reason for dismissing the predicate approach as superfluous and for sticking to the “standard” operator approach to modality. Viewed from this perspective Halbach and Welch’s reduction puts some pressure on the proponent of the predicate approach to abandon his theory of modality in favor of the operator approach.

In this paper we show that Kripke’s proposal can be carried out from a proof-theoretic perspective and thereby supplement Halbach and Welch’s reduction by its proof-theoretic counterpart. To this end we construct two axiomatic theories: One axiomatizes the modal predicate; the other is a theory of truth formulated in a language containing a modal operator. We show that the theory of the modal predicate can be interpreted within (“reduced to”) the theory of truth formulated in the modal operator language where the modal predicate is translated as the truth predicate modified by an appropriate modal operator and, additionally, that the two theories match the two semantics of Halbach and Welch used for carrying out their reduction.

The structure of the paper then is as follows. In the next section we motivate our work from a philosophical perspective. In particular, we clarify what kind of reduction we are attempting, why it may be considered as a proof-theoretic counterpart of Halbach and Welch’s work and why it is philosophically interesting. In section 3 we construct the theory of the modal predicate and the theory of truth in a modal operator language. Next we reduce the theory of the modal predicate to the theory of truth, that is we show that the theory of the modal predicate can be interpreted in the theory of truth (section 4). We then turn to semantic aspects and introduce the two semantics that Halbach and Welch use to carry out their reduction (section 5). Finally, we show that the two theories capture the relevant semantics in an interesting way (section 6). We end the paper with a summary and evaluation of our findings.

2. The Syntactic Reduction and Its Two Possible Interpretations

As we have mentioned, Halbach and Welch view their reduction as an argument in favor of the operator approach to modality. Their idea is that the sole argument for opting for a predicate approach to modality is the alleged expressive strength of the predicate approach. Accordingly, they take their reduction to show that the expressive strength of the predicate approach can be recovered within the operator approach, as the modal predicate can be reduced to a modal operator and the truth predicate. However, their reduction is carried out solely in semantic terms: they show that the translation is truth preserving with respect to the two semantics employed. Yet, both semantics are based on possible world semantics and therefore the reduction is convincing only if one accepts possible worlds or similar notions in the analysis of modal notions. Within the predicate approach, in contrast to the operator approach, there is no interpretation problem, i.e., we are not forced to move to possible worlds to provide an interpretation of the modal notion—standard first-order semantics will do the job. Consequently, the proponent of the predicate approach to modality who dislikes possible worlds will remain unconvinced by the semantic reduction proposed by Halbach and Welch.[2] The reduction we are going to propose will be carried out syntactically by employing proof-theoretic means only and therefore simple skepticism toward possible worlds will no longer do. Rather, such a syntactic reduction, if successful both from a philosophical and technical perspective, would, together with Halbach and Welch’s semantic reduction, put the proponent of the predicate approach under considerable pressure—at least if one were to follow Halbach and Welch’s dialectic.

Of course, this kind of argument can only be convincing if the reduction we propose is a plausible reduction in its own right and so far, without further specification, it remains unclear what it means to carry out the reduction by purely proof-theoretic means.[3] We shall now attempt to fill this gap. To this end, let us first reconsider the reduction carried out by Halbach and Welch in more detail. Halbach and Welch construct an intended model for both the language of the modal predicate and the language of the modal operator plus the truth predicate. Let us call the first model M_N and the second model M_☐T. It is assumed that the two languages only differ in the way they conceive of the modal notion, that is, whether they conceive of the modal notion as a predicate or an operator. Next Halbach and Welch provide a translation function 𝜌 from the language of the modal predicate \(\mathcal{L}_{N}\) to the language of the modal operator plus truth predicate \(\mathcal{L}_{\Box T}\). The translation function translates the modal predicate ‘N’ as ‘☐T’ but leaves the remaining vocabulary fixed. In particular the translation commutes with the logical connectives and quantifiers. Thus 𝜌 clearly captures the idea behind Kripke’s proposal and should therefore be considered as a philosophically interesting translation function that translates formulas of \(\mathcal{L}_{N}\) in an intended way.[4] Halbach and Welch show that for all sentences φ of \(\mathcal{L}_{N}\)

In a way, (SR) asserts that whether we treat the modal predicate as a primitive predicate or as a complex predicate that is constructed using the modal operator and the truth predicate does not affect the truth of a modal statement. Therefore, following the dialectics of Halbach and Welch, the modal predicate is dispensable and we can stick to modal operators. With this in mind let us return to outlining the proof-theoretic counterpart of Halbach and Welch’s reduction. The idea is to replace the semantic notions used in (SR) by purely syntactic or proof-theoretic notions. Consequently, we shall replace the notion of truth in a model by the notion of derivability in a theory. This requires developing two theories, which we shall call \(\mathsf{T}_N\) and \(\mathsf{T}_{\Box T}\) for now. \(\mathsf{T}_N\) is the theory of the modal predicate formulated in the language \(\mathcal{L}_{N}\). \(\mathsf{T}_{\Box T}\) is the theory of truth formulated in the modal operator language \(\mathcal{L}_{\Box T}\) . We then show that for all φ ∈ \(\mathcal{L}_{N}\)

(PR) asserts that theoremhood is preserved modulo translation in moving from \(\mathsf{T}_N\) to \(\mathsf{T}_{\Box T}\). In more technical terms, because of the properties of the translation function, (PR) shows that \(\mathsf{T}_N\) is a subtheory of a definitorial extension of \(\mathsf{T}_{\Box T}\) where the arithmetical vocabulary is left unaltered. This is a fairly strong notion of reduction. In other words, 𝜌 is an unrelativized interpretation of \(\mathsf{T}_N\) in \(\mathsf{T}_{\Box T}\) in the sense of Tarski, Mostowski, and Robinson (1953).[5] This sets the syntactic reduction in (PR) apart from reductions where preservation of theoremhood is achieved by translating formulas of the source language in an unintended way.

Consequently, it seems fair to conclude that (PR) establishes from a proof-theoretic side what (SR) establishes from a semantic side, if one accepts \(\mathsf{T}_N\) and \(\mathsf{T}_{\Box T}\) as the intended theories of the languages and the notions involved.[6] For now, let us assume that \(\mathsf{T}_N\) and \(\mathsf{T}_{\Box T}\) were such theories, or at least plausible candidate theories, then it seems the proponent of the predicate approach can no longer resist the dialectics of Halbach and Welch by simply dismissing possible world semantics. Rather, she would also need to dismiss at least one of the two theories as apt characterizations of the notions at stake. Such a dismissal should not be taken lightly, however, because there is an asymmetry between rejecting possible world semantics in the case of the semantic reduction and of rejecting the modal theories and possible world semantics when we have both a semantic and a syntactic reduction. Whereas in the first case the modal semantics, i.e., possible world semantics, was, in a way, superfluous, as one can appeal to simple first-order semantics,[7] and as a last resort adopt a purely proof-theoretic account there is no obvious substitute available for the two theories appealed to in the syntactic reduction. As a consequence, simply rejecting the theories will not be sufficient, rather the proponent of the predicate approach would need to provide us with alternative, well-motivated theories for which the proposed reduction does not hold. This kind of worry is even more pressing in light of Montague’s theorem, which threatens the intelligibility of the predicate approach altogether. It therefore seems crucial for a proponent of the predicate approach to provide us with a positive account, that is, she has to offer a modal theory for which the “Kripke reduction” is not feasible. However, to date there has been little success in direction of such a theory. Consequently, if one subscribes to Halbach and Welch’s claim that the expressive strength is the sole argument favoring predicate approaches to modality, then a proof-theoretic counterpart of Halbach and Welch’s reduction puts the proponent of the predicate approach under considerable pressure given the enormous success of the operator approach in logic and philosophy.

However, in the introduction we have already suggested that if one thinks that predicate approaches are motivated independently of their alleged expressive strength, then the success of the reduction can be viewed as an argument in favor of the modal theory we are about to construct and thus ultimately as an argument in favor of predicate approaches to modality. The guiding idea is that since the predicate approach is motivated independently of its expressive strength and the success of the “Kripke reduction” (as we shall call the reduction from now on) shows that we have constructed a workable theory of modality where the modal notion is conceived as a predicate. This shows that contra Montague there are well motivated, intuitive and consistent accounts of modalities conceived as predicates. Moreover, the syntactic and semantic reduction taken together show that we can have both semantic and syntactic, that is, axiomatic theories of modal predicates. Incidentally, the modal theory we propose will match the semantics Halbach and Welch employ in their semantic reduction. On the one hand this shows that our syntactic reduction really is the proof-theoretic counterpart to Halbach and Welch’s reduction. On the other hand, Halbach and Welch’s work together with our proof-theoretic addendum may be viewed as a full-fledged defense of the predicate approach to modality against the challenges raised by Montague’s theorem and related inconsistency results. One might even hope that based on Kripke’s idea a general strategy for devising modal theories in which the modal notion is conceived as a predicate can be developed.[8]

3. The Theories Modal PKF and Operator PKF

In this section we introduce the theory of the modal predicate and the theory of truth formulated in a language containing a modal operator. Both theories will be formulated in non-classical logic, namely FDE or BDM (as Field 2008 would call it). The reason for our departure from classical logic is twofold. First, the semantics employed by Halbach and Welch is based on Kripke’s theory of truth, which is based on a partial evaluation scheme.[9] Formulating the modal theories in partial logic thus goes nicely with these semantics.[10] Second, if we wish to capture the semantics of Halbach and Welch in classical logic it proves necessary to introduce a primitive possibility predicate. This is a side effect of the so-called diverging inner and outer logic in classical axiomatizations of Kripke’s theory of truth[11] and may be nicely illustrated by reading the modal predicate following the spirit of the Kripke reduction as a modified truth predicate. Under this reading ‘necessarily true not’ would need to be equivalent to ‘not possibly true’ for a possibility predicate to be interdefinable with a necessity predicate. But the latter is (by standard modal logic) equivalent to ‘necessarily not true’, which is not, in general, equivalent to the former statement because of the diverging inner and outer logic.[12] Halbach and Welch do not have a primitive possibility predicate in their language and by axiomatizing their semantics in FDE the introduction of a primitive possibility predicate can be avoided. A further welcome side effect of formulating the modal theory in non-classical logic is that the standard principles of modal operator logic can be transferred to the predicate setting without much trouble. If we were to work in classical logic this would not be possible because of Montague’s theorem. Nonetheless, one can still construct intuitive and “Kripke reducible” modal theories in classical logic, but a lot more care has to be taken in spelling out the modal principles. Roughly, one has to make sure that the modal principles are stated in a way such that any type of semantic ascent or descent is avoided within the modal principle. This can be achieved in stating the modal principles by appeal to a truth predicate in addition to the modal predicate.[13] In fact as a residue of this strategy the non-classical theory of the modal predicate we are about to construct will be developed in a language containing a modal predicate and a truth predicate.

Accordingly, the theory of the modal predicate called “modal theory” will be formulated in the language \(\mathcal{L}_{PATN}\) extending the language of arithmetic \(\mathcal{L}_{PA}\) by two unary predicates; the modal predicate ‘N’ and the truth predicate ‘T’. We add a truth predicate because this allows to establish the connection between the modal theory and its intended semantics. Moreover, adding a truth predicate seems to be desirable independently since principles linking truth and the modal notion can be stated in this way. The theory of truth formulated in the language \(\mathcal{L}_{PAT}^{\Box}\), i.e., a language extending \(\mathcal{L}_{PA}\) by a truth predicate ‘T’ and a unary modal operator ‘☐’, will be called the “operator theory of truth”. In formulating the modal theory and the operator theory of truth we assume some standard coding scheme and denote the code, e.g., the Gödel number, of an expression ζ by #ζ and its name, that is the numeral of #ζ, by \(\ulcorner\zeta\urcorner\). In the remainder of the paper we then freely equate the expressions with their codes in order to keep things as simple as possible. We let the sets \(Sent_{\mathcal{L}}\) (“\(\mathcal{L}\)-sentences”) and \(Cterm_{\mathcal{L}}\) (“\(\mathcal{L}\)-closed terms”) represent themselves and, moreover, drop the subscript when no confusion can arise. In most cases, if \(\rhd\) is a syntactic operation we represent it by \(\underset{\bullet}{\rhd}\). However, there are few exceptions to this rule: we represent the ternary substitution function by x(s/t) where x(s/t) is a name of the formula that results from replacing t by s in x. Also, let Val(·) represent the function that takes codes of closed terms as arguments and provides the code of their denotation as output. Finally, we represent the so-called num function, i.e., the function that takes codes of expressions (#ζ) as input and provides the code of the name of the expression as output (\(\#\ulcorner\zeta\urcorner\)) by a superdot. We thus have \(\dot{\ulcorner\zeta\urcorner}=\ulcorner{\ulcorner\zeta\urcorner}\urcorner\). Sometimes, in case of scope ambiguities, we represent the num function by num^•.

As a matter of fact both the modal theory and the operator theory of truth will be based on the same underlying theory of truth, for otherwise we would arguably fail to reduce the modal predicate to a modal operator and the truth predicate. Instead, from the perspective of the modal theory, the reduction would then show that we may reduce the modal predicate to a modal operator and some other sentential predicate—a sentential predicate that does not share the characteristics of the truth predicate employed in the modal theory. Since Halbach and Welch’s proposal is a generalization of Kripke’s theory of truth to the modal setting, the theory of truth we assume should arguably be a proof-theoretic counterpart of Kripke’s theory of truth and, as we have argued, the theory should be formulated in partial logic.

It turns out that a theory of truth which fits the bill has already been developed by Halbach and Horsten (2006).[14] Their theory of truth “Partial Kripke-Feferman (PKF)” captures Kripke’s construction and is formulated in partial logic. The theory PKF comes in two versions. In Halbach and Horsten (2006), symmetric strong Kleene logic is assumed as the underlying logic, while Halbach (2011: Ch. 16) formulates the theory using FDE, which allows for truth value gaps and gluts. Here we adopt Halbach’s version of the theory PKF. We now introduce the logic of FDE and the aforementioned theory of truth PKF.

3.1. FDE and Partial Kripke-Feferman

We provide a two sided sequent formulation of FDE which is the underlying logic of PKF. In what is to come we denote sequents by ∆ ⇒ Γ with ∆ and Γ being finite (possibly empty) sets of formulas. We sometimes write ∆ ⇔ Γ to convey the sequents ∆ ⇒ Γ and Γ ⇒ ∆.[15] Throughout, the only primitive logical symbols will be ¬, ∧ and ∀. We also take a primitive two place identity predicate = to be part of the language. The existential quantifier ∃, disjunction ∨ and material implication → are defined in the usual way. However, it is important to understand the definitions as mere notational abbreviations.

We now provide the laws and initial sequents of this logic which is basically a variant of the logic presented in Scott (1975).

3.1.1. Structural Rules and Initial Sequents

The structural rules and initial sequents of FDE are the following

3.1.2. Rules and Initial Sequents for the Logical Constants

We provide rules for negation, conjunction, the universal quantifier, and the identity symbol. Note that ¬Γ stands for the set of all negations of sentences in a set Γ.

This completes our presentation of the logic of FDE underlying PKF. Even though this is not strictly speaking part of the syntax of the logic, we indicate the underlying consequence relation in order to avoid misunderstandings and confusion. Let M \(\models_{SK}\) φ[β] denote that φ is true in M under a variable assignment β according to the strong Kleene evaluation scheme we shall define shortly. Then Γ \(\models_{SK}\) ∆ iff for all models M and all variable assignments β:

It is easy to check that the rules and initial sequents of FDE are sound with respect to the consequence relation so defined: if the sequent Γ ⇒ ∆ is FDE-derivable, then Γ \(\models_{SK}\) ∆.

It is important to bear in mind the definition of the consequence relation because several alternative definitions are used within the realm of partial logic and, depending on the consequence relation employed, the rule (¬) may fail to be a sound rule.[16]

The classical rules for negation, that is

are not admissible within the logic of FDE. Yet, FDE will collapse into classical logic for arithmetic φ, i.e., for arithmetic φ the rules (¬RR) and (¬RL) are derivable. As a consequence of this and the rules and initial sequents we are about to give, the arithmetic fragment of PKF will be a supertheory of classical PA.

3.1.3. Rules and Initial Sequents for Arithmetic

Besides the rule of induction we have an initial sequent for every axiom φ of PA:

Finally, we give the principles characterizing the truth predicate which together with the arithmetic sequents and rules constitute the theory Partial Kripke-Feferman PKF.

3.1.4. Partial Kripke-Feferman

The system PKF consists of the rules and initial sequents of arithmetic in the language \(\mathcal{L}_{PAT}\) together with the following truth specific initial sequents:

For a more in depth discussion of the theory PKF we refer the reader to Halbach and Horsten (2006) and Halbach (2011: Ch. 16). However, we note the following facts. First, as we have already mentioned, PKF behaves classically on the arithmetical fragment:

Fact 3.1. For arithmetic φ the rules (¬RR) and (¬RL) are derivable in PKF.

Proof. Cf. Halbach (2011: Ch. 16). The proof uses the fact that in PKF the sequent ⇒ φ, ¬φ is derivable for arithmetical φ.

☐

The second fact we mention highlights some derivability facts.

Fact 3.2. The following sequents are derivable in PKF where \(\phi\in Sent_{\mathcal{L}_{PATN}}\) and λ is some liar sentence such that PAT (PA in the language \(\mathcal{L}_{PAT}\)) proves \(\lambda\Leftrightarrow\neg T\ulcorner\lambda\urcorner\):

Next we construct our modal theory, i.e., the theory of the modal predicate.

3.3. Operator Partial Kripke-Feferman

We now set out the details for operator PKF, that is, PKF formulated in the language \(\mathcal{L}^{\Box}_{PAT}\).[20] The theory will again be formulated in partial logic but as the language now contains a modal operator we also have to specify the logic of this operator. That is, we have to specify the modal logic we employ, which will be a partial modal logic constructed over FDE. However, the rules and sequents of the modal operator are just the standard ones and the partial character of the logic stems solely from its propositional fragment.

3.3.1. Partial Modal Logic

The quantified modal logic QM consists of the rules and initial sequents of FDE together with

Here, (R☐) replaces the more usual rule

In classical logic the latter implies (R☐) due to the rules (¬RR) and (¬RL) but this is no longer the case in partial logic.[21]

If we add a further modal initial sequent X, we call the resulting modal logic QMX. In the remainder we consider the following additional initial sequents:

We call the modal logic that results from addition of (TS), (4S) and (ES) to QM, QM5. As in standard quantified normal modal logic, sequent formulations of what is known as Necessity of Identity (NI) and the Converse Barcan Formula (CBF) are derivable in the modal logic QM.

Fact 3.3. The following are derivable in QM

We now provide the operator theory of truth PKF☐ which is just PKF in the language \(\mathcal{L}^{\Box}_{PAT}\) supplemented by two further initial sequents.

3.3.2. Operator Partial Kripke-Feferman

Operator Partial Kripke-Feferman (PKF☐) is just PKF in the language \(\mathcal{L}^{\Box}_{PAT}\)[22] supplemented by two additional initial sequents:

Let \(\mathcal{S}\) be some modal logic. If some sequent Γ ⇒ ∆ has been derived in PKF☐ using only modal sequents of S then we say that Γ ⇒ ∆ is derivable in PKF☐ assuming the modal logic \(\mathcal{S}\). Importantly, already in QM, PKF☐ proves the rigidity of arithmetic, i.e., of our theory of syntax. For the proof of this fact it is crucial that, at least for arithmetic formulas, (ND) and (BF) can be derived. Indeed, this was the principal reason for adding (ND) and (BF) to QM.

Fact 3.4. For all \(\phi\in\mathcal{L}_{PA}\) the following sequents are derivable in PKF☐ assuming QM

We end the discussion of the modal theory and the operator theory of truth by noting that Fact 3.2 carries over to the extended theories. In particular, the sequent

will be provable for all sentences φ of the language under consideration in the corresponding theory.

Next we show that the modal theories can be interpreted in appropriate operator theories of truth, that is we shall carry out the Kripke reduction for the modal theories we have developed.

4. The Kripke Reduction

We show that MPKF is syntactically reducible to PKF☐ assuming QM5. More precisely, we show that MPKF is interpretable in PKF☐ assuming the underlying modal logic to be QM5 where the modal predicate ‘N’ gets translates as the modified truth predicate ‘☐T’. By inspecting the proof of this result it is also easily seen that BMPKF is interpretable in PKF☐ assuming QM.

However, it is worth discussing in some more detail what we are going to show in this section. In section 2 we have argued that the Kripke reduction, if carried out from a proof-theoretic perspective, should preserve derivability within a theory. But this requirement is slightly ambiguous once one deals with theories formulated in partial logic. In the setting of partial logic, one can distinguish between preservation of theoremhood and what one might call preservation of inferences. Due to the deduction theorem these two notions collapse within classical logic. This is not the case within partial logic and we take it that partial logic is foremost a study of permissible inferences rather than the study of partial tautologies. Consequently, we shall show that Halbach and Welch’s translation does not only preserve derivability but also inferences.

Before we state the details of our proposed reduction, we restate Halbach and Welch’s translation function from \(\mathcal{L}_{PATN}\) to \(\mathcal{L}^{\Box}_{PAT}\)—slightly modified to account for the truth predicate we have added to the language of the modal predicate.

Lemma 4.1 (Halbach and Welch). There is a translation function 𝜌 from formulas of \(\mathcal{L}_{PATN}\) to formulas of \(\mathcal{L}^{\Box}_{PAT}\) with the following properties

Here, the function symbol 𝜌^•(s) represents the primitive recursive function 𝜌 and thus if s is the name of a formula φ, then 𝜌^•(s) will be the name of the formula 𝜌(φ). As an example consider the formula \(N\ulcorner{T\ulcorner{0=0}\urcorner}\urcorner\). By definition of 𝜌, \(\rho(N\ulcorner{T\ulcorner{0=0}\urcorner}\urcorner)=\Box T\rho^{\bullet}(\ulcorner{T\ulcorner{0=0}\urcorner}\urcorner)\) and since \(\rho^{\bullet}(\ulcorner{T\ulcorner{0=0}\urcorner}\urcorner)=\ulcorner{\rho(T\ulcorner{0=0})\urcorner}\urcorner=\urcorner{T\rho^{\bullet}(\ulcorner{0=0})\urcorner}\urcorner\) and \(\rho^{\bullet}(\ulcorner{0=0}\urcorner)=\ulcorner{\rho(0=0)}\urcorner=\ulcorner{0=0}\urcorner\) we get \(\rho(N\ulcorner{T\ulcorner{0=0}\urcorner}\urcorner)=\Box T\ulcorner{T\ulcorner{0=0}\urcorner}\urcorner\).

The reduction or interpretation then amounts to showing that if a formula φ is derivable in MPKF, then so will be the formula 𝜌(φ) in PKF☐ assuming QM5. Before we provide the corresponding theorem we state a lemma that will do the main job in the proof of the theorem.

Lemma 4.2. Let ∆ ⇒ Γ be an initial sequent of MPKF. Then the sequent 𝜌(∆) ⇒ 𝜌(Γ) is derivable in PKF☐ assuming QM5 where 𝜌(A) for some set A is short for {𝜌(φ) : φ ∈ A}.

We only sketch a proof, as the proof basically consists in performing standard derivations within the sequent calculus we have provided. Note, however, that by Theorem 3.4 arithmetic formulas are rigid in PKF☐ assuming QM (and thus QM5). In addition, by formalizing the properties of 𝜌 we may prove in PA

These two facts allow us to deal with the arithmetical conditions appearing in the initial sequents of PKF☐ such as Cterm(x) and Sent(x) in the proof.

Proof sketch. We carry out the proof for the sequents (4′S) and (E′S) in some detail but leave the remaining items to the reader.

(4′S) Using (4S) and (PKF4)(ii) we derive:

Now using \((IA\Box)(i)\) we conclude

By (†1), setting x ≐ 𝜌^•(x), we may derive the 𝜌((4′S)), that is

(E′S) Using the initial sequence (5S) of QM5 we derive (*) \(Sent_{\mathcal{L}_{PAT}^\Box}(x),\neg\Box T\underset{\bullet}{T}\dot{x}\Rightarrow\Box T\underset{\bullet}{\neg}\underset{\bullet}{\Box}\underset{\bullet}{T}\dot{x}\). We may then reason

Now using this together with (†1) and taking x = 𝜌^•(x) we obtain

which is the desired 𝜌((E′S)). The initial sequence of the left branch of the proof tree is an instance of (PKF4)(i). The right branch is (∗), which we shall now prove. The left branch of the proof tree for (∗) starts with an instance of (IA☐)(ii), the right branch uses an instance of (PKF5)(i):

We may now use (ES) to conclude

☐

One last remark is important before we state the main theorem. The modal sequents (TS), (4S) and (ES) of QM5 are only used in the proof of Lemma 4.2 to establish, respectively, the cases (T′S), (4′S) and (E′S). Therefore, the above lemma carries over directly to the initial sequents of BMPKF with respect to PKF☐ assuming QM.

The following theorem establishes that the Kripke reduction can be carried out from a proof-theoretic perspective. That is, using Halbach and Welch’s translation function the theory MPKF can be interpreted in PKF☐ assuming QM5.

Theorem 4.3. Let Γ ⇒ ∆ be a sequent derivable in MPKF. Then the sequent 𝜌(Γ) ⇒ 𝜌(∆) is derivable in PKF☐ assuming the modal logic QM5. Again 𝜌(A) for some set A is short for {𝜌(φ) : φ ∈ A}.

Proof. By induction on the length of a derivation in MPKF we show that if a sequent Γ ⇒ ∆ is derivable in MPKF then so is the sequent 𝜌(Γ) ⇒ 𝜌(∆) in PKF☐ assuming QM5. The start of the induction is immediate by the Lemma 4.2. For the induction step we show that derivability in PKF☐ is preserved if the rule (RN) is applied. Since the remaining rules of BMPKF are also rules of PKF☐ this will end our proof. Now as our induction hypothesis we may assume that \(\rho(T\ulcorner\Gamma\urcorner)\Rightarrow\rho(Tt),\rho(\neg T\ulcorner\Delta\urcorner)\) is derivable in PKF☐. By the properties of 𝜌 this is just \(T\ulcorner\rho(\Gamma)\urcorner\Rightarrow T\rho^\bullet(t),\neg T\ulcorner\rho(\Delta)\urcorner\). But then using the rule (R☐) we may derive the sequent \(\Box T\ulcorner\rho(\Gamma)\urcorner\Rightarrow\Box T\rho^\bullet(t),\neg\Box T\ulcorner\rho(\Delta)\urcorner\), which by the properties of 𝜌 is just \(\rho(N\ulcorner\Gamma\urcorner)\Rightarrow\rho(Nt),\rho(\neg N\ulcorner\Delta\urcorner)\).

☐

The theorem establishes that inferences of MPKF are preserved in PKF☐ assuming QM5 modulo translation. This immediately implies that theoremhood is also preserved modulo translation. We may state this simpler claim as corollary of Theorem 4.3 by writing \(\Sigma\vdash\phi\) (\(\Sigma\vdash_{\mathcal{S}}\phi\)) if the sequent ⇒ φ is derivable in a theory Σ (assuming the modal logic \(\mathcal{S}\)).

Corollary 4.4. For all \(\phi\in\mathcal{L}_{PATN}\)

The corollary and the foregoing theorem establish that MPKF is “Kripke-reducible” to PKF☐ assuming QM5. In other words the modal predicate of MPKF can be understood as a modified truth predicate as suggested by Kripke. It remains to substantiate our claim that our Kripke reduction can be viewed as the proof-theoretic counterpart to the semantic reduction by Halbach and Welch.

5. Modal Fixed-Point Semantics

We now give the semantics for \(\mathcal{L}_{PATN}\) and \(\mathcal{L}_{PAT}^{\Box}\), which are slight variants of the semantics introduced by Halbach and Welch. Both semantics combine the strategy employed by Kripke (1975) in formulating his theory of truth with ideas from possible world semantics for modal operator logic. The two semantics have the same structure, are both based on the strong Kleene scheme and only diverge in their respective clause for the modal notion. The key concepts of the two semantics are the notions of a frame and of an evaluation function, a function that assigns to each possible world a subset of ω—the interpretation of the truth predicate.

Definition 5.1 (Frame, evaluation function). Let W ≠ ∅ be a set of natural number structures and R ⊆ W × W a dyadic relation on W. Then F = 〈W, R〉 is called a frame. A function f : W → P(ω) is called an evaluation function for a frame F. The set of all evaluation functions of a frame F is denoted by Val_F.

Worlds have a two-fold role to play in the present framework. Firstly, they serve as parameters in the definition of the notion of “truth in a model” but secondly, they already provide the interpretation of the arithmetical vocabulary. The frame and the evaluation function are then employed to provide an interpretation of the semantic vocabulary, i.e., the truth predicate and the modal notion.

The previous remarks should become clearer by the definition of a model for \(\mathcal{L}_{PATN}\) induced by a frame and an evaluation function at a world w. We shall not explicitly mention the antiextension of the truth predicate in our presentation of the models since it can be taken to consist of the negations of the sentences in the truth predicate’s extension. However, we need to explicitly provide the antiextension of the necessity predicate.

Definition 5.2 (Models for \(\mathcal{L}_{PATN}\)). Let F be a frame, f an evaluation function and \(\overline{f(w)}\) the set \(\{\#\neg\phi:\#\phi\in f(w)\}\) for arbitrary w. Furthermore, set

with [wR] being an abbreviation for {v ∈ W : wRv}. Then \(M_{w}=\left\langle w, f(w),Y^{+}_{w},Y^{-}_{w}\right\rangle\), where w ∈ W is a natural number structure, f(w) is the extension of the truth predicate and \(Y^{+}_{w}\)(\(Y^{-}_{w}\)) the (anti-)extension of the necessity predicate, is a model of the language \(\mathcal{L}_{PATN}\) induced by F and f at a world w.[23] If it is important to keep track of the frame and the evaluation function, we write F, \(w\models_{SK}^{f}\phi\) instead of \(M_{w}\models_{SK}\phi\).

The necessity predicate is thus interpreted as truth in all accessible worlds, but where the relevant notion of truth is not the metalinguistic notion but the notion of truth of \(\mathcal{L}_{PATN}\) itself. As a consequence the antiextension of the necessity predicate consists of those sentences whose negation is true in at least one accessible world. We now specify the notion of truth in a model M at a world w according to the modal strong Kleene scheme.

Definition 5.3 (Modal Strong Kleene Truth in a Model). Let F be a frame and f an evaluation function f . We define the notion of truth in a model induced by the frame F and the evaluation function f at a world w according to the strong Kleene scheme, \(\models_{SK}\) by

t^N is the interpretation of a term t in the standard model and \(\overline{Sent_{\mathcal{L}_{PAT}}}\) denotes the set of natural numbers that are not codes of sentences under the coding scheme assumed. We say a formula φ is true in the model induced by the frame F and the evaluation function f, \((F,f)\models_{SK}\phi\), iff \(\forall w(F,w\models^{f}_{SK}\phi)\).

The semantics for the language \(\mathcal{L}_{PAT}^{\Box}\) differs from the semantics we have just presented in the way the modal notion is interpreted. Since we are now dealing with an operator instead of a predicate, the interpretation is no longer given by an extension and antiextension but by the standard clause known from possible world semantics.

Definition 5.4 (Models for \(\mathcal{L}_{PAT}^{\Box}\)). Let F be a frame and f ∈ Val_F an evaluation function on F. Then the tuple (F, f ) is called a model of \(\mathcal{L}_{PAT}^{\Box}\).

Definition 5.5 (Operator Strong Kleene Truth in a Model). Let F be a frame and f an evaluation function. The truth of a formula φ of \(\mathcal{L}_{PAT}^{\Box}\) in the model (F, f ) at a world w according to operator strong Kleene truth, F, \(w\models^f_{SK\Box}\phi\), is defined by clauses (i)-(iv) and (vii)-(xi) of Definition 5.3 but where the clauses (v) and (vi) of Definition 5.3 are replaced by

We say that φ is true in the model (F, f), (F, f) \(\models_{SK\Box}\) φ, iff for all w ∈ W(F, w \(\models^f_{SK\Box}\) φ).

Following the outlines of Halbach and Welch we next define operations on evaluation functions called the modal strong Kleene jump and the operator strong Kleene jump.

Definition 5.6 (Modal and Operator Strong Kleene Jump). Let F be a frame and Val_F the set of evaluation functions of F. The modal strong Kleene jump (operator strong Kleene jump) \(\Theta_{F}\) (\(\Theta^{\Box}_{F}\)) is an operation on Val_F relative to F such that for all w ∈ W

Importantly, the modal and the operator strong Kleene jump will be monotone operations with respect to an ordering ≤:

Lemma 5.7 (Monotonicity). Let F be a frame. The jump \(\Theta_{F}\) (\(\Theta^{\Box}_{F}\)) is a monotone operation on Val_F, i.e. for all f,g ∈ Val_F:

where f ≤ g :⇔ ∀w ∈ W( f (w) ⊆ g(w)).

Proof. Clearly for all evaluation functions f, g with f (w) ≤ g(w) for all w ∈ W we have [ΘF(f)](w) ⊆ [ΘF(g)](w) and thus ΘF(f) ≤ ΘF(g). Similarly for \(\Theta^{\Box}_{F}\).

☐

The monotonicity of ΘF implies, assuming standard set theory, the existence of fixed points, i.e., the existence of evaluation functions f, g ∈ ValF such that

As we shall show in the next section, exactly these fixed points induce models for BMPKF and PKF☐ assuming the underlying modal logic to be QM.

6. The Adequacy of MPKF and PKF☐ relative to Modal Fixed-Point Semantics

In this section we show that the two theories we have constructed are intimately related to the corresponding modal fixed-point semantics. However, we should warn the reader that we do not attempt to connect the notion of truth in modal fixed-point semantics with the notion of derivability in MPKF or PKF☐, as one might expect if one thinks of adequacy as entailing the completeness of some proof system. Such a result is excluded by the fact that in modal fixed-point semantics the standard model of arithmetic is assumed to be the base model at every world. Thus every true arithmetical sentence will be true in modal fixed-point semantics but of course not all of them can be proved in the modal theories because of Gödel’s incompleteness theorem.[24]

Rather, our notion of adequacy connects the models of our theories to the models of modal fixed-point semantics. It asserts that the fixed-point models that we obtain relative to so-called equivalence frames are exactly the models of MPKF and PKF☐ assuming QM5 respectively.[25] Thus only the fixed-points of the modal and the operator Kripke jump respectively give rise to models of MPKF and PKF☐ assuming QM5 respectively. Philosophically speaking, one might take such a result to establish that fixed-point models are precisely the intended models of the theories. Moreover, this adequacy result also has the nice consequence that the notion of truth in modal fixed-point semantics corresponds to the object-linguistic notion of truth as characterized by MPKF and PKF☐ respectively—the theories we have developed force these two notions to correspond. By this we mean that if we can prove \(T\ulcorner\phi\urcorner\) for some sentence φ in MPKF (PKF☐ assuming QM5) then φ will be true in each SK (SK☐) fixed-point model at every world.[26]

Before we provide the relevant results to this effect, we introduce some auxiliary terminology. Le Σ be some theory. We write F, \(w\models^{f}_{\gamma}\Sigma\) for γ ∈ {SK, SK☐} iff for all Σ derivable sequents Γ ⇒ ∆ and variable assignments β:

• if F, \(w\models^{f}_{\gamma}\phi[\beta]\) for all φ ∈ Γ, then there exists a ψ ∈ Δ such that F, \(w\models^{f}_{\gamma}\psi[\beta]\)
• if F, \(w\models^{f}_{\gamma}\neg\psi[\beta]\) for all ψ ∈ Δ, then there exists a φ ∈ Γ such that F, \(w\models^{f}_{\gamma}\neg\phi[\beta]\)

We assume β to be constant across worlds and assume the SK-satisfaction relation to be defined in the expected way. Finally, let \(\mathcal{S}\) be some modal logic. We take PKF\(\Box_{\mathcal{S}}\) to be the set of all PKF☐ derivable sequents assuming the modal logic \(\mathcal{S}\).

We state the key result, which establishes that the fixed-point models we obtain relative to arbitrary frames are exactly the models of BMPKF and PKF☐ respectively.

Theorem 6.1. Let F be a frame and f ∈ Val_F an evaluation function. Then

Proof. For the left-to-right direction we need to show that every BMPKF (PKF☐ assuming QM) derivable sequent preserves truth in the respective fixed-point models. The proof is a routine induction on the length of a proof and is left to the reader. For the converse direction we assume the right-hand-side. It then suffices to show for an arbitrary world w that (i) [ΘF( f )](w) = f (w) and (ii) \([\Theta_{F}(f)](w)=f(w)\). (PKF6) tells us that there will be only sentences in the extension of the truth predicate.[27] We may thus establish our claim by an induction on the positive complexity of the members of (i) [ΘF( f )](w) and (ii) \([\Theta^{\Box}_{F}(f)](w)=f(w)\). The proof is routine and for both (i) and (ii) we only check one of the modal cases for sake of illustration.

• (i) We discuss the case where φ \(\doteq\)Nt. The reader may check the remaining cases.
  
• (ii) We discuss the case φ \(\doteq\) ☐ψ and assume that the induction hypothesis holds for ψ. The remaining cases are again left to the reader.
  

☐

Theorem 6.1 tells us that the standard models of BMPKF and PKF☐ (assuming QM) are generated exactly by the fixed-points of the modal and the operator strong Kleene jump relative to arbitrary frames. More importantly, we may obtain similar adequacy results for the theory MPKF and (unsurprisingly) for PKF☐ assuming alternative modal logics if we restrict our attention to classes of modal frames which meet certain properties.

Definition 6.2. Let F be a frame and Σ some theory. If for all evaluation functions f with \(\Theta_{F}(f)=f\) (\(\Theta_{F}^{\Box}(f)=f\)) and \(\forall w(F,w)\models^f_{SK}\Sigma\) (\(\forall w((F,w)\models^f_{SK\Box}\Sigma\)), we write \(F\models_{SK}\Sigma\) (\(F\models_{SK\Box}\Sigma\)).

Theorem 6.3. Let F = 〈W,R〉 be a frame. Then

Proof sketch. The left-to-right direction works as in possible world semantics for modal operator logic. For the converse direction we consider case (i) and assume ¬wRw. Moreover, let τ be the truth teller.[28] We observe that there is a fixed point, that is, an evaluation function f, such that τ ∉ f(w) but τ ∈ f(v) for all v with wRv. Therefore, we have F, \(w\models_{SK}^{f}N\ulcorner\tau\urcorner\) but \(F,w\not\models^{f}_{SK} T\ulcorner\tau\urcorner\) which contradicts the sequent (T′S). Similarly for the remaining items.

☐

Corollary 6.4. Let F = 〈W,R〉 be a frame. Then

Similarly, as a consequence of well-known facts about possible world semantics for modal operator logic we get the parallel results for our modalized theory of truth. We only mention the adequacy result for PKF☐ when the modal logic QM5 is assumed.

Theorem 6.5. Let F = 〈W,R〉 be a frame. Then

A final trivial corollary of the adequacy results we have put forward is the consistency of all the theories we have constructed. Again we only explicitly mention two consistency results as the remaining consistency results are immediately implied by those mentioned.

Corollary 6.6. MPKF and PKF☐ assuming QM5 are consistent.

This concludes the investigation of the relation between the modal theories and modal fixed-point semantics. We have shown that the fixed-points of the two jump operations are exactly the evaluation functions that give rise to models of the respective theories, if frames with the suitable property are assumed. This shows that there is, to say the least, a close connection between the theories we introduced and modal fixed-point semantics, as laid out by Halbach and Welch. Due to this close tie between the theories and the semantics employed in Halbach and Welch’s reduction, the proof-theoretic version of the reduction we have carried out may rightly be considered as a proof-theoretic counterpart to Halbach and Welch’s work.[29]

7. Conclusion

Summing up, we have constructed modal theories and operator truth theories formulated in the logic of FDE. We showed that the modal theories were “Kripke-reducible” to the operator truth theories, that is, the modal theory can be interpreted in the operator truth theory if we assume an appropriate modal logic where the modal predicate is translated as the truth predicate modified by the modal operator. Finally, we showed that the theories we constructed match the semantics Halbach and Welch used to carry out their semantic Kripke reduction. We take this to establish that the semantic reduction of Halbach and Welch has a natural proof-theoretic counterpart. Moreover, the family of theories we constructed is rather flexible with respect to the modal properties assumed, which in turn suggests that a reducible modal theory will be found for almost any set of modal properties one wishes to adopt. The critical reader might draw attention to the fact that we have not allowed for contingent vocabulary in our language and have thereby failed to provide a philosophically interesting study of modality. However, in this context nothing but further complication would arise if we had allowed contingent vocabulary in our language. All the results we have provided carry over with minor modification when contingent vocabulary is introduced into the picture and the absence of contingent vocabulary should therefore not count against our proposal.[30]

Let us now turn to the philosophical evaluation of our work. To start with we consider the view that understands the Kripke reduction along the lines of Halbach and Welch, that is, as an argument in favor of the operator approach. According to this view, we have argued, the proponent of the predicate approach will be under considerable pressure to revise his treatment of modal notions in favor of an operator treatment of modality. The idea is that it no longer suffices to reject possible worlds because the syntactic reduction we have carried out shows that conceiving of the modal predicate as a truth predicate modified by a modal operator is equally warranted from a proof-theoretic perspective. The proponent of the predicate approach might reply that the modal theories we have constructed do not capture the kind of modal predicate she has in mind and that, indeed, the success of the Kripke reduction is nothing but a case in point. We are more than happy to concede this if the proponent of the predicate approach were to provide such an alternative modal theory, which fails to be Kripke reducible. However, so far, very little progress in direction of developing such a theory has been made and the proponent of the operator approach has every right to be skeptical as to whether a philosophically attractive theory of this kind is forthcoming. So while our proof-theoretic addition to Halbach and Welch’s reduction might not seal the case for operator approaches, it forces the proponent of the predicate approach to put his own non-reducible theory of modality on the table.

There is a further, more subtle argument the proponent of the predicate approach may bring forward in her defense, which highlights a slight asymmetry between Halbach and Welch’s semantic reduction and our proof-theoretic counterpart: while in the semantic case the converse direction of the reduction holds as well, this need not be true in the proof-theoretic case. Indeed, to date we don’t know whether a formula is derivable in MPKF if its translation is derivable in PKF☐ assuming QM5. In other words we don’t know whether 𝜌 faithfully interprets MPKF in PKF☐ assuming QM5. Now, assuming that there was a sentence for which this implication would fail the proponent of the predicate approach could argue that one of the advantages of the predicate approach was precisely that it refrained from asserting this particular sentence.[31] While this is certainly a coherent position it does not strike us as a very plausible one. First, it hinges on the fact that the converse direction of the syntactic reduction does not hold, which is highly speculative, as we don’t see a principle reason why MPKF should not be faithfully interpretable in PKF☐ assuming QM5. But let us assume for sake of the argument that MPKF cannot be faithfully interpreted in PKF☐ assuming QM5. Still it seems to us that simply because there is no principled reason speaking against the converse direction in the case of MPKF, it is unlikely that an alternative theory, which can be faithfully interpreted in PKF☐ assuming QM5, will be very different in character to MPKF.[32]

The question then arises why the proponent of the predicate approach is inclined to accept MPKF as a philosophically attractive theory of modality, while the alternative theory fails to be attractive on principled grounds. We don’t see how this question can be answered in a plausible and satisfactory way. Nonetheless, a result establishing the converse direction of the proposed reduction is clearly desirable.

In sum, it seems that if we follow the dialectics of Halbach and Welch and view the expressive strength of the predicate approach as the sole argument in favor of conceiving of modalities as predicates, then the syntactic and semantic Kripke reduction taken together make a strong case in favor of the operator approach. However, already in the introduction of this paper we have pointed toward further reasons why the predicate approach may be preferable and, presumably, the proponent of the predicate approach will have further such reasons for her preferred approach, other than its expressive strength. On this reading the Kripke reduction serves as an argument in favor of predicate approaches to modality because it shows that we can develop workable and philosophically adequate approaches to modality. Viewed in this way Halbach and Welch’s work shows how to obtain an attractive semantic theory of modal predicates, whereas our work establishes this point from a proof-theoretic perspective and, in addition, shows that the axiomatic and the semantic theory fit nicely together. Indeed this interpretation of the Kripke reduction seems to be more in line with Kripke (1975) himself who viewed his proposal as a vindication of predicate approaches to modality against the backdrop of liar-like paradoxes that threaten these approaches. Kripke writes:

Now, this is essentially what happens in Halbach and Welch’s semantics for the language of the modal predicate and, by the same token, by introducing the theory MPKF we have shown that the ladder can be also kicked away from a proof-theoretic perspective. Moving on from there the proponent of the predicate approach could even try to provide theories of modality in which the modal predicate can no longer be viewed as a modified truth predicate.

Acknowledgments

This paper was presented at “The Truth to Be Told Again”-conference in Amsterdam and the “Truth and Paradox”-workshop in Munich. I wish to thank the audiences of both venues for helpful comments. I would also like to thank Catrin Campbell-Moore and Martin Fischer for detailed comments on versions of this paper. Finally, I thank two anonymous referees of this journal for their very helpful comments and for catching some mistakes of mine.

My research was funded by the DFG project “Syntactical Treatments of Interacting Modalities” and the Alexander von Humboldt Foundation.

References

• Dunn, J. Michael (1995). Positive Modal Logic. Studia Logica, 55(2), 301-317. http://dx.doi.org/10.1007/BF01061239
• Feferman, Saul (2000). Does Reductive Proof Theory Have a Viable Rationale? Erkenntnis, 53(2), 63-96. http://dx.doi.org/10.1023/A:1005622403850
• Field, Hartry (2008). Saving Truth from Paradox. Oxford University Press. http://dx.doi.org/10.1093/acprof:oso/9780199230747.001.0001
• Fischer, Martin, Volker Halbach, Jönne Kriener, and Johannes Stern (2015). Axiomatizing Semantic Theories of Truth? The Review of Symbolic Logic, 8(2), 257-278. doi: 10.1017/ S1755020314000379
• Halbach, Volker (2011). Axiomatic Theories of Truth. Cambridge University Press. http://dx.doi.org/10.1017/CBO9780511921049
• Halbach, Volker, and Leon Horsten (2006). Axiomatizing Kripke’s Theory of Truth. The Journal of Symbolic Logic, 71(2), 677-712. http://dx.doi.org/10.2178/jsl/1146620166
• Halbach, Volker, and Philip Welch (2009). Necessities and Necessary Truths: A Prolegomenon to the Use of Modal Logic in the Analysis of Intensional Notions. Mind, 118(469), 71-100. http://dx.doi.org/10.1093/mind/fzn030
• Jaspars, Jan, and Elias Thijsse (1996). Fundamentals of Partial Modal Logic. In Patrick Doherty (Ed.), Partiality, Modality and Nonmonotonicity (111-141). CSLI Publications.
• Koellner, Peter (2015). Gödel’s Disjunction. In Leon Horsten and Philip Welch (Eds.), The Scope and Limits of Arithmetical Knowledge. (forthcoming)
• Kremer, Michael (1988). Kripke and the Logic of Truth. Journal of Philosophical Logic, 17(3), 225-278. http://dx.doi.org/10.1007/BF00247954
• Kripke, Saul (1975). Outline of a Theory of Truth. The Journal of Philosophy, 72(19), 690-716. http://dx.doi.org/10.2307/2024634
• Montague, Richard (1963). Syntactical Treatments of Modality, with Corollaries on Reflexion Principles and Finite Axiomatizability. Acta Philosophica Fennica, 16, 153-167.
• Niebergall, Karl-Georg (2000). On the Logic of Reducibility: Axioms and Examples. Erkenntnis, 53(2), 27-61.
• Scott, Dana (1975). Combinators and Classes. In C. Böhm (Ed.), λ-Calculus and Computer Science (1-26). Springer. http://dx.doi.org/10.1007/BFb0029517
• Stern, Johannes (2014a). Modality and Axiomatic Theories of Truth I: Friedman-Sheard. The Review of Symbolic Logic, 7(2), 273-298. http://dx.doi.org/10.1017/S1755020314000057
• Stern, Johannes (2014b). Modality and Axiomatic Theories of Truth II: Kripke-Feferman. The Review of Symbolic Logic, 7(2), 299–318. http://dx.doi.org/10.1017/S1755020314000069
• Stern, Johannes (2014c). Montague’s Theorem and Modal Logic. Erkenntnis, 79(3), 551-570. http://dx.doi.org/10.1007/s10670-013-9523-7
• Tarski, Alfred, Andrzej Mostowski, and Raphael Robinson (1953). Undecidable Theories. North-Holland Publications.

Notes

1. See Montague (1963) for a statement and proof of Montague’s theorem and Stern (2014c) for a discussion of Montague’s result.

2. One might argue that while the proponent of the predicate approach need not accept possible world semantics as her preferred semantics she should be happy to accept possible worlds for instrumental reasons. We think the proponent of the predicate approach has every reason to resist this kind of argument because at least prima facie it is unclear whether the modal theory she has in mind will be sound with respect to possible world semantics.

3. I would like to thank an anonymous referee for stressing this point.

4. In particular, we think one should not criticize the reduction by blaming the translation function to be unprincipled or counterintuitive. This also holds for our syntactic reduction since we use the same translation function as Halbach and Welch.

5. See Niebergall (2000) and Feferman (2000) for a discussion of concepts of reducibility.

6. However, there is one decisive difference between (SR) and (PR). In the case of (SR) the converse direction of the implication will hold as well. In other words the translation is faithful in this case. This might not be so in the case of (PR). Indeed to date we do not know whether this holds for the syntactic reduction we propose. We shall come back to this issue in the conclusion of the paper.

7. One might rightly point out that while standard first-order semantics is an apt semantics for the language of the modal predicate it does not tell us which subsets of the domain of the model are apt interpretations of the modal predicate.

8. Stern (2014a) develops a general strategy for developing modal theories that can be understood in this way.

9. As a matter of fact the evaluation scheme is not only partial but also paraconsistent. In this paper we use the word “partial” carelessly to stand for both.

10. See Halbach and Horsten (2006) for further arguments in favor of axiomatizing Kripke’s theory of truth in partial logic.

11. See Halbach (2011) for a discussion of classical axiomatizations of Kripke’s theory of truth.

12. See Stern (2014b) for a discussion of this problem and a classical modal theory with a primitive possibility predicate. The Kripke reduction can still be carried out for this theory despite these pathologies.

13. See Stern (2014a) for a presentation and discussion of the strategy. This strategy has been independently applied by Koellner (2015).

14. See also Kremer (1988) for a related “logic of truth”.

15. We also use the symbols ⇒ and ⇔ to convey the notions of metalinguistic or semantic implication and equivalence. But the intended use of these symbols should be clear from context.

16. It is very plausible that the reduction we are attempting could be carried out if alternative partial logic were adopted. In particular, most of what we say should also hold modulo some necessary modifications of calculus and semantics for the logics S3, LP and K3.

17. This also means that the concepts of syntax such as ‘Sent’ should now be read as of concepts of syntax \(\mathcal{L}_{PATN}\). That is, Sent(x) should now be read as \(Sent_{\mathcal{L}_{PATN}}(x)\).

18. As a matter of fact most of the initial sequents can be omitted. As far as we can see, only (N1), (N3), (N7)(i) and (RN) are required. However, a proof of this fact is rather lengthy and complicated and would take us too far afield. In a nutshell one first has to prove \(\phi(x_1,\ldots,x_n)\Rightarrow N\ulcorner{\phi(\dot{x}_1,\ldots,\dot{x}_n)}\urcorner\) for arithmetic φ. Then one can derive the redundant initial sequents using the axioms of PKF and the rule (RN).

19. BMPKF proves to be quite important for establishing the link between the modal theories and the semantics we shall discuss shortly.

20. Notice in contrast to the operator language provided by Halbach and Welch our formation rules are standard. In particular, we allow for the application of the modal operator to open formulas.

21. If we were to attempt the Kripke reduction for theories that are based on some non-symmetric logic such as K3 or LP, then we would also need to assume the rule

    

    In FDE the rule can be derived from (R☐) using the rule (¬). See Jaspars and Thijsse (1996) and Dunn (1995) for more on partial modal logics.

22. Again the concepts of syntax appearing in the initial sequences are now thought of as concepts of the language \(\mathcal{L}^{\Box}_{PAT}\)

23. Here ⋂ and ⋃ are taken to be operations on P(ω).

24. Even if we would allow for alternative base models it is unlikely that we would obtain an interesting “completeness” result. See Fischer, Halbach, Kriener, and Stern (2015) for a discussion of these and related issues.

25. In the terminology of Fischer et al. (2015) our adequacy result shows that MPKF and PKF☐ are N-categorical theories relative to equivalence frames.

26. Similarly, if the theory proves \(N\ulcorner\phi\urcorner\) then φ will be true in the model in all the worlds accessible from some world.

27. Note that, as we are working within the standard model, we only need to deal with standard sentences.

28. That is a sentence τ for which we can prove \(T\ulcorner\tau\urcorner\Leftrightarrow\tau\) using only the logical and arithmetical initial sequents of PKF in the language \(\mathcal{L}_{PAT}\).

29. The skeptic may argue that we have failed to axiomatize Halbach and Welch’s semantics for their proposal is based on the least fixed point whereas we allow for arbitrary fixed points. Yet, if we allow for the least fixed point only, no axiomatization of the semantics in the sense of Theorem 6.1 is forthcoming due to complexity issues. See again Fischer et al. (2015) for a discussion of these issues.

    Also even though the reduction of Halbach and Welch is carried out assuming the least fixed point we do not think that this is actually of crucial importance: the reduction will go through for arbitrary fixed points as long as we make some suitable specification and adjustments to the construction.

30. See Stern (2014a) for hints on how to integrate contingent vocabulary.

31. I thank an anonymous referee for raising this worry. I also owe the formulation of the worry to this referee. It is also worth noting how a proponent of the predicate approach should not argue: she should not argue that we have failed to provide an attractive theory of modality because the modal theory is not faithfully interpretable in the operator truth theory. She should not argue in this way since by doing so she would accept the understanding of the modal predicate as the modified truth predicate of PKF☐ and thus implicitly accept the reducibility claim.

32. The set of sentence in the range of 𝜌, which are provable in PKF☐ assuming QM5 is recursively enumerable. Therefore there will be an axiomatizable modal theory that is faithfully interpretable in PKF☐ assuming QM5.