 (D1) is simply a restatement of the requirement from the proof of the first theorem that provability is weakly representable. Roughly put, (D2) requires that the whole demonstration of (D1), for the candidate provability predicate \(\Prov_F\), can itself be formalized inside \(F\). Finally, (D3) requires that the provability predicate is closed under Modus Ponens.