In arXiv:1811.04313, a definition of determinant is formalized in the bounded arithmetic $VNC^{2}$. Following the presentation of [Gathen, 1993], we can formalize a definition of matrix rank in the same bounded arithmetic. In this article, we define a bounded arithmetic $LAPPD$, and show that $LAPPD$ seems to be a natural arithmetic theory formalizing the treatment of rank function following Mulmuley's algorithm. Furthermore, we give a formalization of rank in $VNC^{2}$ by interpreting $LAPPD$ by $VNC^{2}$.

翻译：在arXiv:1811.04313中，行列式的定义在有界算术$VNC^{2}$中被形式化。遵循[Gathen, 1993]的表述，我们可以在同一有界算术中形式化矩阵秩的定义。本文定义了一个有界算术$LAPPD$，并表明$LAPPD$似乎是按照穆尔穆莱算法处理秩函数的自然算术理论。此外，我们通过将$LAPPD$解释为$VNC^{2}$，在$VNC^{2}$中给出了秩的形式化。