Do good PCPs for NP give us good PCPs for the entire polynomial hierarchy?
The truth of a statement is different from it having a (short) proof in a proof system. The language is expressive but it doesn't mean that all valid statements in the language have short proofs in the system.

The theorem doesn't say that you can check the truth of a statement or even the correctness of an arbitrary long proof or of arbitrary theorems. It is for proofs of membership in an $\mathsf{NP}$ set, which by definition have polynomial size proofs (certificates) of membership. The theorem only says that you don't need to read the full (polynomial size) proof of membership in an $\mathsf{NP}$ set to decide its correctness.

One implication of the theorem is applying it to the set of theorems in an arbitrary language which have short (i.e. an arbitrary polynomial) proofs in an efficient proof system (i.e. it is decidable in polynomial time if a given string is a proof of a given statement). For example, theorems of ZFC which have proofs of size $n^{100}$ where $n$ is the size of the formula. If the proof system is sound then you can probabilistically verify the correctness of the theorems which have short proofs with reading a small part of their proofs. I think this is the intend meaning of the informal statement "proofs written up in strict mathematical language can be checked efficiently to any desired degree of accuracy without the requirement of reading the entire proof".