2.1 Strong Kleene logic

Kripke defines his interpretations of $\mathcal {L}_T$ using the trivalent logic $\mathsf {K3}$ , also known as the strong Kleene logic. According to $\mathsf {K3}$ , a structure w can stand in one of three semantic relations with a formula $\varphi $ :

• • $w\vDash _{\mathsf {K3}}\varphi $ , i.e., $\varphi $ is true in $w.$

• • , i.e., $\varphi $ is false in $w.$

• • $w\uparrow _{\mathsf {K3}}\varphi $ i.e., $\varphi $ is neither in $w.$

The semantics of conjunction is given by the following clauses:

• • $w\vDash _{\mathsf {K3}}\varphi \wedge \psi $ if $w\vDash _{\mathsf {K3}}\varphi $ and $w\vDash _{\mathsf {K3}}\varphi .$

• • if or

• • $w\uparrow _{\mathsf {K3}}\varphi $ otherwise.

The semantics of negation is given by the following clauses:

• • $w\vDash _{\mathsf {K3}}\neg \varphi $ if

• • if $w\vDash _{\mathsf {K3}}\varphi .$

• • $w\uparrow _{\mathsf {K3}}\neg \varphi $ otherwise.

The semantics of the universal quantifier is given by the following clauses:

• • $w\vDash _{\mathsf {K3}}\forall x \; \varphi (x)$ if for every $d\in w$ , $w\vDash _{\mathsf {K3}}\varphi (d)$ .

• • if for some $d\in w$ , .

• • $w\uparrow _{\mathsf {K3}}\forall x \; \varphi (x)$ otherwise.

2.2 Classification of sentences

Kripke introduces a large collection of 3-valued (true, false, neither) models for $\mathcal {L}_T$ . These 3-valued models are typically called “fixed points,” since Kripke defines them as the fixed points of a certain function (namely, the Kripke jump). The details of this function are not important for us, but the “fixed points” terminology is ubiquitous, so we will continue to use it. For work on the structure of these fixed points see Cantini [Reference Cantini3] and Fitting [Reference Fitting7].

For any formula $\varphi (x)$ in the language of $\mathcal {L}_T$ , a standard self-reference construction yields an $\mathcal {L}_T$ sentence $\psi $ which “says” $\varphi (\ulcorner \psi \urcorner )$ . In particular, $\psi $ and $\varphi (\ulcorner \psi \urcorner )$ have the same semantic value in each fixed point. For instance, there are $\mathcal {L}_T$ sentences $\lambda ,\tau ,\gamma $ such that:

• • $\lambda $ says $\neg \mathsf {True}(\ulcorner \lambda \urcorner )$ .

• • $\tau $ says $ \mathsf {True}(\ulcorner \tau \urcorner )$ .

• • $\gamma $ says $ \mathsf {True}(\ulcorner \gamma \urcorner )\vee \neg \mathsf {True}(\ulcorner \gamma \urcorner )$ .

In fact, there are many such sentences. We will sometimes appeal to this fact, which is well-known in the theory of truth literature.

The liar $\lambda $ , truth-teller $\tau $ , and tautology-teller $\gamma $ are all ungrounded, so they all have value neither in the minimum model.

The liar $\lambda $ is paradoxical. But the truth-teller $\tau $ and tautology-teller $\gamma $ are not paradoxical:

• • $\tau $ has value true in some models and value false in others.

• • $\gamma $ has value true in some models and does not have the value false in any models.

Though neither $\tau $ nor $\gamma $ is paradoxical, it is worth noting that $\gamma $ alone cannot take on both of the binary truth values. We introduce the following definition to discuss this property of $\gamma $ .

Any grounded sentence is inevitable. There are also ungrounded inevitable sentences. For instance, if $\tau $ is a truth-teller, then the sentence $\tau \vee \neg \tau $ is inevitable (inevitably true) as is $\tau \wedge \neg \tau $ (inevitably false).

Informally, the intrinsic sentences are those inevitable sentences whose truth/falsity does not depend on any arbitrary sentences. Here is a more precise definition.

Definition 2.7. A fixed point w is intrinsic if for every fixed point v,

is consistent. A sentence $\varphi $ is intrinsic if it is true or false in an intrinsic fixed point.

Note that inevitability and intrinsicality come apart. The tautology-teller $\gamma $ is both intrinsic and inevitable. By contrast, $\tau \vee \neg \tau $ is inevitable but not intrinsic. The issue is that any fixed point which makes $\tau \vee \neg \tau $ true must either make $\tau $ true or $\neg \tau $ true. So $\tau \vee \neg \tau $ can only be made true by making a binary truth-value assignment that is incompatible with other possible binary truth-value assignments.

4.1 Normal forms

One of our main tools will be a normal form theorem due to Carnap [Reference Carnap4]. Let’s begin by drawing a distinction between two kinds of formulas.

Note that the distinction between extensional and intensional formulas is exclusive but not exhaustive.

The following notion is inspired by the model-theoretic notion of an isolated type.

$\mathbf {S5[Con]}$ refutes (i) and makes the additional conjuncts in (ii) and (iii) redundant. Hence, we have the following.

Proposition 4.6. The extensional 1-isolators for $\mathbf {S5[Con]}$ are

$$ \begin{align*}T(x), F(x), N(x).\end{align*} $$

There is an analogous notion of intensional 1-isolators.

Let’s restrict our attention to $\mathbf {S5[Con]}$ and its extensions. Here is how we characterize the intensional 1-isolators of such a system. We begin by considering all formulas of the form:

$$ \begin{align*}^{+}_{\neg} \lozenge T(x) \wedge ^{+}_{\neg} \lozenge F(x) \wedge ^{+}_{\neg} \lozenge N(x).\end{align*} $$

That is, for each of the extensional 1-isolators, we choose whether it is possible or not and add that choice as a conjunct. Call these the intensional pre-1-isolators. To isolate the intensional 1-isolators we must figure out which of the intensional pre-1-isolators are consistent.

$\mathbf {S5[Con]}$ refutes exactly one of the intensional pre-1-isolators:

