Introduction:
- 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.
- Example SOL Expression:
- (∃T)(∀Q)(∀D)(∃A)((T⊂ Q) ∧ (A, D∈T) ∧ ((C(x,y) ∧ ¬D) → ((A ∧ E(t,z)) ∨ F)))
- 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 (3rd, 4th, 5th, 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.