Internalizing Case-Relative Truth in CIFOL$+$

Abstract

CIFOL is defined in Belnap and Müller 2013 (J Phil Logic 2013) as the first-order fragment of Aldo Bressan’s higher-order modal typed calculus $MC^\nu$. Bressan based his calculus on Carnap’s “method of extension and intension”: In CIFOL, truth is relative to “cases,” where cases play the formal role of “worlds” (but with less pretension). CIFOL$+$ results by following Bressan in adding term-constants t for the true and f for the false, and a single predicate constant, $P_0$, which together with a couple of simple axioms enable the representation of “sentence $\Phi$ is true in case $x$” by means of a defined expression, $T(\Phi , x)$, where $\Phi$ is the sentence of CIFOL$+$ in question and where $x$ ranges over a defined family of “elementary cases.” (Whereas being a case is defined in the semantic metalanguage, elementary cases are squarely in the (first order) domain of CIFOL$+$.) A suitable suite of axioms guarantees that one can prove (in CIFOL$+$) that there is exactly one elementary case, $x$, such that $x$ happens (i.e., such that $x=\mathbf t$), a fact that underlies the equivalence of $\square (x=\mathbf t \rightarrow \Phi )$ and $\lozenge (x=\mathbf t \,\,\wedge \,\,\Phi )$. (Proofs are surprisingly intricate for first order modal logic.) One can then go on to show that $T(\Phi , x)$ is well-behaved in terms of its relation to the connectives of CIFOL$+$, a result required for ensuring that $T(\Phi , x)$ is properly read as “that $\Phi$ is true in elementary case $x$.”

1 Introduction

Belnap and Müller 2013 (BM2013) defined and discussed the first-order fragment, CIFOL,¹ of Aldo Bressan’s splendid but little-known higher-order modal typed calculus $MC^\nu$ (Bressan 1972).² Since higher-order type theories are intrinsically powerful, it is perhaps not surprising that $MC^\nu$ contains a truth concept for itself. CIFOL by design is “case-intensional,” meaning that the basic truth concept is “true in a case,” which plays the same role as “true according to a world” or the like plays in the most common quantified modal logics. One might not expect, however, that a certain modest first-order extension of CIFOL, which we will call CIFOL$+$, can contain a powerful kind of truth concept for itself. It is this surprising result, which is based on Bressan 1972, that we present here. (The proof is the most intricate of any of which we know of a theorem in—rather than a theorem about—quantified modal logic.) We say a little about CIFOL in this introductory section, but by and large we presuppose acquaintance with BM2013.

1.1 Grammar and Semantics

Grammatically, CIFOL is the first order quantified modal logic with identity detailed in BM2013. (CIFOL$+$ results from adding two more axioms to CIFOL, as we see in Sects. 1.4 and 2.1.) Its proof theory is largely—but not entirely—a simple combination of S5 with first order predicate calculus with identity (with predication intensional, but with replacement of identicals restricted to extensional contexts), conservatively extended by both definite descriptions, ${{\iota }}x\Phi$, and lambda abstracts, $\lambda x\Phi$, governed by transparent principles.³ (This chapter uses both the ${{\iota }}$ and the $\lambda$ of CIFOL, but we also use $\lambda$ metalinguistically.) It is the semantics of CIFOL that sets it apart. CIFOL is a “case-intensional” logic, meaning the following. There is a set of cases, $\Gamma$, which is formally like a set of “worlds” in the jargon of much contemporary modal logic. Following Carnap (1947), each expression, ${\xi }$, of each type, be it individual expression $\alpha$ (whether constant $c$, variable $x$, or complex, predicate constant $P$, operator constant $f$, or sentence ${\Phi }$) has an extension in each case, $\gamma \in \Gamma$, written $ext_\gamma (\xi )$; in particular, truth of sentences is case-relative. Furthermore, each expression, $\xi$, has an intension, written $int(\xi )$, which is not something extra, but is explicable as the pattern of its extensions $ext_\gamma (\xi )$, as $\gamma$ varies over $\Gamma$.

Fact 1

(Intension-extension connection) Using lambda-abstraction, we may say, where $\gamma$ ranges over the set of cases, $\Gamma$, that $int(\xi )=\lambda \gamma (ext_\gamma (\xi ))$, and that $ext_\gamma (\xi )= (int(\xi ))(\gamma )$.

There is an “individual domain,” $D$, which harbors all the possible extensions of singular terms, $\alpha$, and there is a parallel “sentential domain,” ${\mathbf {2}} = \{{\mathbf {T}}, {\mathbf {F}}\}$, containing the standard truth values to serve as the extensions of sentences. Where $X \mapsto Y$ is the set of functions from $X$ into $Y$, an intension is always a function in $(\Gamma \mapsto Y)$, for appropriate $Y$. A CIFOL interpretation, ${\mathcal {I}}$, endows each atomic expression with an intension of the appropriate type.⁴ Then recursive clauses come along to guarantee that singular terms $\alpha$, sentences $\Phi$, operators $f$, and predicates $P$ each have the right type of extension and intension. Along with sentences and singular terms, we illustrate only one-place operators and predicates.

Fact 2

(Types of intensions and extensions)

• $ext_\gamma (\alpha ) \in D$.

• $int(\alpha )\in (\Gamma \mapsto D)$.

• $ext_\gamma (\Phi ) \in {\mathbf {2}}$.

• $int(\Phi )\in (\Gamma \mapsto {\mathbf {2}}).$

• $ext_\gamma (P) \in ((\Gamma \mapsto D)\mapsto {\mathbf {2}}).$

• $int(P) = {\mathcal {I}}(P) \in (\Gamma \mapsto ((\Gamma \mapsto D)\mapsto {\mathbf {2}})).$

• $ext_\gamma (f) \in ((\Gamma \mapsto D)\mapsto D).$

• $int(f) = {\mathcal {I}}(f) \in (\Gamma \mapsto ((\Gamma \mapsto D)\mapsto D)).$

Identity is an important special case: Unlike predication, its semantics is extensional, so that the truth value of $\alpha = \beta$ in $\gamma$ depends only on the extensions in case ${\gamma }$ of ${\alpha }$ and of ${\beta }$.

CIFOL invokes ${\delta }$ as an assignment of intensional values (that is, values in ${\Gamma }\,\mapsto$ D) to the individual variables, so that free individual variables and individual constants have exactly the same semantics. Then BM2013 explains a CIFOL “model” as a triple ${\mathcal {M}}= \langle \Gamma , D, {\mathcal {I}}\rangle$.⁵ There is a special constant, $*$, whose case-relative extensions in $D$ are also called $*$. In Frege’s way, $*$ helps process definite descriptions that do not satisfy the standard unique-existence clause. It is assumed that D contains something other than $*$. Among modal logics, the hallmark of CIFOL is that truth of sentences is defined relative to “cases,” which are a common generalization of worlds, times, and so on. When ${\mathcal {M}}$ is understood, the fundamental semantic (metalinguistic) truth-locution has the form “$\Phi$ is true in case $\gamma \in \Gamma$,” with $\Phi$ denoting a sentence, and corresponding to the more familiar phrase, “$\Phi$ is true in world w.” We sometimes use $\gamma \models \Phi$ to say that ${\Phi }$ is true in case $\gamma$. For example, with reference to a certain model, ${\mathcal {M}}$, the semantic clause for necessity proclaims that $\gamma \models \square \Phi$ just in case $\gamma '\models \Phi$ for all $\gamma '\in \Gamma$.

1.2 Finding “True in a Case” in CIFOL$+$

What we seek is a sentence of CIFOL itself which can reasonably be read in English as “that ${\Phi }$ is true in case x,” with $\Phi$ taking the place of (rather than denoting) a sentence; CIFOL is not, however, adequate in this respect. We repair the inadequacy in four steps. (1) We enrich CIFOL with two new axioms, labeling the result “CIFOL$+$.” (2) We take $\Phi$ as being rather than denoting a CIFOL$+$ sentence, and we take x as an individual variable that one can interpret as ranging over an “internal” representation of the set, ${\Gamma }$, of all the cases in a certain model ${\mathcal {M}}$. (3) We formulate within CIFOL$+$ an “internal” concept of cases, which intuitively are in one-one correspondence with the set ${\Gamma }$ of “external” cases. Theorem 1 testifies that we have succeeded in this endeavor. Finally, (4) we define within CIFOL$+$ a rich (but paradox-free) concept of truth via a locution having the force of “that ${\Phi }$ is true in case $x$.”⁶

1.3 Paths not Taken

We pause to contrast our path with nearby paths that we do not take. We are after defining what Curry calls a “mixed nector,” the English “that $\Phi$ is true in case $x$,” to be written $T(\Phi ,x)$, where the character $\Phi$ takes the place of a sentence and where x takes the place of an individual variable ranging over internal cases. The comparable Tarskian goal would be to define a locution having the form, “$s$ is true in case $x$,” written $T(s, x)$, where $s$ denotes a sentence and $T$ is a genuine predicate. (So $s$ denotes a sentence, whereas $\Phi$ is a sentence.) Consider the non-case-relative truth predicate for a moment: If one wished to exhibit a Tarskian form with $\Phi$, one would need to write $T$(‘$\Phi$’) rather than $T(\Phi )$, so that the grammatical argument of $T$ would be the name of a sentence rather than a sentence. If one wrote $T(\Phi )$, $T$ would be a connective; and given a Tarski-like schema $T(\Phi )\leftrightarrow \Phi$, $T$ would have to be the trivial identity connective. The contrast is that given case-relativity, $T(\Phi , x)$ is by no means trivial; we shall have to engage in honest toil to find a schema that will serve. We might think merely to add the “true in” form to CIFOL, but that would rightly be judged as theft.

1.4 Extending CIFOL

Suppose we are looking for a truth predicate for some language, $L$. Tarski explained that a language with a truth predicate for $L$ must of necessity be stronger than $L$. What about a true-in schema for $L$? No such general result is available: It is obvious that there are languages with case-dependent semantics that can consistently contain their own true-in schema. But what about CIFOL in particular? It would seem—but I don’t offer a proof—that CIFOL, as it stands, does not permit an appropriate definition of “true in” for CIFOL. What is much more important, however, is that the modest extension of CIFOL to CIFOL$+$ by an extra pair of first order principles does permit the definition of a “true in” schema.

