1: \begin{equation}\label{Hconsistency}

2: \mbox{\it for any finite sequence $S$ of formulas, $S$ is not a \pa-derivation of $\bot$,}\footnote{$\bot$ is a propositional constant for contradiction which in arithmetical context can be interpreted as the formula $(0\! = \! 1)$.}

3: \end{equation}

4: