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$似乎是遵循Mulmuley算法形式化秩函数处理的自然算术理论。此外，我们通过在$VNC^{2}$中解释$LAPPD$，给出了秩在$VNC^{2}$中的形式化。