To begin, we add to CIFOL a pair of individual (not sentential) constants, t, f, that can be used to tag sentences true in a case with t and sentences false in a case with f.⁷ We can ensure that t and f do their jobs properly by postulating that they are necessarily distinct, and that some intension is possibly (extensionally) equal to each:

Axiom 1

(tf) $\vdash \square (\mathbf t \not =\mathbf f \,\,\wedge \,\,\exists x[\lozenge (x=\mathbf t )\,\,\wedge \,\,\lozenge (x=\mathbf f )])$

Evidently there must be at least two cases, a low-grade fact indeed. It is noteworthy that Axiom 1 is the only information that we have concerning t and f; we have no information about their extensions in any case, $\gamma$, except that their extensions are not the same. In particular, there is no assumption that t and f are “rigid designators.”

1.5 Picturing Intensions

In picturing the intensions of t and f, however, it is helpful to imagine first, that in every model, t and f are not only individual constants, but are also members of the extensional domain, $D$, and second, that in every case, $\gamma \in \Gamma$, t has itself as its own extension, and likewise for f. So in our imagination, t and f each has a constant extension, namely, the symbol itself in every case.⁸ As a further mental prop, we imagine that the set of cases, $\Gamma$, comes as a sequence, $\gamma _1, \gamma _2, \ldots , \gamma _i, \ldots$, so that

$$ int(\mathbf t {}) = \mathbf t \mathbf t \ldots , \mathbf t {},\ldots $$

and

$$ int(\mathbf f )=\mathbf f \mathbf f \ldots , \mathbf f , \ldots \ . $$

Of course, the intent of the pictures is not to limit the cardinality or structure of $\Gamma$ in any way. We may then picture the intension of a sentence, $\Phi$, as a sequence of occurrences of t and f, with the former marking those cases in which $\gamma \models \Phi$, and the latter marking the cases in which $\gamma \not \models \Phi$. Suppose, for example, that $\Phi$ is true in the odd cases and not true in the even cases. Recalling that in his semantics, Carnap defined “the range of $\Phi$” as the set of cases⁹ in which $\Phi$ is true, the intension

$$ int(\textit{x}) = \mathbf t \mathbf f \mathbf t \mathbf f \mathbf t \mathbf f , \ldots $$

could be a first-order (intensional) representation of the range of some $\Phi$.

2 Theory of Internal Ranges

In order to find an internal representation of “that $\Phi$ is true in case $\gamma$,” it is necessary to find an internal representation of $\gamma$. A natural thing to try is to represent $\gamma$ by an intension, that is, by a function in $\Gamma \mapsto D$, that picks out $\gamma$ uniquely. Standard set-theory tells us that a function $f\in (\Gamma \mapsto D)$, such that $f(\gamma )=ext_\gamma (\mathbf t )$, while $f(\gamma ')=ext_{\gamma '}(\mathbf f )$ for every $\gamma '\in \Gamma$ other than $\gamma$, would adequately fill that bill. We just need a way of saying this in CIFOL. How can we describe $x$ such that $int(x)\in \Gamma \mapsto D$ in such a way that $int(x)$ picks out a unique case $\gamma$? First, we want $int(x)$ to be pictured as having in each case $\gamma \in \Gamma$ either t or f.¹⁰ Let us describe such an $x$ as a “range,” since it does the work of a Carnapian range. In the language of CIFOL, we can carry “in each case” by the necessity modality, and “in some case” by the possibility modality. We make a definition of “proper range” that includes the requirement that the picture of $x$ contains at least one t and at least one f:

Definition 1

(Proper range, $PR$ )

$$ \forall x[ PR (x)\leftrightarrow _{d\!\!f}\leftrightarrow _{df}(\square (x=\mathbf t \,\,\vee \,\,x=\mathbf f ) \,\,\wedge \,\,\lozenge (x=\mathbf t )\,\,\wedge \,\,\lozenge (x=\mathbf f ))]. $$

Of course “$=$” in Definition 1 is extensional identity, telling us only that in each case either $\gamma \models x=\mathbf t$ or $\gamma \models x=\mathbf f$, but that is quite enough for our purpose.

Second, we want a way of saying that there is one and only one case $\gamma$ such that $\gamma \models x=\mathbf t$. (This cannot be said by directly using the “exactly one $x$” quantifier; it is cases that need counting, not intensions and not extensions.) “In at least one case” is easy: $\lozenge (x = \mathbf t {})$, and we have already included it as part of the definition of $PR$. To say “there is at most one case” is a bit more work. Begin by finding a way to say that one range, $x$, is a “subrange” of another range, $y$, meaning that in every case in which $x= \mathbf t$ is true, so also is $y = \mathbf t$; but not necessarily conversely (the picture is easily imagined).

Definition 2

(Subrange, $SubR$ )

$$ \forall x\forall y[ SubR (x, y)\leftrightarrow _{d\!\!f}\leftrightarrow _{df}( PR (x)\,\,\wedge \,\, PR (y)\,\,\wedge \,\,\square (x=\mathbf t \rightarrow y=\mathbf t ))]. $$