$$ \begin{align*}\mathbf{S5[Con]}\vdash \neg \big(\neg \lozenge T(x) \wedge \neg \lozenge F(x) \wedge \neg \lozenge N(x)\big).\end{align*} $$

$\mathbf {S5[Con, Ground]}$ refutes one more in addition:

$$ \begin{align*}\mathbf{S5[Con, Ground]}\vdash \neg \big(\lozenge T(x) \wedge \lozenge F(x) \wedge \neg \lozenge N(x)\big).\end{align*} $$

We are now ready to state Carnap’s theorem. To make sense of Carnap’s theorem, recall the convention that an empty disjunction of formulas is just a contradiction.

4.2 Counting

Carnap [Reference Carnap4] calculates the number of formulas up to provable equivalence in the modal logic $\mathsf {S5}$ . Note the emphasis on the word logic. The system that Carnap studies is in the typical language of modal logic, i.e., without the predicates $T,F$ but with propositional variables $p_1,p_2,\dots $ . There are far more equivalence classes of 1-formulas in our system $\mathbf {S5}$ than in the modal logic Carnap studied. Throughout this paper we provide Carnap-style calculations of the number of formulas up to provable equivalence in a various modal systems. As we progress to stronger and stronger systems, the number of equivalence classes shrinks. Hence, these calculations provide an exact, quantitative illustration of the increasing strength of the systems under consideration.

Proof. Let’s introduce some abbreviations:

$$ \begin{align*} B(x) & \quad T(x) \wedge F(x).\\ T_{only}(x) & \quad T(x) \wedge \neg F(x).\\ F_{only}(x) & \quad \neg T(x) \wedge F(x).\\ N(x) & \quad \neg T(x) \wedge \neg F(x). \end{align*} $$

$\mathbf {S5}$ has 4 extensional 1-isolators and 15 intensional 1-isolators, namely, all 1-formulas of the form:

$$ \begin{align*}^{+}_{\neg} \lozenge B(x) \wedge ^{+}_{\neg} \lozenge T_{only}(x) \wedge ^{+}_{\neg} \lozenge F_{only}(x)\wedge ^{+}_{\neg} \lozenge N(x)\end{align*} $$

except for the one with all negations.

Each extensional 1-isolator is inconsistent with the intensional 1-isolators claiming that it is impossible, and consistent otherwise.

So, for instance, $B(x)$ is consistent with all and only those intensional 1-isolators of the form:

$$ \begin{align*}\lozenge B(x) \wedge ^{+}_{\neg} \lozenge T_{only}(x) \wedge ^{+}_{\neg} \lozenge F_{only}(x)\wedge ^{+}_{\neg} \lozenge N(x)\end{align*} $$

of which there are exactly $2^3=8$ .

A 1-isolator is a consistent conjunction of an extensional 1-isolator and an intensional 1-isolator. So there are $4\times 8=32$ many 1-isolators for $\mathbf {S5}$ . Hence, the number of 1-formulas up to provable equivalence is exactly $2^{32}=4{,}294{,}967{,}296$ .

Proof. We approach this calculation in a similar way. This time the extensional 1-isolators are $T(x),F(x),N(x)$ .

Focus on $T(x)$ for a moment. It is consistent with all and only those intensional 1-isolators of the form:

$$ \begin{align*}\lozenge T(x) \wedge ^{+}_{\neg} \lozenge F(x)\wedge ^{+}_{\neg} \lozenge N(x)\end{align*} $$

of which there are exactly $2^2=4$ .

A 1-isolator is a consistent conjunction of an extensional 1-isolator and an intensional 1-isolator. So there are $3\times 4 = 12$ many 1-isolators for $\mathbf {S5[Con]}$ . Hence, the number of formulas up to provable-equivalence is exactly $2^{12}=4096$ .

Proof. Again, the extensional 1-isolators are $T(x),F(x),N(x)$ .

Focus on $T(x)$ for a moment. It is consistent with all and only those intensional 1-isolators of the form:

$$ \begin{align*}\lozenge T(x) \wedge ^{+}_{\neg} \lozenge F(x)\wedge ^{+}_{\neg} \lozenge N(x)\end{align*} $$

except (by the $\mathbf {Ground}$ axiom) for

$$ \begin{align*}\lozenge T(x) \wedge \lozenge F(x)\wedge \neg \lozenge N(x).\end{align*} $$

So $T(x)$ is consistent with $2^2-1=4-1=3$ intensional 1-isolators. Likewise, $F(x)$ is consistent with $3$ intensional 1-isolators. $N(x)$ is consistent with $4$ (there is no need to delete one since we focus on formulas including $\lozenge N(x)$ ).

A 1-isolator is a consistent conjunction of an extensional 1-isolator and an intensional 1-isolator. So there are $3+3+4 = 10$ many 1-isolators for $\mathbf {S5[Con,Ground]}$ . Hence, the number of formulas up to provable-equivalence is exactly $2^{10}=1024$ .

4.3 Completeness

In this section we present a complete axiomatization of the one-variable fragment of the modal theory of $\mathbf {FIX}$ . Completeness follows easily from Carnap’s normal form theorem. The connection between normal forms and completeness theorems was explored previously in Fine [Reference Fine6]. We extend this result to the full modal language in a later section.

Proof. The soundness direction is Proposition 3.8. Let’s focus on completeness. Suppose that $\mathbf {S5[Con, Ground]}\nvdash \varphi $ . Then, by classical logic, $\mathbf {S5[Con, Ground]}+\neg \varphi $ is consistent. By Theorem 4.9,

$$ \begin{align*}\mathbf{S5[Con, Ground]}\vdash \neg \varphi \leftrightarrow (\psi_1\vee\dots\vee\psi_k),\end{align*} $$

where each $\psi _i$ is a 1-isolator. By classical logic, at least one of these 1-isolators $\psi _i$ is consistent. By Lemma 4.13, we infer that there is some $\star $ such that $\mathbf {FIX}\Vdash _{V^\star } \psi _i$ . Hence $\mathbf {FIX}\Vdash _{V^\star } \neg \varphi $ , so $\mathbf {FIX}\nVdash \varphi $ .

Before continuing, we note that the normal form theorem also yields an exact characterization of the number of $\mathbf {FIX}$ -definable sets.

