  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}$.
