I think it would be a good idea to make a list of theorems stating that P does not equal NP if and only if such and such exits, some complexity class is contained in another complexity class and so on and so forth.
Here is a result from descriptive complexity theory:
$P \ne NP$ if and only if some second order property is not expressible using first order logic plus least fixed point.
Reference: Immerman, Languages that capture complexity classes
Ladner theorem can be stated as:
$P \ne NP$ if and only if there exists an incomplete set in $NP-P$.
Incomplete set is a set that is not complete for $NP$ under many-one polynomial time reductions.
Complexity Theory and Cryptology: An Introduction to Cryptocomplexity By Jörg Rothe, page 106