4.4 Descriptive complexity

In this section we will finally fulfill our promise to prove the following result.

There are multiple ways of verifying this, and we will present two. One could check all 64 single variable definitions, although this would be tedious. Luckily, there are more conceptual arguments.

Every $\mathbf {FIX}$ -definable set is definable by an intensional 1-formula. This is because if $\varphi \mathbf {FIX}$ -defines a set $\mathcal {A}$ , then so does $\Box \varphi $ . We have already seen that each intensional 1-formula is $\mathbf {S5[Con, Ground]}$ -equivalent to a disjunction of intensional 1-isolators. So, pushing quantifiers in, we see that every modal definition is equivalent to a formula of the following form:

$$ \begin{align*}\big( {}_{\lozenge}^{\Box} {}_{\neg}^{+} {}_{F}^{T} (x) \wedge \dots \wedge {}_{\lozenge}^{\Box} {}_{\neg}^{+} {}_{F}^{T} (x) \big)\vee \dots \vee ({}_{\lozenge}^{\Box} {}_{\neg}^{+} {}_{F}^{T} (x) \wedge \dots \wedge {}_{\lozenge}^{\Box} {}_{\neg}^{+} {}_{F}^{T} (x)\big).\end{align*} $$

Let’s say that any such formula is in basic form.

The desired indefinability result then follows from the following theorem.

4.5 Indiscernibility

The previous result demonstrates the non-definability of a great number of sets. Nevertheless, it is a coarse tool. We can prove the indefinability of the intrinsic sentences in a more informative way.

Informally, sets $\mathcal {A}$ and $\mathcal {B}$ are $\mathbf {FIX}$ -indiscernible just in case every formula that applies to the $\mathcal {A}$ s applies to the $\mathcal {B}$ s and vice-versa. We will prove that the intrinsic sentences and the inevitable sentences are $\mathbf {FIX}$ -indiscernible, whence the set of intrinsic sentences—the smaller of the two sets—cannot be definable.

Proof. Let $\mathcal {A}$ be the set of intrinsic and $\mathcal {B}$ the set of inevitable sentences. Then (2) implies that (1) (Definition 4.23) is trivial.

It suffices to check that (1) implies (2). So assume (1), i.e.,

$$ \begin{align*}\oplus \quad \text{For all }\star \text{ with }x^\star \text{ intrinsic, }\mathbf{FIX}\Vdash_{\mathbf{V^\star}} \varphi(x).\end{align*} $$

We may assume that $\varphi $ is an intensional formula (if it is not, just stick a $\Box $ in front of it). We may then assume that $\varphi $ is in normal form, i.e., $\varphi $ is a disjunction of intensional 1-isolators.

Now the intensional 1-isolators are the following six formulas:

1. (i) $\psi _1(x):=\lozenge T(x) \wedge \lozenge F(x) \wedge \lozenge N(x).$

2. (ii) $\psi _{2}(x):=\lozenge T(x) \wedge \neg \lozenge F(x) \wedge \lozenge N(x).$

3. (iii) $\psi _{3}(x):=\neg \lozenge T(x) \wedge \lozenge F(x) \wedge \lozenge N(x).$

4. (iv) $ \psi _{4}(x):=\lozenge T(x) \wedge \neg \lozenge F(x) \wedge \neg \lozenge N(x).$

5. (v) $ \psi _{5}(x):=\neg \lozenge T(x) \wedge \lozenge F(x) \wedge \neg \lozenge N(x).$

6. (vi) $ \psi _{6}(x):=\neg \lozenge T(x) \wedge \neg \lozenge F(x) \wedge \lozenge N(x).$

Note that the set of inevitable sentences is defined by the disjunction

$$ \begin{align*}\psi_2(x)\vee \psi_3(x) \vee \psi_4(x)\vee \psi_5(x).\end{align*} $$

Suppose, for the sake of contradiction, that (2) fails. Then there is some $\star $ such that $y^\star =\psi $ is inevitable and that $\mathbf {FIX}\nVdash _{\mathbf {V^\star }} \varphi (y)$ . So $\varphi $ must be missing one of the disjuncts required to define the inevitable sentences, i.e., $\psi _2(x)$ ,…, $\psi _5(x)$ . Let’s break into cases.

Case 1: $\varphi $ is missing disjunct $\psi _2$ . But $\gamma $ is intrinsic and $\psi _2(\gamma )$ . So if $x^\star $ is $\gamma $ , then $\mathbf {FIX}\nVdash _{\mathbf {V^\star }} \varphi (x)$ , contra $\oplus $ .

Case 2: $\varphi $ is missing disjunct $\psi _3$ . But $\neg \gamma $ is intrinsic and $\psi _3(\neg \gamma )$ . So if $x^\star $ is $\neg \gamma $ , then $\mathbf {FIX}\nVdash _{\mathbf {V^\star }} \varphi (x)$ , contra $\oplus $ .

Case 3: $\varphi $ is missing disjunct $\psi _4$ . But $0=0$ is intrinsic and $\psi _4(0=0)$ . So if $x^\star $ is $0=0$ , then $\mathbf {FIX}\nVdash _{\mathbf {V^\star }} \varphi (x)$ , contra $\oplus $ .

Case 4: $\varphi $ is missing disjunct $\psi _5$ . But $0=1$ is intrinsic and $\psi _5(0=1)$ . So if $x^\star $ is $0=1$ , then $\mathbf {FIX}\nVdash _{\mathbf {V^\star }} \varphi (x)$ , contra $\oplus $ .

5.1 Counting formulas

Let’s begin with some relatively easy counting problems. We will turn to more difficult counting problems in a later section.

5.2 Matrices

The combinatorics of definability is much harder when $n>1$ . In this section, for the sake of developing intuitions, we focus on the 2-variable case. Let’s begin by considering Table 1:

Table 1

All extensional 2-isolators.

Table 1 Long description

The table consists of three rows and three columns. The first row contains TT in the first cell, TF in the second cell, and TN in the third cell. The second row contains FT, FF, and FN from left to right. The third row contains NT, NF, and NN from left to right. Each cell label represents a distinct extensional 2-isolator as indicated by the caption.

