An informal definition of a logical truth is a sentence that's true in virtue of its form alone: $\phi$ is logically true iff all substitutions of $\phi$ that leave its logical vocabulary alone are true.

We might try to formulate a version of this idea in modal logic. Let $\mathcal{L}$ be a modal language, and let $v: \mathcal{L} \to \{0,1\}$ be a Boolean valuation (i.e. $v(A\wedge B) = min(v(A),v(B))$ and $v(\neg A)=1-v(A)$). Say that $v$ is proper if it additionally satisfies the constraint:

  • $v(\Box A)=1$ if and only if $v(iA)=1$ for every substitution $i$

here we represent a substitution, $i$, as a function from letters to arbitrary sentences and write $iA$ for the result of applying that substitution to $A$. (If $S$ is a restricted set of substitutions, say that $v$ is an $S$-valuation if the corresponding biconditional with $i$ restricted to $S$ holds instead.)

This conception of modality validates some interesting principles: for example if $v(\Box A)=1$ then $v(iA)=1$ for every substitution $i$. In particular, for any given $j$, $v(i(jA)) =1$ for every $i$, since $i\circ j$ is also a substitution. So $v(\Box jA)=1$ for every $j$, and so $v(\Box\Box A)=1$. It follows that the S4 principle is true in every proper valuation. Indeed, one can show that every theorem of S4M is true in every proper valuation. (M is the McKinsey axiom, $\Box \Diamond A \to \Diamond \Box A$, and can be seen to be validated by considering substitutions that map letters to $\top$ and $\bot$.)

Note, however, that it's not obvious that there are any proper valuations. The bulleted claim is a constraint, not a definition, as it involves circularity. For example $v(\Box p) = 1$ iff $v(ip)$ is true for every $i$, and the circularity arises in cases where $ip =\Box p$. But the circularity is not vicious in this case, e.g. $v(\Box p)=0$ since $v(ip)=0$ when $ip= \bot$. I conjecture that the constraint is never vicious, and can always be satisfied. So I was wondering:

  • Are there any proper valuations?

