We study various formulations of the completeness of first-order logic phrased in constructive type theory and formalised in the Coq proof assistant. Specifically, we examine the completeness of variants of natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game semantics. As completeness with respect to standard model-theoretic semantics is not readily constructive, we analyse the assumptions necessary for particular syntax fragments and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.
Note that there is a more recent extended version of this paper.