Editing First-order logic (section)

==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<sub>2</sub>: first-order logic with two variables and the [[counting quantifiers]] <math>\exists^{\ge n}</math> and <math>\exists^{\le n}</math>.<ref>{{cite web|last=Horrocks|first=Ian|authorlink=Ian Horrocks|year=2010|title=Description Logic: A Formal Foundation for Languages and Tools|url=https://www.cs.ox.ac.uk/ian.horrocks/Seminars/download/semtech-tutorial-pt1.pdf |archive-url=https://web.archive.org/web/20150906135046/http://www.cs.ox.ac.uk/ian.horrocks/Seminars/download/semtech-tutorial-pt1.pdf |archive-date=2015-09-06 |url-status=live|at=Slide 22}}</ref>

===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 [[Morley's categoricity theorem|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{{clarification needed|date=January 2023|reason=Article should clarify syntactic-semantic distinction here, e.g. second-order logic can be interpreted as a many-sorted first-order logic, so syntactically it could be argued that it's not more expressive, and it admits categorical axiomatizations only using full semantics, but using Henkin semantics it is a conservative extension of the typical semantics for first-order logic. So really the article needs to clarify whether it is discussing FOL exclusively as a syntactic system, or as a syntactic and semantic system, and in either case clarify in which senses "extensions" of first-order logic are being assumed to extend it (i.e. syntactically only or also semantically).}}. 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===
{{Main|Logic translation#Natural language formalization}}
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 language]]s, 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".{{sfn|Gamut |1991 |p=75}}

{| class="wikitable"
|-
! Type !! Example !! Comment
|-
! {{rh}} | {{nowrap|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: {{nowrap|{{mono|Zj → ∃X(Xj∧Xp)}}}}.
|-
! {{rh}} | 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: {{nowrap|{{mono|∀X(∀x(Sx → Xx) → Xs)}}}}.
|-
! {{rh}} | Predicate adverbial 
| John is walking quickly. || Example cannot be analysed as {{nowrap|{{mono|Wj ∧ Qj}}}};<br/>predicate adverbials are not the same kind of thing as second-order predicates such as colour.
|-
! {{rh}} | Relative adjective
| Jumbo is a small elephant. || Example cannot be analysed as {{nowrap|{{mono|Sj ∧ Ej}}}};<br/>predicate adjectives are not the same kind of thing as second-order predicates such as colour.
|-
! {{rh}} | Predicate adverbial modifier 
| John is walking very quickly. || {{sdash}}
|-
! {{rh}} | 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".
|-
! {{rh}} | Prepositions 
| Mary is sitting next to John. || The preposition "next to" when applied to "John" results in the predicate adverbial "next to John".
|}