We identify each cell of the matrix with an extensional 2-isolator. In particular, we identify the cell AB with the formula $A(x_1)\wedge B(x_2)$ . For instance, we identify the cell TN with the formula $T(x_1) \wedge N(x_2)$ . This yields an association of extensional 2-isolators with pairs of numbers, via Table 2. We will often consider subsets $\mathcal {S}$ of the $3\times 3$ matrix and we move freely between writing as though $\mathcal {S}$ contains NN, $N(x_1)\wedge N(x_2)$ , and (3,3), trusting that no confusion will arise.

Table 2

Standard numbering of the $3\times 3$ matrix.

Table 2 Long description

Starting from the top row, the first cell is labeled 1 comma 1, followed by 1 comma 2 and 1 comma 3. The second row contains 2 comma 1, 2 comma 2, and 2 comma 3. The bottom row has 3 comma 1, 3 comma 2, and 3 comma 3. Each label represents the row and column position within the three by three matrix, arranged in a grid with three rows and three columns.

Each intensional 2-isolator for $\mathbf {S5[Con]}$ corresponds to a subset of the $3 \times 3$ matrix. In particular, each intensional 2-isolator has the form:

$$ \begin{align*}\bigwedge \{\lozenge \varphi \mid \varphi\in \mathcal{S}\} \wedge \bigwedge \{\neg\lozenge \varphi \mid \varphi \notin \mathcal{S}\},\end{align*} $$

where $\mathcal {S}$ is some subset of the matrix.

However, it is not the case that each subset $\mathcal {S}$ of the matrix yields an intensional 2-isolator for $\mathbf {S5[Con]}$ . The issue is that some of the subsets of the matrix correspond to $\mathbf {S5[Con]}$ -refutable formulas, and intensional 2-isolators are consistent by definition. For instance, letting $\mathcal {S}$ be the empty set yields the formula:

$$ \begin{align*}\bigwedge \{\neg\lozenge \varphi \mid \varphi \notin \emptyset\},\end{align*} $$

which is refuted by $\mathbf {S5[Con]}$ , whence it is not an intensional 2-isolator.

The crucial question for us is to identify which subsets of the matrix actually reflects the intensional properties of $\mathcal {L}_T$ sentences. Let’s review some examples.

Consider Tables 3–6. Each of these images exhibits a subset of the $3\times 3$ matrix. In each case, consider the following question: Is there a variable assignment $\star $ such that $x_1^\star $ and $x_2^\star $ can attain all and only these combinations of values? Put another way, given a subset $\mathcal {S}$ of the $3\times 3$ matrix, is there a variable assignment $\star $ such that $\mathbf {FIX} \Vdash _{V^\star } \bigwedge \{\lozenge \varphi \mid \varphi \in \mathcal {S}\} \wedge \bigwedge \{\neg \lozenge \varphi \mid \varphi \notin \mathcal {S}\}$ ?

Table 3

A proper subset of the extensional 2-isolators.

Table 3 Long description

Starting from the leftmost column, the header is T T. Below T T are two mathematical expressions, each representing an extensional 2-isolator. The middle column is labeled T F, with two stacked expressions beneath it, also denoting extensional 2-isolators. The rightmost column is labeled T N, and similarly contains two vertically stacked mathematical expressions. All expressions are distinct and correspond to a proper subset of the extensional 2-isolators. The spatial arrangement is consistent across all columns, with headers at the top and expressions stacked below.

Table 4

A proper subset of the extensional 2-isolators.

Table 4 Long description

Starting at the top row, the first cell is labeled T T, the second cell is labeled T F, and the third cell contains a symbolic entry. The second row, from left to right, contains three symbolic entries, each representing a subset of extensional 2-isolators, with the first and third cells labeled T T and T F respectively. The third row, from left to right, contains three symbolic entries, with the first and third cells labeled T T and T F. All symbolic entries are graphical representations of logical isolators, and the table as a whole presents a proper subset of the extensional 2-isolators as indicated in the caption.

Table 5

A proper subset of the extensional 2-isolators.

Table 5 Long description

Starting from the top row, the left cell contains T T, the middle cell displays a mathematical expression, and the right cell shows another mathematical expression. The second row begins with a mathematical expression in the left cell, F F in the middle cell, and a mathematical expression in the right cell. The third row starts with a mathematical expression in the left cell, a mathematical expression in the middle cell, and N N in the right cell. All mathematical expressions are rendered as inline graphics, and the initialisms T T, F F, and N N are spaced letter-by-letter.

Table 6

A proper subset of the extensional 2-isolators.

Table 6 Long description

Beginning at the top-left, the first row contains cells labeled T T, a table with entries T T, T N, F N, N T and mathematical symbols, and T N. The second row starts with a table showing T T, T N, F N, N T and mathematical symbols, followed by another table with similar labels and symbols, and F N. The third row begins with N T, then a table with T T, T N, F N, N T and mathematical symbols, and finally a table with the same labels and symbols. Each table cell contains a subset of extensional 2-isolators, with mathematical notation distinguishing the entries.

The answers are given here:

Table 3: Yes. Let $x_1^\star $ be a grounded truth (e.g., $0=0$ ) and $x_2^\star $ be a truth-teller.

Table 4: No. Note that the first two columns are non-empty but the third is empty. Thus, the axiom $\mathbf {Ground}$

$$ \begin{align*}\big( \lozenge T(x) \wedge \lozenge F(x) \big) \to \lozenge N(x)\end{align*} $$

rules out this possibility, and $\mathbf {FIX}\Vdash \mathbf {Ground}$ .

Table 5: Yes. Let $x_1^\star $ and $x_2^\star $ be the same truth-teller.

Table 6: No. However, one cannot see that there is no such assignment merely deploying the principles codified in $\mathbf {S5[Con,Ground]}$ . Indeed, we must introduce the following axiom:

$$ \begin{align*}\mathbf{Min_2} := \big(\lozenge N(x) \wedge \lozenge N(y)\big) \to \lozenge \big(N(x)\wedge N(y)\big).\end{align*} $$

