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](https://www.jstor.org/stable/2267027) 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.)



Substitutional modality
$\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](https://en.wikipedia.org/wiki/Admissible_rule) [intermediate logic](https://en.wikipedia.org/wiki/Intermediate_logic) with the [disjunction property](https://en.wikipedia.org/wiki/Disjunction_and_existence_properties).


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](https://en.wikipedia.org/wiki/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.
> 
> 
> 


**Proof:**


$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](https://en.wikipedia.org/wiki/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.)


**References:**


[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](https://doi.org/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](https://doi.org/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.


