Completeness of the Q0 Higher-Order Logic

We formalize the completeness of Peter B. Andrews' system \( Q_0 \), an implementation of Higher-Order Logic (also called simple type theory), following his textbook An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Our work builds on Díaz's formalization of \( Q_0 \)'s syntax, semantics, soundness and consistency. The completeness is with respect to general models. We prove completeness by introducing an abstract consistency property for \( Q_0 \) using the framework for abstract consistency properties by From and Schlichtkrull to get a model existence theorem for \( Q_0 \). We adapt proofs from Andrews' book to this context.