Using FOL to Describe the Properties of Systems

Limitations

Although first-order logic is sufficient for formalizing much of mathematics and is commonly used in computer science and other fields, it has certain limitations. These include limitations on its expressiveness and limitations of the fragments of natural languages that it can describe.

For instance, first-order logic is undecidable, meaning a sound, complete and terminating decision algorithm for provability is impossible. This has led to the study of interesting decidable fragments, such as C₂: first-order logic with two variables and the counting quantifiers $\exists ^{\geq n}$ and $\exists ^{\leq n}$ .

Expressiveness

The Löwenheim–Skolem theorem shows that if a first-order theory has any infinite model, then it has infinite models of every cardinality. In particular, no first-order theory with an infinite model can be categorical. Thus, there is no first-order theory whose only model has the set of natural numbers as its domain, or whose only model has the set of real numbers as its domain. Many extensions of first-order logic, including infinitary logics and higher-order logics, are more expressive in the sense that they do permit categorical axiomatizations of the natural numbers or real numbers. This expressiveness comes at a metalogical cost, however: by Lindström's theorem, the compactness theorem and the downward Löwenheim–Skolem theorem cannot hold in any logic stronger than first-order.

Formalizing natural languages

First-order logic is able to formalize many simple quantifier constructions in natural language, such as "every person who lives in Perth lives in Australia". Hence, first-order logic is used as a basis for knowledge representation languages, such as FO(.).

Still, there are complicated features of natural language that cannot be expressed in first-order logic. "Any logical system which is appropriate as an instrument for the analysis of natural language needs a much richer structure than first-order predicate logic".

Type	Example	Comment
Quantification over properties	If John is self-satisfied, then there is at least one thing he has in common with Peter.	Example requires a quantifier over predicates, which cannot be implemented in single-sorted first-order logic: Zj → ∃X(Xj∧Xp).
Quantification over properties	Santa Claus has all the attributes of a sadist.	Example requires quantifiers over predicates, which cannot be implemented in single-sorted first-order logic: ∀X(∀x(Sx → Xx) → Xs).
Predicate adverbial	John is walking quickly.	Example cannot be analysed as Wj ∧ Qj; predicate adverbials are not the same kind of thing as second-order predicates such as colour.
Relative adjective	Jumbo is a small elephant.	Example cannot be analysed as Sj ∧ Ej; predicate adjectives are not the same kind of thing as second-order predicates such as colour.
Predicate adverbial modifier	John is walking very quickly.	—
Relative adjective modifier	Jumbo is terribly small.	An expression such as "terribly", when applied to a relative adjective such as "small", results in a new composite relative adjective "terribly small".
Prepositions	Mary is sitting next to John.	The preposition "next to" when applied to "John" results in the predicate adverbial "next to John".