Can coq express its own metatheory?
It is possible to formalize Coq's logic within Coq but only subsets of the logic have been formalized yet. Relevant contributions are CoqInCoq, PTS, PTSATR, and PTSF.