Even though $\mathbf {S5[Con,Ground]}\nvdash \mathbf {Min_2}$ , it is still the case that $\mathbf {FIX}\Vdash \mathbf {Min_2}$ (by Remark 2.4). Note that the axiom $\mathbf {Min_2}$ rules out Table 6 since the third row is non-empty and the third column is non-empty but the corner element NN is missing.

This last example identifies the only constraint on intensional 2-isolators that is not codified in the $\mathbf {S5[Con,Ground]}$ axioms.

5.3 The prime conditions

For the full completeness theorem we need new axioms:

$$ \begin{align*} \mathbf{Min_n}:= \big(\lozenge N(x_1) \wedge \dots \wedge \lozenge N(x_n)\big) \to \lozenge \big(N(x_1)\wedge\dots\wedge N(x_n)\big). \end{align*} $$

Remark 5.5. For $n>k$ , $\mathbf {Min_n}\vdash \mathbf {Min_k}$ . To see this, just pick an instance of $\mathbf {Min_n}$ wherein some variables are repeated. For instance, to see that $\mathbf {Min_3}\vdash \mathbf {Min_2}$ note that the following instance of $\mathbf {Min_3}$ :

$$ \begin{align*}\big(\lozenge N(x_1) \wedge \lozenge N(x_1) \wedge \lozenge N(x_2)\big) \to \lozenge \big(N(x_1)\wedge N(x_1)\wedge N(x_2)\big)\end{align*} $$

is (logically equivalent to) an instance of $\mathbf {Min_2}$ .

In the previous section we identified intensional $2$ -isolators with subsets of the $3\times 3$ matrix. For the n-variable case, we must turn from matrices to tensors, which are generalizations of matrices beyond two dimensions. In particular, we will be interested in $3^n$ tensors, i.e., $\underbrace {3\times \cdots \times 3}\limits _{{\scriptsize n \text { times}}}$ matrices.

Let $[3]^n$ be the set of n-tuples from the set $\{1,2,3\}$ . This is the set of positions in a $3^n$ tensor. We can no longer speak only of rows and columns. Instead, we speak in terms of slices. The rows are the 1-slices, the columns are the 2-slices, and so on. How do we speak of the first row, the second row, the third column, etc.? The first row is the first layer in the first slice, the third column is the third layer in the second slice, and so on. We introduce the following notation.

Definition 5.6. For $k\leq 3$ and $j\leq n$ , the kth layer of the jth slice (written $j_k$ ) is

$$ \begin{align*}\{a\in [3]^n \mid \exists b_1,\dots,\exists b_{n-1} \; a=\langle b_1,\dots b_{j-1}, k, b_{j},\dots,b_{n-1} \rangle\}.\end{align*} $$

Note that as $j_k$ is defined, it is a set of positions in the $3^n$ tensor. That is, so far we have still only discussed positions. The tensors we are interested in are 0–1 valued tensors, i.e., assignments of 0 and 1 to these positions. It is easiest to think of these as just subsets of $[3]^n$ , and that is how we will proceed.

We now introduce a definition that will be crucial to the proofs of the remaining theorems.

5.4 The main lemma

The main technical lemma of this paper connects the prime conditions with $\mathbf {FIX}$ -satisfiability. That is, this lemma shows that those sets that satisfy the prime conditions are exactly the sets that reflect the intensional properties of $\mathcal {L}_T$ sentences.

Proof. (2) implies (1): This follows from soundness, i.e.,

$$ \begin{align*}\mathbf{FIX}\Vdash \mathbf{S5[Con,Ground,Min_n]}.\end{align*} $$

See Remarks 2.1 and 2.4.

(1) implies (2): Suppose that $\mathcal {S}$ meets the prime conditions. There are two cases to consider:

1. (I) $\mathcal {S}$ does not contain $(3,\dots ,3)$ .

2. (II) $\mathcal {S}$ does contain $(3,\dots ,3)$ .

Case (I): There are very few ways a set can meet the prime conditions and omit (3,…,3). The important thing to note is that:

Claim 1. For some $j\leq n$ and some $i\leq 2$ , $\mathcal {S}$ is contained in the ith layer of the jth slice.

Proof. To see that the claim holds, suppose that for all $j\leq n$ , for all $i\leq 2$ , $\mathcal {S}$ is not contained in the ith layer of the jth slice. Since $\mathcal {S}$ meets the prime conditions, $\mathcal {S}$ is non-empty. Thus, for every j, $\mathcal {S}$ must intersect some layer of the jth slice. We reason as follows:

• • $\mathcal {S}$ is not contained in the first layer of the jth slice, so $\mathcal {S}$ intersects either the second or third layer of the jth slice.

• • $\mathcal {S}$ is not contained in the second layer of the jth slice, so $\mathcal {S}$ intersects either the first or third layer of the jth slice.

It follows that either $\mathcal {S}$ intersects $j_3$ or it intersects both $j_1$ and $j_2$ . In the latter case, the prime conditions imply that $\mathcal {S}$ intersects $j_3$ . So either way, $\mathcal {S}$ intersects $j_3$ .

So, for every j, $\mathcal {S}$ intersects $j_3$ . The prime conditions imply that $\mathcal {S}$ contains $(3,\dots ,3)$ , a contradiction. This completes the proof of the claim.

With the claim on board we now set about finishing Case (I) by induction. The base case is $n=2$ .

Base case: We can split into the subcases provided by the claim ( $\mathcal {S}$ is contained either in the first row, the second row, the first column, or the second column). Suppose for simplicity’s sake that $\mathcal {S}$ is contained in the first row. There are only so many sets contained in the first row:

1. (i) $\mathcal {S}$ is the first row. Let $A^\star $ be $0=0$ and $B^\star $ be $\tau $ .

2. (ii) $\mathcal {S}$ contains just the leftmost and the rightmost elements of the first row. Let $A^\star $ be $0=0$ and $B^\star $ be $ \gamma $ .

3. (iii) $\mathcal {S}$ contains the two rightmost elements of the first row. Let $A^\star $ be $0=0$ and $B^\star $ be $\neg \gamma $ .

4. (iv) $\mathcal {S}$ is just the leftmost element. Let $A^\star $ be 0=0 and $B^\star $ be 0=0.

