SOL

Expressive power of second order logic

Second-order logic is more expressive than first-order logic. For example, if the domain is the set of all real numbers, one can assert in first-order logic the existence of an additive inverse of each real number by writing ∀x ∃y (x + y = 0) but one needs second-order logic to assert the least-upper-bound property for sets of real numbers, which states that every bounded, nonempty set of real numbers has a supremum. If the domain is the set of all real numbers, the following second-order sentence expresses the least upper bound property:

In second-order logic, it is possible to write formal sentences which say "the domain is finite" or "the domain is of countable cardinality." To say that the domain is finite, use the sentence that says that every injective function from the domain to itself is surjective. To say that the domain has countable cardinality, use the sentence that says that there is a bijection between every two infinite subsets of the domain. It follows from the upward Löwenheim–Skolem theorem that it is not possible to characterize finiteness or countability in first-order logic.