What is the simplest formal language $L$ such that if a particular Turing machine $M_i$ halts, then there exists a finite formula $F$ in $L$ such that $F$ is a complete proof that $M_i$ halts (for clarity, we assume that $F$ is required to include the complete description of $M_i$)?
I think that the first part of $F$ is assumed to contain the complete description of $M_i$ and the second part of $F$ is assumed to contain the computation history of $M_i$. But what is an example of $L$ that allows to write such formulas (assuming that I want $L$ to be as simple as possible)?