 Since Fagin’s Theorem (Fagin 1974) shows that a property of finite models is definable in \(\Sigma_1^1\) if and only if it is recognizable in polynomial time by a nondeterministic Turing machine (that is, if and only if it is in NPTIME), it follows at once that