Second-Order Logic extends First-Order Logic to Quantify Sets. Whereas first-order logic may only quantify Variables in a domain of discourse (set), Second-Order logic may also quantify of sets themselves.

This is read there exists a set T, for all sets Q, for all D, there exists an A, such that set T is a proper subset of a set from Q, and A and D are elements of set T, and C and not D, implies A and E or F.

Second-Order Logics is even MORE expressive. This can be used to build even MORE extensive complex models of the domains of discourse.

Note: Higher-order logics (3^{rd}, 4^{th}, 5^{th}, etc.) extend the quantification operators to quantifications over quantifications over quantifications…this is analogous to types of types of types… in type-theory. Hence the connection to programming languages types.