5. (v) $\mathcal {S}$ is just the middle element. Let $A^\star $ be 0=0 and $B^\star $ be 0=1.

6. (vi) $\mathcal {S}$ is just the rightmost element. Let $A^\star $ be 0=0 and $B^\star $ be $\lambda $ .

By the prime conditions, $\mathcal {S}$ cannot contain just the two leftmost elements of the first row, so these cases are exhaustive.

The reasoning is similar if $\mathcal {S}$ is contained in the second row, first column, or second column. We leave these cases to the reader.

Induction step: Assume the induction hypothesis: For any $\mathcal {S}\subseteq [3]^n$ meeting the prime conditions, there is an appropriate realization $\star $ . Now let $\mathcal {T}\subseteq [3]^{n+1}$ meet the prime conditions. By Claim 1, $\mathcal {T}$ is contained in the ith layer of the jth slice. The key observation is that the ith layer of the jth slice is a $3^{n}$ tensor. More precisely, the jth conjunct is the same in all the entries in $j_i$ , so ignoring this conjunct in all entries yields a $3^{n}$ tensor $\mathcal {T}\restriction [3]^n$ . Apply the induction hypothesis to get an $\mathcal {L}_T$ realization $\star $ such that

$$ \begin{align*}\mathbf{FIX} \Vdash_{V^\star} \bigwedge \{\lozenge \varphi \mid \varphi\in \mathcal{T}\restriction [3]^n\} \wedge \bigwedge \{\neg\lozenge \varphi \mid \varphi \notin \mathcal{T}\restriction [3]^n\}.\end{align*} $$

To extend $\star $ to a realization $\sharp $ for $\mathcal {T}$ , just let

$$ \begin{align*}x_j^\sharp= \begin{cases} 0=0 & \text{ if }i = 1 \\ 0=1 & \text{ if } i =2 \\ \lambda & \text{ if } i=3. \end{cases}\end{align*} $$

Case (II): Assume that $(3,\dots ,3)\in \mathcal {S}$ . We must define sentences $A^1,\dots ,A^n$ . Pick some k such that $2^k>3^n$ . Take a set $\{\tau _1,\dots ,\tau _k\}$ of independent truth-tellers (see Remark 2.2). There are $2^k$ -many formulas of the form:

$$ \begin{align*}^{+}_{\neg} \tau_1 \wedge \dots \wedge ^{+}_{\neg} \tau_k.\end{align*} $$

Fix some enumeration $C_1,\dots ,C_{2^k}$ of these formulas. We then define the formulas $A^1_1,\dots ,A^1_{3^n},\dots ,A^n_1,\dots ,A^n_{3^n}$ so that $A^i_j$ is a conditional of the form $C_j\to \theta $ where $\theta \in \{0=0,0=1,\lambda \}$ .

More precisely, we proceed as follows. We fix a numbering $\Phi $ of the cells in the $3^n$ tensor. Then $\Phi (j)$ is some formula $\varphi _1(x_1)\wedge \dots \wedge \varphi _n(x_n)$ . Let $\Phi (j)_i$ be the ith conjunct of $\Phi (j)$ . We then define

$$ \begin{align*}A^i_j= C_j \to \begin{cases} 0=0 & \text{ if }\Phi(j)_i = T(x_i) \\ 0=1 & \text{ if }\Phi(j)_i = F(x_i) \\ \lambda & \text{ if }\Phi(j)_i = N(x_i). \end{cases}\end{align*} $$

We define $\mathcal {S}^\Phi :=\{k \leq 3^n\mid \Phi (k)\in \mathcal {S}\}$ .

We define $A^i$ as follows:

$$ \begin{align*}A^i\equiv \bigwedge \{A^i_j \mid j \in \mathcal{S}^\Phi\}\wedge \bigwedge \{C_j\to \lambda \mid j\in \{1,\dots,2^k\}-\mathcal{S}^\Phi\}.\end{align*} $$

Let $\star $ be a variable assignment such that $x_i^\star =A^i$ for each $i\leq n$ .

Claim 2. If $\varphi \in \mathcal {S}$ , then $\mathbf {FIX}\Vdash _{V^\star }\lozenge \varphi $ .

Proof. Suppose that $\varphi \in \mathcal {S}$ . Note that $\varphi $ is a conjunction of the form $\varphi _1(x_1)\wedge \dots \wedge \varphi _n(x_n)$ . Note also that $\Phi ^{-1}(\varphi )$ is some number $k\leq 3^n$ (by $\Phi ^{-1}$ I mean the inverse of $\Phi $ ; so $\Phi ^{-1}(\varphi )$ is just the number that $\Phi $ maps to $\varphi $ ). Since $C_k$ is a Boolean statement about independent truth-tellers, there is some w such that $\mathbb {N},w\vDash _{\mathsf {K3}} C_k$ (see Remark 2.2).

Let $i\leq n$ . Note that $A^i_k$ is a conditional of the form $C_k\to \theta $ .

$A^i$ is a conjunction of conditionals with antecedent $C_j$ such that for $j\neq k$ , . Which is to say that for all conjuncts $A^i_j$ of $A^i$ except for $A^i_k$ , $\mathbb {N},w\vDash _{\mathsf {K3}} A^i_j$ . Thus, $\mathbb {N},w\vDash _{\mathsf {K3}}A^i\Leftrightarrow \mathbb {N},w\vDash _{\mathsf {K3}} A^i_k$ . Since $\mathbb {N},w\vDash _{\mathsf {K3}} C_k$ , we infer that $\mathbb {N},w\vDash _{\mathsf {K3}}A^i\Leftrightarrow \mathbb {N},w\vDash _{\mathsf {K3}}\theta $ .

We now want to prove that $\mathbf {FIX},w\Vdash _{V^\star }\varphi _i$ , where $\varphi _i$ is the ith conjunct of $\varphi $ . Let’s break into cases depending on which formula $\varphi _i$ is.

