  This paper proves that a plactic monoid of any finite rank will have
decidable first order theory. This resolves other open decidability problems
about the finite rank plactic monoids, such as the Diophantine problem and
identity checking. This is achieved by interpreting a plactic monoid of
arbitrary rank in Presburger arithmetic, which is known to have decidable first
order theory. We also prove that the interpretation of the plactic monoids into
Presburger Arithmetic is in fact a bi-interpretation, hence any two plactic
monoids of finite rank are bi-interpretable with one another. The algorithm
generating the interpretations is uniform, which answers positively the
decidability of the Diophantine problem for the infinite rank plactic monoid.
