Substitutional modality 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.)
 A: $\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:

*

*$v$ is proper


*$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 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.
[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.
