Practically all of mathematics can be formalized in Coq. One notable exception is the internal consistency of Coq itself (due to Gödel's first incompleteness theorem, I believe).
Coq's logic is intuitionistic, which means it's impossible to prove the following: forall P, P or ~P. But this actually makes Coq more powerful than classical logic, not less, because:
a) If you want, you can add that proposition (called the law of the excluded middle) as an axiom. Now you have classical logic.
b) By not adding that axiom, you can show that certain results do not depend on it. You couldn't do this if it were built-in.
Coq's logic is intuitionistic, which means it's impossible to prove the following: forall P, P or ~P. But this actually makes Coq more powerful than classical logic, not less, because:
a) If you want, you can add that proposition (called the law of the excluded middle) as an axiom. Now you have classical logic.
b) By not adding that axiom, you can show that certain results do not depend on it. You couldn't do this if it were built-in.