I have some thoughts about constructing a valuation, but they haven't delivered anything so far. One useful fact to note is that if there is a proper valuation $v$, we can construct a Kripke model by letting $W$ be the set of substitutions, letting $i R (j\circ i)$ for all $i,j$, and letting $i \Vdash p$ iff $v(ip)=1$. Conversely, if there's a Kripke model on this frame satisfying $i \Vdash p$ iff $id\Vdash ip$ then we can construct a proper valuation by letting $v(\phi)=1$ iff $id\Vdash \phi$, where $id$ is the identity substitution. So this gives us another way of thinking about the problem. (There is also a topological reformulation of the problem, but I think that's enough for now.)

(Background: McKinsey talks about related notions of necessity here and investigates their logic. He constructs what I've called an $S$-valuation for a very restricted $S$. However, he doesn't seem to raise or recognize the issue with the unrestricted notion.)

  • 1
    $\begingroup$ I’m not sure whether a proper valuation exists, but: if something is vicious here, I don’t think it’s the circularity.. Second-order propositional logic has essentially the same circularity, and quite unproblematic semantics. Rather, the issue in your setup is the (lack of) treatment of bound variables: the semantics of $\Box \varphi$ quantifies over propositional variables in $\varphi$, but syntactically, $\Box$ doesn’t bind them. E.g. any proper valuation must have $v(\lnot \Box A) = \top$ (so one might think $\lnot \Box A$ was “logically true”) but also $v(\Box \lnot \Box A) = \bot$. $\endgroup$ – Peter LeFanu Lumsdaine Jan 16 '18 at 13:11
  • $\begingroup$ @PeterLeFanuLumsdaine If you understand the propositional quantifiers substitutionally, and you have propositional operators in the language, the constraints on truth are no-longer well-founded (and the circularity is potentially problematic, as demonstrated by things like Prior's paradox). It's not in general obvious that the unproblematic semantic interpretation of the propositional quantifiers corresponds to the substitutional interpretation: i.e. that $\forall p\phi$ is true in the semantic sense if and only if $\phi(A/p)$ is true for every sentence $A$. $\endgroup$ – Andrew Bacon Jan 16 '18 at 19:25
  • $\begingroup$ Ah, yes, my bad: I was overlooking that the interpretation of 2nd order prop. logic won’t give that “if and only if” when the quantification is restricted to sentences. $\endgroup$ – Peter LeFanu Lumsdaine Jan 16 '18 at 23:34

$\def\ml{\mathrm{ML}}\let\LOR\bigvee\let\ET\bigwedge$The question you asked is a variant of Problem 42 in Friedman [1]. It also has an intuitionistic analogue, Problem 41, which asks if there exists a set $V$ of propositional formulas such that

  • $A\land B\in V$ iff $A\in V$ and $B\in V$,

  • $A\lor B\in V$ iff $A\in V$ or $B\in V$,

  • $\bot\notin V$, and

  • $A\to B\in V$ iff for every substitution $\sigma$, if $\sigma(A)\in V$, then $\sigma(B)\in V$.

Under some mild extra assumptions (if $V$ is closed under substitution, or just contains the schema $A\to(B\to A)$), it is easy to see that $V$ satisfies Friedman’s conditions if and only if it is a structurally complete intermediate logic with the disjunction property.

Both problems were solved affirmatively by Prucnal [2]. Concerning Problem 41, Prucnal proved structural completeness of Medvedev’s logic of finite problems $\ml$, which means that $V=\ml$ satisfies Friedman’s conditions. In fact, $\ml$ is the largest structurally complete intermediate logic with the disjunction property. We do not know any other such logic, and it is quite possible that $\ml$ is the only solution.

The largest modal companion of Medvedev’s logic, $\sigma\ml$, gives a solution to Problem 42 (hence to the question here).

Let me now explain the connection in more detail. First, recall that a rule $A/B$ is admissible in a logic $L$ if for all substitutions $\sigma$, $\vdash_L\sigma(A)$ implies $\vdash_L\sigma(B)$; the rule is derivable in $L$ if $A\vdash_LB$. (In the case of normal modal logics, we take the global consequence relation as $\vdash_L$ here, so that $A\vdash_L\Box A$. Note that for $L\supseteq\mathrm{S4}$, we have the deduction theorem: $A\vdash_LB$ iff $\vdash_L\Box A\to B$ iff $\vdash_L\Box A\to\Box B$.)

A logic is structurally complete if all admissible rules are derivable.

A modal logic $L$ has the disjunction property if $${}\vdash_L\Box A_1\lor\dots\lor\Box A_k\implies{}\vdash_LA_1\text{ or }\dots\text{ or }{}\vdash_L A_k.$$ (As a special case, for $k=0$ this condition amounts to the consistency of $L$.)

Proposition: For any Boolean valuation $v$, the following are equivalent:

  1. $v$ is proper

  2. $L=\{A:v(\Box A)=1\}$ is a structurally complete normal modal logic extending S4 satisfying the disjunction property.


$1\to2$: That $L$ is a normal extension of S4 is easy to show, and has been already observed in the question. For the DP, if $v(\Box(\LOR_i\Box A_i))=1$, then also $v(\LOR_i\Box A_i)=1$, hence $v(\Box A_i)=1$ for some $i$.

Assume that the rule $A/B$ is $L$-admissible; we want to show $\Box A\to\Box B\in L$, i.e., $v(\Box\sigma(A)\to\Box\sigma(B))=1$ for every substitution $\sigma$. But this follows by definition: if $v(\Box\sigma(A))=1$, then $\sigma(A)\in L$, thus $\sigma(B)\in L$ by admissibility, thus $v(\Box\sigma(B))=1$.

$2\to1$: We need to show $$\vdash_LA\iff\forall\sigma\:v(\sigma(A))=1.$$ Left-to-right: since $L$ is closed under substitution, it suffices to show $v(A)=1$. By writing $A$ in CNF and considering each conjunct separately, we may assume $A$ has the form $$\ET_ip_i^{e_i}\land\ET_j\Box A_j\to\LOR_k\Box B_k,$$ where $p_i$ are propositional variables, $e_i\in\{0,1\}$, and we put $p^1=p$, $p^0=\neg p$. Assume $v(\ET_j\Box A_j)=1$. Then $L$ derives each $A_j$, hence also $\Box A_j$; since it also derives $A$, it must derive $$\ET_ip_i^{e_i}\to\LOR_k\Box B_k.$$ For any $\{0,1\}$ assignment $a$, let $\sigma_a$ be the substitution defined by $\sigma_a(p_i)=p_i^{a_i}$. It follows that $L$ derives $$\sigma_a\Bigl(\ET_ip_i^{e_i}\to\LOR_k\Box B_k\Bigr)$$ for each $a$, hence by combining them together, it derives $$\LOR_k\LOR_a\Box\sigma_a(B_k).$$ By the disjunction property, $L$ derives $\sigma_a(B_k)$ for some $k$ and $a$; but then $\vdash_LB_k$, as $\sigma_a$ is an involution. Thus, $v(\Box B_k)=1$ as needed.

Right-to-left: First, let us assume that $A$ is modalized, i.e., all occurrences of variables in $A$ are in the scope of some $\Box$. By considering the CNF, we may further assume it is of the form $$\ET_j\Box A_j\to\LOR_k\Box B_k.$$ Now, if $v(\sigma(A))=1$ for every $\sigma$, then the rule $\ET_jA_j/\LOR_k\Box B_k$ is admissible: for any $\sigma$, if $\ET_j\sigma(A_j)\in L$, then $v(\sigma(\ET_j\Box A_j))=1$, thus $v(\sigma(\LOR_k\Box B_k))=1$, thus $v(\Box\sigma(B_k))=1$ for some $k$, thus $\sigma(B_k)\in L$, thus $\LOR_k\Box\sigma(B_k)\in L$. By structural completeness, $\vdash_L\ET_j\Box A_j\to\LOR_k\Box B_k$, i.e., $\vdash_L A$.

I don’t have an elementary argument for the case when $A$ is not necessarily modalized, but it can be handled as follows. Let $L'=\{A:\forall\sigma\:v(\sigma (A))=1\}$. Then $L'$ is a quasi-normal extension of $L$. Using the machinery of Zakharyaschev’s canonical formulas (see e.g. [3]), one can show that $L'$ can be axiomatized (as a quasinormal logic) over S4 by modalized formulas. Since each of them is derivable in $L$ by the previous part of the proof, $L=L'$. QED

Now, it remains to show that structurally complete extensions of S4 with the disjunction property exist. As I already mentioned, let $\ml$ be Medvedev’s logic: it is defined semantically as the logic of the finite intuitionistic frames $M_n=\langle\mathcal P([n])\smallsetminus\{[n]\},{\subseteq}\rangle$ for $n\in\mathbb N$ (i.e., $M_n$ is the $n$-dimensional Boolean cube without its top element). $\ml$ is easy seen to have the disjunction property, and as proved by Prucnal, it is structurally complete.

Let $\sigma\ml$ be the largest modal companion of $\ml$. Note that $\sigma\ml$ is the logic of $\{M_n:n\in\mathbb N\}$ considered as modal frames. Since largest modal companions preserve the disjunction property (easy) and structural completeness (see Rybakov [4,Thm. 5.4.7]), $\sigma\ml$ has all the required properties:

Proposition: A structurally complete normal modal logic extending S4 with the disjunction property exists. Thus, proper valuations exist.

Note by the way that it is a long-standing open problem if $\ml$ (and $\sigma\ml$, for that matter) is decidable, or equivalently, recursively axiomatizable. (The semantic definition only guarantees it is co-r.e.)


[1] Harvey Friedman, One hundred and two problems in mathematical logic, Journal of Symbolic Logic 40 (1975), no. 2, pp. 113–129, doi: 10.2307/2271891.

[2] Tadeusz Prucnal, On two problems of Harvey Friedman, Studia Logica 38 (1979), no. 3, pp. 247–262, doi: 10.1007/BF00405383.

[3] Alexander Chagrov and Michael Zakharyaschev, Modal logic, Oxford Logic Guides vol. 35, Oxford University Press, 1997.

[4] Vladimir Rybakov, Admissibility of logical inference rules, Studies in Logic and the Foundations of Mathematics vol. 136, Elsevier, 1997.

  • $\begingroup$ Wonderful! And thanks for the references, I will check those out later. Do you have a reference for the disjunction property for $\sigma ML$? (It wasn't jumping out to me as obvious: My strategy was to glue together an $M_i$ that falsified $\Box A$ and $M_j$ that falsified $\Box B$ to get something that falsified the disjunction, and show that it was bisimilar (or otherwise equivalent) to some $M_k$, but that's quite fiddly.) $\endgroup$ – Andrew Bacon Jan 17 '18 at 1:34
  • 1
    $\begingroup$ IIRC The argument for ML is given in Chagrov&Zakharyaschev; for $\sigma\ml$ it's essentially the same. The point is that $M_n$ and $M_m$ embed as disjoint generated subframes in $M_{n+m}$; unlike the usual "gluing" construction, the frame will contain various extra points besides the root and the two original frames, but this does not matter for the disjunction property. The gluing of $M_n$ and $M_m$ as such in general does not validate ML (or $\sigma\ml$): if it did, then Visser rules would be admissible in ML, hence derivable, hence the logic would have width at most $2$, quod non. $\endgroup$ – Emil Jeřábek Jan 17 '18 at 9:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.