\(\sc{PROOF}\ \sc{CHECKING}_{\mathsf{T}}\ \)  Given a formula \(\phi\) in the language of \(\mathsf{T}\) and a finite object \(\mathcal{D}\) of the appropriate sort (e.g. a derivation sequence or tree), is \(\mathcal{D}\) a well-formed proof of \(\phi\) from the axioms of \(\mathsf{T}\)?[37]