formalized provability predicate and implication relation

Question

$\DeclareMathOperator{\pvbl}{pvbl}$ Let $\pvbl$ be the formalized provability predicate.

Sentences $A$, $B$, $C$, $D$ have the following relation.

$\pvbl ( A \rightarrow B)$

$\pvbl ( C \rightarrow D)$

Then, under this situation, is the following correct?

$\pvbl ( (A \land C ) \rightarrow (B \land D))$

Answer 1

This is something that follows from Löb's conditions (as described on http://plato.stanford.edu/entries/logic-provability/).

$(A \rightarrow B) \rightarrow (C \rightarrow D) \rightarrow ((A \wedge C) \rightarrow (B \wedge D))$ is a theorem of propositional logic, and so $\mathrm{pvbl}((A \rightarrow B) \rightarrow (C \rightarrow D) \rightarrow ((A \wedge C) \rightarrow (B \wedge D)))$ is provable by the first condition. This implies that $\mathrm{pvbl}(A \rightarrow B) \rightarrow \mathrm{pvbl}(C \rightarrow D) \rightarrow \mathrm{pvbl}((A \wedge C) \rightarrow (B \wedge D))$ is provable, by the second condition. Therefore, if $\mathrm{pvbl}(A \rightarrow B)$ and $\mathrm{pvbl}(C \rightarrow D)$ hold, $\mathrm{pvbl}((A \wedge C) \rightarrow (B \wedge D))$ must also hold.

Answer 2

Zhen Lin's comment says it very clearly: if the proof system is reasonable (and the provability predicate is correct), then that conclusion should be correct. If you needed to prove it, you should probably look for lemmata of the form

\begin{gather} \mathit{pvbl}(\phi \land \psi) \to (\mathit{pvbl}(\phi) \land \mathit{pvbl}(\psi) ) \tag{$\land$E} \\ (\mathit{pvbl}(\phi) \land \mathit{pvbl}(\psi)) \to \mathit{pvbl}(\phi \land \psi) \tag{$\land$I} \\ (\mathit{pvbl}(\phi) \land \mathit{pvbl}(\phi \to \psi)) \to \mathit{pvbl}(\psi) \tag{$\to$E} \\ (\mathit{pvbl}(\phi) \to \mathit{pvbl}(\psi)) \to \mathit{pvbl}(\phi \to \psi)) \tag{$\to$I} \\ \end{gather}

Then you could actually start from the assumptions $\mathit{pvbl}(A \to B)$ and $\mathit{pvbl}(C \to D)$ and prove $\mathit{pvbl}((A \land C) \to (B \land D))$.