Second-order logic over finite structures

Aggregates the second-order logic modules (currently syntax; semantics and isomorphism-invariance to follow), the machinery for Fagin's theorem NP = ∃SO on roadmap track L6.