Lastly, define an “elementary range” as a minimal subrange (that is, a proper range without a proper subrange).

Definition 3

(Elementary range, $ElR$ )

$$ \forall x[ ElR (x)\leftrightarrow _{d\!\!f}\leftrightarrow _{df}( PR (x)\,\,\wedge \,\,\forall y[ SubR (y,x)\rightarrow \square (x=y)])]. $$

In a picture, it has to be that

$$\begin{aligned} int(x) = \mathbf f \mathbf f \ldots \mathbf f \mathbf f \mathbf t \mathbf f \mathbf f \ldots . \end{aligned}$$

(1)

That is, the picture of Eq. (1) shows exactly one t among all the fs. Please sit still for an interpretive hint: No matter what happens in an elementary case, exactly one case happens. In case-intensional logic, we want to say that a certain case happens. Let $x$ be an (intensional) individual variable. Then for $x$ to represent that a particular case, $\gamma$, happens, $x$ must code an elementary range, and it must be that $ext_\gamma (x)=ext_\gamma (\mathbf t )$. The trick, such as it is, comes to “identifying” cases.

The following can be verified by eye simply by noting that each atomic part of each of the three definiens occurs within the scope of a modal connective.

Fact 3

(Status of $PR , SubR$, and $ElR$ ) $PR$, $SubR$, and $ElR$ are modally constant; that is, their extensions do not vary with the case.

