$\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.