Case 1: Suppose $\varphi _i$ is $T(x_i)$ , i.e., $\varphi $ is in the first layer of the ith slice. Since $k = \Phi ^{-1}(\varphi )$ , $\Phi (j)_i =T(x_i)$ . So, $\theta $ is $0=0$ . So $\mathbb {N},w\vDash _{\mathsf {K3}} A^i$ . So $\mathbb {N},w\vDash _{\mathsf {K3}} \mathsf {True}(\ulcorner A^i\urcorner )$ . Since $x_i^\star =A^i$ , $\mathbf {FIX},w\Vdash _{V^\star } T(x_i)$ .

Case 2: Suppose $\varphi _i$ is $F(x_i)$ , i.e., $\varphi $ is in the second layer of the ith slice. Since $k = \Phi ^{-1}(\varphi )$ , $\Phi (j)_i =F(x_i)$ . So, $\theta $ is $0=1$ . So . So $\mathbb {N},w\vDash _{\mathsf {K3}} \mathsf {True}(\ulcorner \neg A^i\urcorner )$ . Since $x_i^\star =A^i$ , $\mathbf {FIX},w\Vdash _{V^\star } F(x_i)$ .

Case 3: Suppose $\varphi _i$ is $N(x_i)$ , i.e., $\varphi $ is in the third layer of the ith slice. Since $k = \Phi ^{-1}(\varphi )$ , $\Phi (j)_i =N(x_i)$ . So, $\theta $ is $\lambda $ . So $\mathbb {N},w\uparrow _{\mathsf {K3}} A^i$ . So $\mathbb {N},w\nvDash _{\mathsf {K3}} \mathsf {True}(\ulcorner A^i\urcorner )$ and $\mathbb {N},w\nvDash _{\mathsf {K3}} \mathsf {True}(\ulcorner \neg A^i\urcorner )$ . Since $x_i^\star =A^i$ , $\mathbf {FIX},w\Vdash _{V^\star } N(x_i)$ .

So $\mathbf {FIX},w\Vdash _{V^\star }\varphi $ . So for all $v\in \mathbf {FIX}$ , $\mathbf {FIX},v\Vdash _{V^\star }\lozenge \varphi $ . That is, $\mathbf {FIX}\Vdash _{V^\star }\lozenge \varphi $ .

Claim 3. If $\varphi \notin \mathcal {S}$ , then $\mathbf {FIX}\nVdash _{V^\star }\lozenge \varphi $ .

Proof. We prove the contrapositive. Suppose $\mathbf {FIX}\Vdash _{V^\star } \lozenge \varphi $ . Then there is some w such that

$$ \begin{align*}(\triangle) \quad \mathbf{FIX},w\Vdash_{V^\star} \varphi.\end{align*} $$

We now break into cases depending on whether any of the $C_s$ is true at w.

Case 1: Suppose $\mathbb {N},w\uparrow _{\mathsf {K3}} C_s$ for all $s\leq 2^k$ . We claim that $A^1,\dots ,A^n$ all have value neither in w.

To see this, note that $A^i$ is a conjunction of conditionals each of which has an antecedent $C_s$ , which has value neither. A conditional with a neither antecedent cannot be false, so $A^i$ cannot be false. $A_i$ is true only if all its conjuncts are true. Since $2^k>3^n\geq |\mathcal {S}^\Phi |$ , there is some $j\leq 2^k$ such that $j\notin \mathcal {S}^\Phi $ . But then by definition of $A^i$ , $C_j\to \lambda $ is a conjunct of $A^i$ , and this has value neither.

So $\varphi $ is the formula $N(x_1)\wedge \dots \wedge N(x_n)$ . Since we are working in Case (II), we have assumed that this formula belongs to $\mathcal {S}$ .

Case 2: Suppose $\mathbb {N},w\vDash _{\mathsf {K3}} C_s$ for exactly one s. We split into subcases depending on whether $s>3^n$ or $s\leq 3^n$ .

Subcase 2.1: Suppose $s>3^n$ . $A^i$ is a conjunction of conditionals of the form $C_j\to \theta ^A_i$ such that for $j\neq s$ , , whence $\mathbb {N},w\vDash _{\mathsf {K3}} A^i_j$ . Accordingly, $\mathbb {N},w\uparrow _{\mathsf {K3}}A^i\Leftrightarrow \mathbb {N},w\uparrow _{\mathsf {K3}}\theta $ , where $\theta $ is the consequent of $A^i_s$ . Since $s>3^n$ , $\theta $ is $\lambda $ . Hence, $\mathbb {N},w\uparrow _{\mathsf {K3}} A^i$ . Hence, $\mathbb {N},w\nVdash _{\mathsf {K3}} \mathsf {True}(\ulcorner A^i\urcorner )$ and $\mathbb {N},w\nVdash _{\mathsf {K3}} \mathsf {True}(\ulcorner \neg A^i\urcorner )$ . Since $x_i^\star =A^i$ , $\mathbf {FIX},w\Vdash _{V^\star } N(x_i)$ .

Thus, $\varphi $ is $N(x_1)\wedge \dots \wedge N(x_n)$ , i.e., (3, …, 3). Once again, since we are working in Case (II), we have assumed that this formula belongs to $\mathcal {S}$ .

Subcase 2.2: Suppose that $s\leq 3^n$ . As in the previous subcase, $\mathbb {N},w\vDash _{\mathsf {K3}}A^i_s \Leftrightarrow \mathbb {N},w\vDash _{\mathsf {K3}}\theta ,$ where $\theta $ is the consequent of $ A^i_s$ .

Now $A^i$ itself is a conjunction of conditionals which is defined to include $A^i_s$ if and only if $s\in \mathcal {S}^\Phi $ . Let’s split into subsubcases depending on whether $s\in \mathcal {S}^\Phi $ .

Subsubcase 2.2.1: Suppose $s\in \mathcal {S}^\Phi $ . Then $\mathbb {N},w\vDash _{\mathsf {K3}} A^i\Leftrightarrow \mathbb {N},w\vDash _{\mathsf {K3}}A^i_s$ , where $A^i_s$ is $C_s\to \theta $ .

Note that, by the definition of $A^i_s$ :

$$ \begin{align*}(\circledast) \quad \theta \text{ is } 0=0 \text{ just in case } \Phi(s)_i=T(x_i).\end{align*} $$

Since $\mathbb {N},w\vDash _{\mathsf {K3}}C_s$ , we infer that