Intuitively, in each model, the elementary ranges are in one-one correspondence with the cases. Given a case, $\gamma$, let its mate be the unique intension, $x$, such that $ext_\gamma (x)=ext_\gamma (\mathbf t )$, and for $\gamma '\not =\gamma$, $ext_{\gamma '}(x)=ext_{\gamma '}(\mathbf f )$; and going the other way, given $x$ with an intension such that $ElR (x)$, let its mate be the one and only case $\gamma$ such that $ext_\gamma (x)=ext_\gamma (\mathbf t )$. So we should be able to say what we want to say about cases in CIFOL$+$, that is, indirectly, by instead speaking of elementary ranges. Let us use pictures of intensions to give an (abstract) example. Let $\Gamma =\{\gamma _1, \gamma _2, \gamma _3\}$. The following three tables exhibit the possible extensions (a) of a proper range, $PR$, (b) of an elementary range, $ElR$, and (c) of the property, $\lambda x( ElR (x)\,\,\wedge \,\,x=\mathbf t )$, of being an elementary range that happens.

In Table 1, you can see that $PR$ is modally constant, and in each case contains all t-f sequences with at least one t and at least one f.

Table 1 $PR$ (proper range)

Table 2 shows that $ElR$ is modally constant, and given $ElR (x)$, that the extension of $x$ in each $\gamma _i$ contains exactly one t.

Table 2 $ElR$ (Elementary range)

Table 3 $\lambda x( ElR (x)\,\,\wedge \,\,x=\mathbf t )$ (Elementary range that happens)

Table 3 on p. 64 is the most interesting, just because it is not modally constant. In case $\gamma _i$, it contains some or all elementary ranges—that is, the elementary range—with t in the column for $\gamma _i$, and f in each other column.

2.1 CIFOL$+$ and Elementary Ranges

There is still work to do in order to have a viable theory of elementary ranges. It is a trivial truth in our semantic metalanguage that for each $\gamma \in \Gamma$, there is an individual intension (in $\Gamma \mapsto D$) that is an elementary range whose extension in $\gamma$ is identical to the extension of t in $\gamma$. This is what Table 3 portrays in miniature. The problem is to try to bring this down to the language of CIFOL$+$ itself, rather than leaving it to pictures, or descriptions in the semantic metalanguage. Already a solution is almost possible: A CIFOL + Ax. 1 sentence that seems to have the right form is the following:

$$\begin{aligned} \square {\exists } x [ ElR (x) \,\,\wedge \,\,x = \mathbf t {}]. \end{aligned}$$

(2)

Equation 2 may be read informally as saying that necessarily there is an elementary range (a case) that happens, relying on a convention that a case that happens is marked with t. So CIFOL + Ax. 1 has the expressive power to say what needs to be said, a fact that might seem to solve the problem. However, the question is whether we can prove Eq. 2 in CIFOL + Ax. 1 itself; the answer is “not quite.” Bressan shows, however, that it can be proven in $MC^\nu$ with the help of a certain modest second-order axiom (his Axiom 12.19):

Bressan axiom 12.19.

$$ \vdash \square \exists P\forall x[(Px \leftrightarrow \Phi ) \,\,\wedge \,\,(\square Px\leftrightarrow \lozenge Px)]. $$

According to this axiom, for each case, $\gamma$, for each sentence, $\Phi$, presumably with $x$ free, there is a property, $P$, that applies to any $x$ if and only if $x$ satisfies the condition $\Phi$ in case $\gamma$, and furthermore is modally constant. So for each case, $\gamma$, the range of $P$ is the same in every case, $\gamma '$, and is precisely the range of $\Phi$ with respect to $x$ in the particular case, $\gamma$. In a picture, $P$ picks up the range of $\Phi$ with respect to $x$ in case $\gamma$, and duplicates that range in every case. The first conjunct of 12.19 is standard in classical second order logic; it is the addition of the second conjunct that is distinctive. It arises neither out of second order quantification theory nor out of S5 considerations.

We cannot merely add second-order 12.19 to CIFOL + Ax. 1, which is intended to be first order. For the purpose of proving that some elementary range happens, it suffices to define CIFOL$+$ by adding to CIFOL + Ax. 1 a single further first-order axiom involving a single “reserved predicate constant,” $P_0$, corresponding to instantiating $\Phi$ in 12.19 with $(x=\mathbf t \,\,\wedge \,\,\square (x=\mathbf t \,\,\vee \,\,x=\mathbf f ))$:

Axiom 2

(12.19 instance)

$$ \forall x[(P_0 x \leftrightarrow (x=\mathbf t \,\,\wedge \,\,\square (x=\mathbf t \,\,\vee \,\,x=\mathbf f ))) \,\,\wedge \,\,(\lozenge P_0 x \leftrightarrow \square P_0 x)]. $$

This $P_0$ consequence of Bressan’s axiom 12.19 is first order, and we count it as the second and last axiom of CIFOL$+$:

$$ \text{ CIFOL }+ \text{= } \text{ CIFOL } \text{+ } \text{ Ax. } \text{1,2. } $$

Observe that Axiom 2 does not begin with $\square$. As a first-order work-around of the second-order axiom 12.19, we are to think of it as only contingent, true in some particular case—a second-class axiom, if you like. In proofs, we mark only “first-class” formulas with the customary “$\vdash$”.

It is helpful to keep in mind that Axiom 2 can be seen as coming by second-order existential instantiation of $P$ in a demodalized version of 12.19 by $P_0$, all in the interest of keeping to the first order. We give bite to this mental picture of the axiom by imposing two requirements on CIFOL$+$: Axiom 2 must be the only postulate that mentions this predicate constant; and $P_0$ cannot occur in the last line of any complete proof in CIFOL$+$. (The requirements are the same as imposed on the result of “existential instantiation” in Belnap 2009.) To repeat, it is understood that although Axiom 2 may be used in a proof in CIFOL$+$, the last line must not contain $P_0$—that is, $P_0$ must be discharged. This requirement (and the requirement that no other axiom may contain an occurrence of $P_0$) distinguishes the logic CIFOL$+$ from a CIFOL$+$ theory with Axiom 2 as a non-logical axiom. The payoff is that we will now be able to prove Eq. 2. Indeed, we can prove not only the existence claim, but also existence and (strict) uniqueness.

Theorem 1

(Unique existence of an elementary range that happens)

$$ \vdash \square \exists x[ ElR (x) \,\,\wedge \,\,x=\mathbf t \,\,\wedge \,\,\forall y[( ElR (y)\,\,\wedge \,\,y=\mathbf t )\rightarrow \square (y=x)]]. $$

By Definition 4 coming up, this may be written as

$$ \vdash \square \exists _1^\square x[ ElR (x) \,\,\wedge \,\,x=\mathbf t ]. $$

It is essential to observe that Theorem 1 contains no occurrence of $P_0$. That means that we can count Theorem 1, once we prove it, as a theorem of logic, rather than merely as a consequence of Axiom 1 and the contingent Axiom 2.

3 Proving Theorem 1

The proof of the theorem will invoke three CIFOL$+$ abbreviative definitions. We use the standard notation for syntactic replacement; that is, $[y/x]\Phi$ stands for the expression obtained by replacing all free occurrences of $x$ by $y$. We will also employ the CIFOL definition of definite descriptions: The extension of the term ${{\iota }}x\Phi$ in a case $\gamma$ is $d\in D$ iff $d$ is the extensionally unique witness fulfilling $\Phi$ in case $\gamma$, and $*$ otherwise.

Definition 4

Unique existence, strict unique existence, extensionality

$$ \exists _1x\Phi \leftrightarrow _{d\!\!f}\leftrightarrow _{df}\exists x[\Phi \,\,\wedge \,\,\forall y [[y/x]\Phi \rightarrow (y=x)]]. $$

$$ \exists _1^\square x\Phi \leftrightarrow _{d\!\!f}\leftrightarrow _{df}\exists x[\Phi \,\,\wedge \,\,\forall y[[y/x]\Phi \rightarrow \square (y=x)]]. $$

$$ (extnl\ x)\Phi \leftrightarrow _{d\!\!f}\leftrightarrow _{df}\forall y[(\Phi \,\,\wedge \,\,x=y) \rightarrow [y/x]\Phi ] $$

These three definitions provide the respective CIFOL$+$ renderings of “there is a unique $x$ such that $\Phi$,” “there is a strictly unique $x$ such that $\Phi$,” and “$\Phi$ is extensional with respect to $x$.”

Fact 4

If $\Phi$ is extensional with respect to $x$ (i.e., if $(extnl\ x)\Phi$, so that $\Phi$ supports replacement of identicals), then $\vdash \exists _1 x \Phi \rightarrow \Phi ({{\iota }}x\Phi ).$

The proof of the Fact is straightforward.

We now turn to the proof in CIFOL$+$ of Theorem 1 stating that a strictly unique elementary case happens; the proof, which has five parts, occupies the rest of Sect. 3. We note that lines of the proof that contain any of $P_0$, ${\Theta }$, or ${\theta }$, the latter two of which are defined in terms of $P_0$, do not have the status of theorems of CIFOL$+$. Neither Axiom 2 nor any such line begins with the sign of necessity.¹¹ We emphasize the distinction when we mark proper theorems with the customary turnstile, $\vdash$. The last line of the proof is 4.12, which can be seen by inspection to contain no notation that relies on $P_0$ for its definition. For convenience, we break up the proof of Theorem 1 into five parts. Parts Ia and Ib prove that the individual constant $\theta$ denotes a proper range, and is (extensionally) equal to t—which says that $\theta$ happens. The conclusion of this part, since it contains $\theta$, depends on Axiom 2 as a hypothesis. Only at the end of Part IV can we discharge Axiom 2 as a hypothesis. The annotation “C.P.” signifies “Conditional proof,” and “$\forall$” advertises a quantifier rule. Watch for the role of $\theta$.

Part Ia

Part Ib

Note that $y$ is free in line 1a.2, and that $x$ is free in lines 1a.12, 1a.13. “MConst” in line 1b.10 refers to the part of Axiom 2 saying that $P_0$ is modally constant.

So ${\theta }$ is a proper range that is extensionally equal to t; but that conclusion of Part I is insufficiently strong. What is wanted is that ${\theta }$ is not just a proper range, but an elementary range, which is proved in Part III. Part II is chiefly “housekeeping” on the way to facts 2.12 and 2.13, required for Part III. Throughout Part II, $\Phi$ is any sentence, and $\rho _\Phi$ may be thought of as the internal representation of the range of $\Phi$.

Part II

Part III is chiefly a “conditional proof,” from 3.1 to 3.12, the purpose of which is to serve as a premiss for the use of the rule of conditional proof in justifying 3.13. Part III ends with establishing that ${\theta }$ is an elementary range equal to t, thus providing material for the existence portion of the desired conclusion, Theorem 1, at line 4.12.

Part III

Part III might be taken to establish $\theta$, introduced at line 1a.4, as a kind of logical constant; but is it unique? That is the job of the next and last part of the proof: Part IV establishes that $\theta$ is not only an elementary range extensionally equal to t, but is strictly (or intensionally) unique in that respect. Then existential generalization yields Theorem 1 at line 4.10, which, aside from the abbreviated and necessitated version at line 4.12, finishes our work: We will have established that elementary ranges, $ElR$, are suitable surrogates for “cases.”

Part IV

Observe in particular that 4.10–4.12 contain no occurrences of $P_0$ nor of any notation defined in terms of $P_0$; accordingly, we are entitled to count $4.12 = \text {Theorem}$ 1 in particular as a theorem of logic.

4 The concept of case-relative truth

Theorem 1 told us that necessarily there is an intensionally unique elementary range—our internal surrogate for “case”—that happens. This takes us part way to finding the idea of “true in a case” inside of CIFOL$+$. Let us step back and think for a minute about “true in a case.” That phrase is special, partly because there is very little intuitive support for the phrase “true in a world,” even though one can be led by well-worked-out formal machinery to prize the idea. A substitute phrase, “truth according to a world” seems marginally more idiomatic, although hardly an expression of conversational English. In contrast, “true in a case” is somewhat more idiomatic. I don’t mean the truth of sentences, which isn’t idiomatic at all, but rather certain informal “true that” expressions relativized to cases:

• It’s true that we shall get wet in case it rains, but otherwise not.

• I shall be sad in case you find fault with my examples.

• There are two cases in which it would be true that Mary will bake pies, but there is no case in which it would be true that I do the baking.

If we idealize by ruling out subcases, such a concept of truth can find a (formal) home in CIFOL$+$. The idea is to carry the true-in locution with a mixed nector (Curry), with one input place for a sentence and another for a term, and with the output being a sentence. So the locution that we are after in CIFOL$+$ will have the form

$$ T(\Phi ,\alpha ) $$

with $\Phi$ a CIFOL$+$ sentence and $\alpha$ a CIFOL$+$ term that we can take as standing for a case. The CIFOL$+$ sentence, $T(\Phi ,\alpha )$, is intended to be read in English with the pattern “that $\Phi$ is true in $\alpha$,” presupposing that $\alpha$ is an elementary range (no proper subranges). $T(\Phi ,\alpha )$ must be “found” (i.e., defined) in CIFOL$+$, not merely added.

We begin by noting that in any CIFOL$+$ model ${\mathcal {M}}= \langle \Gamma , D, {\mathcal {I}}\rangle$, for each case, $\gamma$, we can find the set of intensions representing elementary ranges that satisfy $ElR (x)$ in $\gamma$. We can gain some purchase on this in the semantic metalanguage of CIFOL$+$ by way of “$\gamma \models ( ElR (x)\,\,\wedge \,\,x=\mathbf t )$,” which can be read as saying that $x$ stands for the elementary case that holds in case $\gamma$. Simple logic tells us that if there is exactly one European king alive today, then to say that some European king alive today is bald is to say the same thing as saying that every European king alive today is bald. Just so, since intensionally speaking, in each model and in each case $\gamma$, there is exactly one elementary range that happens, we should expect that if $ElR (x)$, then $\lozenge (x=\mathbf t \,\,\wedge \,\,\Phi )$ (that $\Phi$ is true in some elementary range (= case) that happens) and $\square (x = \mathbf t \rightarrow \Phi )$ (that $\Phi$ is true in every elementary range that happens) equally express that $\Phi$ is true in the elementary range that happens in $\gamma$.¹² Furthermore, Lemma 1 below suggests that provided $ElR (x)$, each of ${\lozenge }(x = \mathbf t \,\,\wedge \,\,\Phi )$ and $\square (x= \mathbf t \rightarrow \Phi )$ is a suitable candidate for the CIFOL$+$ representation of  “$\Phi$ is true in case $x$.” We choose the former, and then from time to time mention the availability of the latter.

Definition 5

($\Phi$ is true in case $x$)

$$ \forall x[ ElR (x)\rightarrow (T(\Phi , x) \leftrightarrow _{d\!\!f}\leftrightarrow _{df}\lozenge (x=\mathbf t \,\,\wedge \,\,\Phi ))]. $$

Definition 5 is intended as a conditional definition, the thought being that one can apply the equivalence of $T(\Phi , x)$ and $\lozenge (x=\mathbf t \,\,\wedge \,\,\Phi )$ only when $x$ is an elementary range.

We need to verify the equivalence between $\lozenge (x = \mathbf t {} \,\,\wedge \,\,\Phi )$ and $\square (x = \mathbf t \rightarrow \Phi )$, under the hypothesis that $ElR (x)$, for that equivalence is required for showing that the appropriate clauses for $T(\Phi ,x)$ hold as they should. That is, we prove Lemma 1 as an essential step in verifying that “that $\Phi$ is true in case $x$” can be found in CIFOL$+$.

Lemma 1

(Fundamental equivalence)

$$ \vdash \forall x[ ElR (x)\rightarrow (\lozenge (x=\mathbf t \,\,\wedge \,\,\Phi )\leftrightarrow \square (x=\mathbf t \rightarrow \Phi ))]. $$

Lemma 1, which grounds our indifference between the two ways to express the “that $\Phi$ is true in case $x$” locution in CIFOL$+$—subject, of course to the assumption that $ElR$($x$)—encourages us to verify that the “true in” locution in CIFOL$+$ behaves properly with respect to the connectives of CIFOL$+$. That is, we show that the various metalinguistic semantic clauses can be approximated within CIFOL$+$ itself using the predicate $ElR$ and the mixed nector $T(\Phi ,x)$.¹³ The result, Theorem 2, is evidence for the conceptual coherence of CIFOL$+$ and its semantics. This is a striking result given that neither truth nor satisfaction (that is, “true on an assignment to the variables”) is available within CIFOL$+$, on pain of contradiction.¹⁴

Theorem 2

(Internal semantic clauses) Each of the following is provable in CIFOL$+$. We assume that $x$ has no free occurrence in $\Phi , \Phi _1$, or $\Phi _2$. All clauses are subject to the condition, $ElR (x)$, stating that $x$ is an elementary range— which is the internal representation of “$x$ is a case” (or $x\in \Gamma$). Here we are using “$\Phi$” to take the place of CIFOL$+$ sentences in schemata, so that the instances of e.g. ($\lnot$) are particular CIFOL$+$ sentences. (In contrast, in giving the metalinguistic semantics of CIFOL, as in Belnap and Müller 2013, “$\Phi$” denotes rather than takes the place of a CIFOL$+$ sentence.)

$(\wedge )$ :

$\vdash \forall x[ ElR (x)\rightarrow (T((\Phi _1\,\,\wedge \,\,\Phi _2), x) \leftrightarrow (T(\Phi _1,x) \,\,\wedge \,\,T(\Phi _2,x)))]$

$(\vee )$ :

$\vdash \forall x[ ElR (x)\rightarrow (T((\Phi _1\,\,\vee \,\,\Phi _2),x) \leftrightarrow (T(\Phi _1,x)\,\,\vee \,\,T(\Phi _2,x)))]$

$(\lnot )$ :

$\vdash \forall x[ ElR (x) \rightarrow (T(\lnot \Phi , x) \leftrightarrow \lnot T(\Phi ,x))]$

$(\forall y)$ :

$\vdash \forall x[ ElR (x) \rightarrow (T(\forall y \Phi , x) \leftrightarrow \forall y T(\Phi , x))]$

$(\exists y)$ :

$\vdash \forall x[ ElR (x) \rightarrow (T(\exists y\Phi , x) \leftrightarrow \exists y T(\Phi , x))]$

$(\square )$ :

$\vdash \forall x[ ElR (x) \rightarrow (T(\square \Phi , x) \leftrightarrow \forall z[ ElR (z)\rightarrow T(\Phi , z)])]$

$(\lozenge )$ :

$\vdash \forall x[ ElR (x) \rightarrow (T(\lozenge \Phi , x) \leftrightarrow \exists z[ ElR (z) \,\,\wedge \,\,T(\Phi , z)])]$

 

These “conditioned equivalences” are structurally like conditional definitions: $ElR$ appears as a presupposition of $T(\Phi ,x)$ rather than as an implicate, just as it would if we were to take the list as (say) giving the clauses of an inductive definition.

Proof. In each of the following, we assume that $x$ does not occur in $\Phi$, and as definiens of $T(\Phi ,x)$ we use whichever of $\square (x = \mathbf t \rightarrow \Phi )$ or $\lozenge (x = \mathbf t \,\,\wedge \,\,\Phi )$ is more convenient, relying on Lemma 1 as the warrant for our indifference.  

$(\wedge )$ :

It suffices that in quantified S5, $\vdash \forall x[ ElR (x)\rightarrow (\square (x=\mathbf t \rightarrow (\Phi _1\,\,\wedge \,\,\Phi _2)) \leftrightarrow (\square (x=\mathbf t \rightarrow \Phi _1)\,\,\wedge \,\,\square (x=\mathbf t \rightarrow \Phi _2)))].$

$(\vee )$ :

It suffices that in quantified S5, $\vdash \forall x[ ElR (x)\rightarrow (\lozenge (x=\mathbf t \,\,\wedge \,\,(\Phi _1\,\,\vee \,\,\Phi _2)) \leftrightarrow (\lozenge (x=\mathbf t \,\,\wedge \,\,\Phi _1)\,\,\vee \,\,\lozenge (x=\mathbf t \,\,\wedge \,\,\Phi _2)))].$

$(\lnot )$ :

By the fundamental equivalence of Lemma 1, $\vdash \forall x[ ElR (x)\rightarrow (\lozenge (x=\mathbf t \,\,\wedge \,\,\lnot \Phi ) \leftrightarrow \square (x=\mathbf t \rightarrow \lnot \Phi ))]$. By S5, $\square (x=\mathbf t \rightarrow \lnot \Phi )$ is interchangeable with $\lnot \lozenge (x=\mathbf t \,\,\wedge \,\,\Phi )$. So using Def. 5 twice, we have the required conditional equivalence:

$$\vdash \forall x [ ElR (x)\rightarrow (T(\lnot \Phi ,x)\leftrightarrow \lnot (T(\Phi , x)))]$$

$(\forall y)$ :

It suffices that in quantified S5, $\vdash \forall x[ ElR (x)\rightarrow (\square (x=\mathbf t \rightarrow \forall y\Phi ) \leftrightarrow \forall y[\square (x=\mathbf t \rightarrow \Phi )])]$.

$(\exists y)$ :

It suffices that in quantified S5, $\vdash \forall x[ ElR (x)\rightarrow (\lozenge (x=\mathbf t \,\,\wedge \,\,\exists y\Phi ) \leftrightarrow \exists y[\lozenge (x=\mathbf t \,\,\wedge \,\,\Phi )])]$.

($\square$):

It suffices that in quantified S5, $\vdash \forall x[ ElR (x)\rightarrow \lozenge (x = \mathbf t \,\,\wedge \,\,\square \Phi ) \leftrightarrow \forall z[ ElR (z)\rightarrow \lozenge (z=\mathbf t \,\,\wedge \,\,\Phi )]].$ We supply detail, first proving 6.19 as a lemma.

Now we are ready to prove what is needed for the “truth-condition” clause $(\square )$ as line 7.13.

 

Lastly, ($\lozenge$). It suffices to dualize the argument for $\square$, which concludes the proof of Theorem 2, and in this way speaks to a fit between CIFOL$+$ and its internal theory of “true in a case.” $\blacksquare$

5 Summary

To put these results in a suitable context, we repeat that our aim has been to find a way of properly formalizing “that ${\Phi }$ is true in case $\gamma$” in the first-order extension, CIFOL$+$, of CIFOL, which is itself a first-order distillation from Bressan’s higher-order modal calculus, $MC^\nu$. This aim is intermediate between the futile aim of formalizing naive disquotation in CIFOL$+$, “ ‘$\Phi$’ is true iff $\Phi$,” and the too-easy aim of formalizing the tautological “that $\Phi$ is true iff $\Phi$.”

We began by giving an extremely brief account of the chief features of CIFOL, described in Belnap and Müller 2013, and we indicated the wisdom of extending CIFOL to CIFOL$+$ by including a first-order trace of a certain second-order principle. We introduced a way of understanding a pair of CIFOL$+$ singular terms, t and f, as playing the role of internal truth values. Then we defined the CIFOL$+$ predicate, $ElR$ (elementary range), as a suitable surrogate for “case,” and $( ElR (x)\,\,\wedge \,\,x=\mathbf t )$ as a surrogate for “$x$ is a case that happens,” giving a detailed proof that these CIFOL$+$ concepts are provably adequate representations of their respective intuitive ideas. Finally, we showed that $\lozenge (x = \mathbf t \,\,\wedge \,\,\Phi )$ adequately represents in CIFOL$+$ itself “that $\Phi$ is true in case $x$,” where $\Phi$ is a CIFOL$+$ sentence and $x$ denotes a CIFOL$+$ surrogate case, thus successfully threading our way between the impossible task of formalizing “ ‘$\Phi$’ is true” and the trivial task of formalizing “that $\Phi$ is true.”