**The setup:** Given a formula $\varphi$ of intuitionistic propositional logic (i.e., made from the connectors $\Rightarrow$, $\land$, $\lor$, $\top$ and $\bot$ from propositional variables $A,B,C,\ldots$), by replacing the logical connectors $\Rightarrow$, $\land$, $\lor$, $\top$ and $\bot$ by $\mathop{\mathrm{Hom}}(—,—)$ (set of functions), $\times$ (cartesian product), $+$ (disjoint sum), $1$ (singleton set) and $0$ (empty set) respectively, we define a map $\hat\varphi$ from the class of $r$-tuples of finite sets, where $r$ is the number of free variables of $\varphi$ (or more precisely, from mappings of the free variables of $\varphi$ to finite sets), to finite sets.  In more fancy terms, I think I'm supposed to say that $\hat\varphi$ is obtained by the Curry-Howard-Lambek correspondence applied to $\varphi$ for the bicartesian closed category of finite sets.

For example, if $\varphi$ is $\neg A \lor \neg\neg A$ (where $\neg P$ is an abbreviation for $P\Rightarrow \bot$), then $\hat\varphi(A) = \mathop{\mathrm{Hom}}(A,0) + \mathop{\mathrm{Hom}}(\mathop{\mathrm{Hom}}(A,0),0)$ is a singleton for every finite set $A$ (N.B.: the ambient set theory is classical).

*Observation:* if $\varphi$ is provable intutionistically, then $\hat\varphi$ is inhabited (i.e., nonempty) for every value of its arguments.  The above example shows that the converse is not true.

Now define each variable occurrence in $\varphi$ to be either *positive* (=covariant) or *negative* (=contravariant): a variable alone is positive, the occurrences in $P\land Q$ and $P\lor Q$ have the same variance as in $P$ and $Q$, but for $P\Rightarrow Q$ the occurrences in $Q$ are the same whereas those in $P$ are flipped (I hope this is clear enough and standard anyway; for example in $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$, the only occurrence of $B$ is positive, the two first occurrences of $A$ are negative and the last is positive).

Say that $\varphi$ has **consistent variance** when each variable occurs either always positively or always negatively (so $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$ does not have consistent variance, but $(A\Rightarrow B)\Rightarrow A$ does; we agree that if a formula has no variable, it has consistent variance); also say that $\varphi,\psi$ jointly have consistent variance when $\varphi\land\psi$ has consistent variance.

Now when $\varphi$ has consistent variance, $\hat\varphi$ is not just a map of classes from $\mathbf{FinSet}^r$ to $\mathbf{FinSet}$, it's a *functor* (covariant or contravariant in each variable according to that variable's variance in $\varphi$).

Furthermore, if $\varphi,\psi$ jointly have consistent variance, and if $\psi\Rightarrow\varphi$ is provable intuitionistically (note that this generally does not have consistent variance), we get a natural transformation from $\hat\psi$ to $\hat\varphi$ from the proof (this follows from general nonsense, but it's easy to see by examining the proof rules).

**QUESTION:** Is the converse of this statement true?  That is, if $\varphi,\psi$ jointly have consistent variance and if there is a natural transformation $\hat\psi \to \hat\varphi$, is $\psi\Rightarrow\varphi$ provable?

(For example, a positive answer to the question would let us say “there is no natural transformation from $\mathop{\mathrm{Hom}}(\mathop{\mathrm{Hom}}(A,B),A)$ to $A$ because Peirce's law $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$ is not provable intuitionistically”.)

I would be surprised if this isn't a well-known construction in categorical logic, but I don't know the terminology well enough to search for it.

Note that I'm asking the question with finite sets because I thought it would be better behaved, but if you wish to remove “finite” throughout, be my guest.  Finiteness isn't the real issue here: functoriality is.

----

**Additional remarks** (2023-12-12):

* To dispel a possible confusion, the functor construction defined here is *not* (or at least, not *obviously*!) the set construction applied in the topos of covariant functors (=presheaves on the opposite category) $\mathbf{FinSet}^{\lbrace\mathit{variables}\rbrace} \to \mathbf{Set}$ (with each variable interpreted as the corresponding coordinate): in the latter, the $\mathrm{Hom}$ is an internal hom between covariant functors so it always returns a covariant functor in all variables, whereas in this question's interpretation, $\mathrm{Hom}$ is simply the functor of morphisms in $\mathbf{Set}$, so it is contravariant in the first variable (hence the variance restriction on the formula).

* The construction here is also not the same as Medvedev's “logic of finite problems” (for a definition of which see, e.g., §3 of [this survey by Plisko](https://www.jstor.org/stable/25470303) on a different subject).  The main difference is that Medvedev logic only demands uniformity in varying the “solution sets” of the variables, whereas here full functoriality is demanded (at the expense of requiring consistent variance on the formula).

* I maybe should have mentioned that propositions (resp. proofs, modulo some equivalence relation that doesn't matter here) in intuitionistic logic form the objects (resp. arrows) in the free bicartersian closed category over the given set of variables: see [this paper by Fiore, Di Cosmo and Balat](https://www.sciencedirect.com/science/article/pii/S0168007205001272) for a definition of the latter, with some connections to this question.  So the question can be phrased in a purely categorical way, without any references to logic.  But I haven't been able to use this line of thought usefully to actually answering it.