Unprovability of P = NP in PV

Let $f$ be a polynomial-time algorithm, viewed as a function symbol of $\mathsf{PV}$, and let

$$\varphi_{\mathsf{P} = \mathsf{NP}}(f):= \forall x\,\forall y\,[\psi_{\mathsf{SAT}}(x,y) \rightarrow \psi_{\mathsf{SAT}}(x,f(x))]$$

where $\psi_{\mathsf{SAT}}(x,y)$ expresses that $y$ satisfies the Boolean formula encoded by $x$. Unprovability conjecture. For no polynomial-time algorithm $f$ does theory $\mathsf{PV}$ prove the sentence $\varphi_{\mathsf{P} = \mathsf{NP}}(f)$. This is a formal weakening of the conjecture that $\mathsf{P} \neq \mathsf{NP}$: if $\mathsf{P} = \mathsf{NP}$, the equality should nevertheless not be provable using only polynomial-time concepts and reasoning. By standard conservation results, the claim is also equivalent to consistency of $\mathsf{PV}$ and $\mathsf{S}^1_2$ with $\mathsf{P} \neq \mathsf{NP}$ in the intended sense.