$$ \begin{align*}(\boxminus) \quad \mathbb{N},w\vDash_{\mathsf{K3}} A^i\Leftrightarrow \mathbb{N},w\vDash_{\mathsf{K3}}\theta.\end{align*} $$

We reason as follows:

$$ \begin{align*} \varphi_i \text{ is }T(x_i) &\Longleftrightarrow \mathbf{FIX},w\Vdash_{V^\star}T(x_i) \text{ by }(\triangle).\\ &\Longleftrightarrow \mathbb{N},w\vDash_{\mathsf{K3}}A^i \text{ since } x_i^\star=A^i.\\ &\Longleftrightarrow \mathbb{N},w\vDash_{\mathsf{K3}} \theta \text{ by }(\boxminus). \\ &\Longleftrightarrow \theta \text{ is } 0=0 \text{ since }\theta\in\{0=0,0=1,\lambda \}.\\ &\Longleftrightarrow \Phi(s)_i = T(x_i) \text{ by }(\circledast). \end{align*} $$

Exactly analogous arguments deliver exactly analogous conclusions. Summarizing, we have

$$ \begin{align*} \varphi_i \text{ is }T(x_i) &\Longleftrightarrow \Phi(s)_i = T(x_i).\\ \varphi_i \text{ is }F(x_i) &\Longleftrightarrow \Phi(s)_i = F(x_i).\\ \varphi_i \text{ is }N(x_i) &\Longleftrightarrow \Phi(s)_i = N(x_i). \end{align*} $$

These equivalences show that $\varphi =\Phi (s)$ . It is the assumption of Subsubcase 2.2.1 that $s\in \mathcal {S}^\Phi $ , i.e., $\Phi (s)\in \mathcal {S}$ , so $\varphi \in \mathcal {S}$ , which is desired result.

Subsubcase 2.2.2: Suppose $s\notin \mathcal {S}^\Phi $ . Then $A^i_s$ is $C_s\to \lambda $ . So $\mathbb {N},w\uparrow _{\mathsf {K3}}A^i_s$ , whence $\mathbb {N},w\uparrow _{\mathsf {K3}}A^i$ . As before, we conclude that $\mathbf {FIX},w\Vdash _{V^\star } N(x_i)$ . So $\varphi $ is $N(x_1)\wedge \dots \wedge N(x_n)$ . By the assumption of Case (II), $\varphi \in \mathcal {S}$ .

This completes the proof of Claim 3.

Claims 2 and 3 jointly yield Case (II) of (1) implies (2). This completes the proof of Lemma 5.9.

5.5 Completeness

Combining Lemma 5.9 (the analysis of $\mathbf {FIX}$ -satisfiability in terms of the prime conditions) with Carnap’s normal form theorem (Theorem 4.9), yields a complete axiomatization of the modal theory of $\mathbf {FIX}$ .

Proof. The soundness direction is trivial. Let’s focus on completeness. Suppose that $ \mathbf {S5[Con, Ground, Min_n]}\nvdash \varphi $ . By the normal form theorem,

$$ \begin{align*}\mathbf{S5[Con, Ground, Min_n]}\vdash \neg \varphi \leftrightarrow (\psi_1\vee\dots\vee\psi_k),\end{align*} $$

where each $\psi _i$ is a disjunction of n-isolators. Since $\neg \varphi $ is consistent, at least one of the disjuncts $\psi _i$ is also consistent. It follows that $\psi _i$ meets the prime conditions. By Lemma 5.9, there is an $\mathcal {L}_T$ realization $\star $ such that

$$ \begin{align*}\mathbf{FIX} \Vdash_{V^\star}\psi_i.\end{align*} $$

Hence, we infer that $\mathbf {FIX} \nVdash \varphi .$

5.6 Counting definable relations

Lemma 5.9 yields an explicit characterization of the $\mathbf {FIX}$ -definable binary relations, namely, each $\mathbf {FIX}$ -definable binary relation is a disjunction of intensional 2-isolators. The following counting result follows from this characterization.

Proof. First we need to determine the number of intensional 2-isolators. By Lemma 5.9, this is to count the number of subsets of the $3\times 3$ matrix meeting the prime conditions.

There are $2^{3^2}$ subsets of the $3\times 3$ matrix in total. We must subtract those sets that do not meet the prime conditions:

1. (1) The empty set. Subtract 1.

2. (2) The number of sets that intersect the first two rows but not the third is $(2^3 -1)^2=49$ . Indeed, we must pick at least one element from the first row and at least one from the second and none from the third. The first row has three cells. Hence it has $2^3 -1=7$ non-empty subsets. Likewise for the second. So we must subtract $7^2=49$ total.

3. (3) The number of sets that intersect the first two columns but not the third is likewise $(2^3 -1)^2=49$ .

4. (4) We must add back in all those sets that violated both the rows condition and the columns condition. Note that if a set intersects the first two rows but not the third and the first two columns but not the third then it is a subset of the upper left $2\times 2$ square. Exactly $7$ of these sets intersects the first two rows and first two columns.

5. (5) The sets that intersect row 3 and column 3 but not (3,3). There are $2^2-1=3$ non-empty subsets of the first two slots of the third row. Multiply this by the $3$ ways of doing the same for the third column. Then multiply this with the number of ways of filling in the upper left $2\times 2$ square, which is $2^4=16$ . This makes for $3\times 3\times 16$ total.

Here is the calculation:

$$ \begin{align*}2^9 -1 - 49\times 2 + 7 - 3\times 3\times 16 = 276.\end{align*} $$

So there are $276$ intensional 2-isolators. The definable binary relations are exactly the disjunctions of intensional 2-isolators, so there are $2^{276}$ of them. This completes the proof.

How many $\mathbf {FIX}$ -definable n-ary relations are there? The following coarse estimate is immediate.

Clearly this interval is huge (and only grows as n grows). One could perhaps use the inclusion–exclusion principle to count exactly the number of $\mathbf {FIX}$ -definable n-ary relations, but it is not clear whether the resulting formula would be at all informative. Instead of focusing on the exact number, one could aim to find a more informative estimate, but we will not pursue this further in this paper.