First-order logic: Difference between revisions
Jump to navigation
Jump to search
imported>Farkle Griffen m →Formulas: Equality is a predicate, and linked to the correct article |
imported>Jochen Burghardt Undid revision 1354107739 by ~2026-29128-82 (talk) |
||
| Line 2: | Line 2: | ||
{{Redirect|Predicate logic|logics admitting predicate or function variables|Higher-order logic}} | {{Redirect|Predicate logic|logics admitting predicate or function variables|Higher-order logic}} | ||
{{Transformation rules}} | {{Transformation rules}} | ||
'''First-order logic''', also called '''predicate logic''', '''predicate calculus''', or '''quantificational logic''', is a | '''First-order logic''', also called '''predicate logic''', '''predicate calculus''', or '''quantificational logic''', is a type of [[formal system]] used in [[mathematics]], [[philosophy]], [[linguistics]], and [[computer science]]. First-order logic uses [[Quantification (logic)|quantified variables]] over non-logical objects, and allows the use of sentences that contain variables. Rather than propositions such as "all humans are mortal", in first-order logic one can have expressions in the form "for all ''x'', if ''x'' is a human, then ''x'' is mortal", where "for all ''x''{{-"}} is a quantifier, ''x'' is a variable, and "... ''is a human''{{-"}} and "... ''is mortal''{{-"}} are predicates.<ref>Hodgson, J. P. E., [https://directory.sju.edu/jonathan-hodgson Professor Emeritus] ([https://web.archive.org/web/20190921071136/http://people.sju.edu/~jhodgson/ugai/1order.html "First Order Logic"]), [[Saint Joseph's University]], [[Philadelphia]], 1995.</ref> This distinguishes it from [[propositional logic]], which does not use quantifiers or [[finitary relation|relation]]s;<ref>[[George Edward Hughes|Hughes, G. E.]], & [[Max Cresswell|Cresswell, M. J.]], ''[https://books.google.com/books?id=Dsn1xWNB4MEC&q=%22first-order+logic%22 A New Introduction to Modal Logic]'' ([[London]]: [[Routledge]], 1996), [https://books.google.com/books?id=_CB5wiBeaA4C&pg=PA161&redir_esc=y#v=onepage&q&f=false p.161].</ref>{{rp|161}} in this sense, first-order logic is an extension of propositional logic. | ||
A theory about a topic, such as [[set theory]], a theory for groups,<ref name="Tarski53">A. Tarski, ''Undecidable Theories'' (1953), p. 77. Studies in Logic and the Foundation of Mathematics, North-Holland</ref> or a formal theory of [[arithmetic]], is usually a first-order logic together with a specified [[domain of discourse]] (over which the quantified variables range), finitely many functions from that domain to itself, finitely many [[Predicate (mathematical logic)|predicates]] defined on that domain, and a set of axioms believed to hold about them. "Theory" is sometimes understood in a more formal sense as just a set of sentences in first-order logic. | A theory about a topic, such as [[set theory]], a theory for groups,<ref name="Tarski53">A. Tarski, ''Undecidable Theories'' (1953), p. 77. Studies in Logic and the Foundation of Mathematics, North-Holland</ref> or a formal theory of [[arithmetic]], is usually a first-order logic together with a specified [[domain of discourse]] (over which the quantified variables range), finitely many functions from that domain to itself, finitely many [[Predicate (mathematical logic)|predicates]] defined on that domain, and a set of axioms believed to hold about them. "Theory" is sometimes understood in a more formal sense as just a set of sentences in first-order logic. | ||
| Line 8: | Line 8: | ||
The term "first-order" distinguishes first-order logic from [[higher-order logic]], in which there are predicates having predicates or functions as arguments, or in which quantification over predicates, functions, or both, are permitted.<ref>{{cite book|last=Mendelson|first=E.|author-link=Elliott Mendelson|title=Introduction to Mathematical Logic|year=1964|publisher=[[Wiley (publisher)|Van Nostrand Reinhold]]|page=[https://books.google.com/books?id=UkP0BwAAQBAJ&pg=PA56&redir_esc=y#v=onepage&q&f=false 56]}}</ref>{{rp|56}} In first-order theories, predicates are often associated with sets. In interpreted higher-order theories, predicates may be interpreted as sets of sets. | The term "first-order" distinguishes first-order logic from [[higher-order logic]], in which there are predicates having predicates or functions as arguments, or in which quantification over predicates, functions, or both, are permitted.<ref>{{cite book|last=Mendelson|first=E.|author-link=Elliott Mendelson|title=Introduction to Mathematical Logic|year=1964|publisher=[[Wiley (publisher)|Van Nostrand Reinhold]]|page=[https://books.google.com/books?id=UkP0BwAAQBAJ&pg=PA56&redir_esc=y#v=onepage&q&f=false 56]}}</ref>{{rp|56}} In first-order theories, predicates are often associated with sets. In interpreted higher-order theories, predicates may be interpreted as sets of sets. | ||
There are many [[deductive system]]s for first-order logic which are both [[Soundness#Logical systems|sound]], i.e. all provable statements are true in all models; and [[Completeness (logic)|complete]], i.e. all statements which are true in all models are provable. Although the [[logical consequence]] relation is only [[semidecidability|semidecidable]], much progress has been made in [[automated theorem proving]] in first-order logic. First-order logic also satisfies several [[metalogic | There are many [[deductive system]]s for first-order logic which are both [[Soundness#Logical systems|sound]], i.e. all provable statements are true in all models; and [[Completeness (logic)|complete]], i.e. all statements which are true in all models are provable. Although the [[logical consequence]] relation is only [[semidecidability|semidecidable]], much progress has been made in [[automated theorem proving]] in first-order logic. First-order logic also satisfies several [[metalogic]]al theorems that make it amenable to analysis in [[proof theory]], such as the [[Löwenheim–Skolem theorem]] and the [[compactness theorem]]. | ||
First-order logic is the standard for the formalization of mathematics into [[Axiomatic system|axioms]], and is studied in the [[foundations of mathematics]]. [[Peano arithmetic]] and [[Zermelo–Fraenkel set theory]] are axiomatizations of [[number theory]] and set theory, respectively, into first-order logic. No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the [[natural number]]s or the [[real line]]. Axiom systems that do fully describe these two structures, i.e. [[categorical theory|categorical]] axiom systems, can be obtained in stronger logics such as [[second-order logic]]. | First-order logic is the standard for the formalization of mathematics into [[Axiomatic system|axioms]], and is studied in the [[foundations of mathematics]]. [[Peano arithmetic]] and [[Zermelo–Fraenkel set theory]] are axiomatizations of [[number theory]] and set theory, respectively, into first-order logic. No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the [[natural number]]s or the [[real line]]. Axiom systems that do fully describe these two structures, i.e. [[categorical theory|categorical]] axiom systems, can be obtained in stronger logics such as [[second-order logic]]. | ||
| Line 16: | Line 16: | ||
==Introduction== | ==Introduction== | ||
{{Logical connectives sidebar}} | {{Logical connectives sidebar}} | ||
While [[propositional logic]] deals with simple declarative propositions, first-order logic additionally covers [[ | While [[propositional logic]] deals with simple declarative propositions, first-order logic additionally covers [[Predicate (mathematical logic)|predicate]]s and [[Quantification (logic)|quantification]]. A predicate evaluates to [[True (logic)|true]] or [[False (logic)|false]] for an entity or entities in the [[domain of discourse]]. | ||
Consider the two sentences "[[Socrates]] is a philosopher" and "[[Plato]] is a philosopher". In [[Propositional calculus|propositional logic]], these sentences themselves are viewed as the individuals of study, and might be denoted, for example, by variables such as ''p'' and ''q''. They are not viewed as an application of a predicate, such as <math>\text{ | Consider the two sentences "[[Socrates]] is a philosopher" and "[[Plato]] is a philosopher". In [[Propositional calculus|propositional logic]], these sentences themselves are viewed as the individuals of study, and might be denoted, for example, by variables such as ''p'' and ''q''. They are not viewed as an application of a predicate, such as <math>\text{isPhilosopher}</math>, to any particular objects in the domain of discourse, instead viewing them as purely an utterance which is either true or false.<ref>[[Harvey Friedman (mathematician)|H. Friedman]], "[https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2022/07/RossProg1072322pdf-1-2.pdf Adventures in Foundations of Mathematics 1: Logical Reasoning]", [[Arnold Ross#Ross Mathematics Program|Ross Program]] 2022, lecture notes. Accessed 28 July 2023.</ref> However, in first-order logic, these two sentences may be framed as statements that a certain individual or non-logical object has a property. In this example, both sentences happen to have the common form <math>\text{isPhilosopher}(x)</math> for some individual <math>x</math>, in the first sentence the value of the variable ''x'' is "Socrates", and in the second sentence it is "Plato". Due to the ability to speak about non-logical individuals along with the original logical connectives, first-order logic includes propositional logic.<ref>[[Ben Goertzel|Goertzel, B.]], Geisweiller, N., Coelho, L., Janičić, P., & Pennachin, C., ''Real-World Reasoning: Toward Scalable, Uncertain Spatiotemporal, Contextual and Causal Inference'' ([[Amsterdam]] & Paris: [[Springer Science+Business Media|Atlantis Press]], 2011), [https://books.google.com/books?id=g7UAIhnmJpsC&pg=PA29&redir_esc=y#v=onepage&q&f=false pp. 29–30].</ref>{{rp|29–30}} | ||
The truth of a formula such as "''x'' is a philosopher" depends on which object is denoted by ''x'' and on the interpretation of the predicate "is a philosopher". Consequently, "''x'' is a philosopher" alone does not have a definite truth value of true or false, and is akin to a sentence fragment.<ref name="Quine81" /> Relationships between predicates can be stated using [[logical connective]]s. For example, the first-order formula "if ''x'' is a philosopher, then ''x'' is a scholar", is a [[material conditional|conditional]] statement with "''x'' is a philosopher" as its hypothesis, and "''x'' is a scholar" as its conclusion, which again needs specification of ''x'' in order to have a definite truth value. | The truth of a formula such as "''x'' is a philosopher" depends on which object is denoted by ''x'' and on the interpretation of the predicate "is a philosopher". Consequently, "''x'' is a philosopher" alone does not have a definite truth value of true or false, and is akin to a sentence fragment.<ref name="Quine81" /> Relationships between predicates can be stated using [[logical connective]]s. For example, the first-order formula "if ''x'' is a philosopher, then ''x'' is a scholar", is a [[material conditional|conditional]] statement with "''x'' is a philosopher" as its hypothesis, and "''x'' is a scholar" as its conclusion, which again needs specification of ''x'' in order to have a definite truth value. | ||
| Line 28: | Line 28: | ||
The predicates "is a philosopher" and "is a scholar" each take a single variable. In general, predicates can take several variables. In the first-order sentence "Socrates is the teacher of Plato", the predicate "is the teacher of" takes two variables. | The predicates "is a philosopher" and "is a scholar" each take a single variable. In general, predicates can take several variables. In the first-order sentence "Socrates is the teacher of Plato", the predicate "is the teacher of" takes two variables. | ||
An interpretation (or model) of a first-order formula specifies what each predicate means, and the entities that can instantiate the variables. These entities form the [[domain of discourse]] or universe, which is usually required to be a nonempty set. For example, consider the sentence "There exists ''x'' such that ''x'' is a philosopher." This sentence is seen as being true in an interpretation | An interpretation (or model) of a first-order formula specifies what each predicate means, and the entities that can instantiate the variables. These entities form the [[domain of discourse]] or universe, which is usually required to be a nonempty set. For example, consider the sentence "There exists ''x'' such that ''x'' is a philosopher." This sentence is seen as being true in an interpretation under which the domain of discourse consists of all human beings, and the predicate "is a philosopher" is understood as "was the author of the ''[[Republic (Plato)|Republic]]''." It is thus true in the case of Plato. | ||
There are two key parts of first-order logic. The [[syntax]] determines which finite sequences of symbols are well-formed expressions in first-order logic, while the [[semantics]] determines the meanings behind these expressions. | There are two key parts of first-order logic. The [[syntax]] determines which finite sequences of symbols are well-formed expressions in first-order logic, while the [[semantics]] determines the meanings behind these expressions. | ||
| Line 44: | Line 44: | ||
====Logical symbols==== | ====Logical symbols==== | ||
{{Main|List of logical symbols}} | {{Main|Logical constant|List of logical symbols}} | ||
Logical symbols are a set of characters that vary by author, but usually include the following:<ref>{{Cite web|title=Predicate Logic {{!}} Brilliant Math & Science Wiki|url=https://brilliant.org/wiki/predicate-logic/|access-date=2020-08-20|website=brilliant.org|language=en-us}}</ref> | Logical symbols are a set of characters that vary by author, but usually include the following:<ref>{{Cite web|title=Predicate Logic {{!}} Brilliant Math & Science Wiki|url=https://brilliant.org/wiki/predicate-logic/|access-date=2020-08-20|website=brilliant.org|language=en-us}}</ref> | ||
* [[Quantifier (logic)|Quantifier]] symbols: {{math | * [[Quantifier (logic)|Quantifier]] symbols: {{math|∀}} for [[universal quantification]], and {{math|∃}} for [[existential quantification]] | ||
* [[Logical connective]]s: {{math|∧}} for [[logical conjunction|conjunction]], {{math|∨}} for [[disjunction]], {{math|→}} for [[material conditional|implication]], {{math|↔}} for [[logical biconditional|biconditional]], {{math|¬}} for negation. Some authors<ref>{{Cite web|title=Introduction to Symbolic Logic: Lecture 2|url=http://cstl-cla.semo.edu/hhill/pl120/notes/wffs.html|access-date=2021-01-04|website=cstl-cla.semo.edu}}</ref> use C''pq'' instead of {{math|→}} and E''pq'' instead of {{math|↔}}, especially in contexts where {{math|→}} is used for other purposes. Moreover, the horseshoe {{math|⊃}} may replace {{math|→}};<ref name="Quine81" /> the triple-bar {{math|≡}} may replace {{math|↔}}; a tilde ({{math|~}}), N''p'', or F''p'' may replace {{math|¬}}; a double bar <math>\|</math>, <math>+</math>,<ref>{{cite book|issn=1431-4657|isbn=3540058192|author=[[Hans Hermes]]|title=Introduction to Mathematical Logic|url=https://books.google.com/books?id=ihYPCQAAQBAJ|location=London|publisher=Springer|series=Hochschultext (Springer-Verlag)|year=1973}}</ref> or A''pq'' may replace {{math|∨}}; and an ampersand {{math|&}}, K''pq'', or the middle dot {{math|⋅}} may replace {{math|∧}}, especially if these symbols are not available for technical reasons. | * [[Logical connective]]s: {{math|∧}} for [[logical conjunction|conjunction]], {{math|∨}} for [[disjunction]], {{math|→}} for [[material conditional|implication]], {{math|↔}} for [[logical biconditional|biconditional]], {{math|¬}} for negation. Some authors<ref>{{Cite web|title=Introduction to Symbolic Logic: Lecture 2|url=http://cstl-cla.semo.edu/hhill/pl120/notes/wffs.html|access-date=2021-01-04|website=cstl-cla.semo.edu|archive-date=2021-04-15|archive-url=https://web.archive.org/web/20210415232642/http://cstl-cla.semo.edu/hhill/pl120/notes/wffs.html|url-status=dead}}</ref> use C''pq'' instead of {{math|→}} and E''pq'' instead of {{math|↔}}, especially in contexts where {{math|→}} is used for other purposes. Moreover, the horseshoe {{math|⊃}} may replace {{math|→}};<ref name="Quine81" /> the triple-bar {{math|≡}} may replace {{math|↔}}; a tilde ({{math|~}}), N''p'', or F''p'' may replace {{math|¬}}; a double bar <math>\|</math>, <math>+</math>,<ref>{{cite book|issn=1431-4657|isbn=3540058192|author=[[Hans Hermes]]|title=Introduction to Mathematical Logic|url=https://books.google.com/books?id=ihYPCQAAQBAJ|location=London|publisher=Springer|series=Hochschultext (Springer-Verlag)|year=1973}}</ref> or A''pq'' may replace {{math|∨}}; and an ampersand {{math|&}}, K''pq'', or the middle dot {{math|⋅}} may replace {{math|∧}}, especially if these symbols are not available for technical reasons. | ||
* Parentheses, brackets, and other punctuation symbols. The choice of such symbols varies depending on context. | * Parentheses, brackets, and other punctuation symbols. The choice of such symbols varies depending on context. | ||
* An infinite set of ''variables'', often denoted by lowercase letters at the end of the alphabet ''x'', ''y'', ''z'', ... . Subscripts are often used to distinguish variables: {{math|1= ''x''<sub>0</sub>, ''x''<sub>1</sub>, ''x''<sub>2</sub>, ... .}} | * An infinite set of ''variables'', often denoted by lowercase letters at the end of the alphabet ''x'', ''y'', ''z'', ... . Subscripts are often used to distinguish variables: {{math|1= ''x''<sub>0</sub>, ''x''<sub>1</sub>, ''x''<sub>2</sub>, ... .}} | ||
| Line 62: | Line 62: | ||
[[Non-logical symbol]]s represent predicates (relations), functions and constants. It used to be standard practice to use a fixed, infinite set of non-logical symbols for all purposes: | [[Non-logical symbol]]s represent predicates (relations), functions and constants. It used to be standard practice to use a fixed, infinite set of non-logical symbols for all purposes: | ||
* For every integer ''n'' ≥ 0, there is a collection of [[arity|''n''-''ary'']], or ''n''-''place'', ''[[predicate symbol]]s''. Because they represent [[ | * For every integer ''n'' ≥ 0, there is a collection of [[arity|''n''-''ary'']], or ''n''-''place'', ''[[predicate symbol]]s''. Because they represent [[Relation (philosophy)|relations]] between ''n'' elements, they are also called ''relation symbols''. For each arity ''n'', there is an infinite supply of them: | ||
*:''P''<sup>''n''</sup><sub>0</sub>, ''P''<sup>''n''</sup><sub>1</sub>, ''P''<sup>''n''</sup><sub>2</sub>, ''P''<sup>''n''</sup><sub>3</sub>, ... | *:''P''<sup>''n''</sup><sub>0</sub>, ''P''<sup>''n''</sup><sub>1</sub>, ''P''<sup>''n''</sup><sub>2</sub>, ''P''<sup>''n''</sup><sub>3</sub>, ... | ||
* For every integer ''n'' ≥ 0, there are infinitely many ''n''-ary ''function symbols'': | * For every integer ''n'' ≥ 0, there are infinitely many ''n''-ary ''[[function symbols]]'': | ||
*:''f<sup> n</sup>''<sub>0</sub>, ''f<sup> n</sup>''<sub>1</sub>, ''f<sup> n</sup>''<sub>2</sub>, ''f<sup> n</sup>''<sub>3</sub>, ... | *:''f<sup> n</sup>''<sub>0</sub>, ''f<sup> n</sup>''<sub>1</sub>, ''f<sup> n</sup>''<sub>2</sub>, ''f<sup> n</sup>''<sub>3</sub>, ... | ||
| Line 135: | Line 135: | ||
|} | |} | ||
The [[formation rule]]s define the terms and formulas of first-order logic.<ref>[[Raymond Smullyan|Smullyan, R. M.]], ''First-order Logic'' ([[New York City|New York]]: [[Dover Publications]], 1968), [https://books.google.com/books?id=kgvhQ-oSZiUC&pg=PA5 | The [[formation rule]]s define the terms and formulas of first-order logic.<ref>[[Raymond Smullyan|Smullyan, R. M.]], ''First-order Logic'' ([[New York City|New York]]: [[Dover Publications]], 1968), [https://books.google.com/books?id=kgvhQ-oSZiUC&pg=PA5 p. 5].</ref> When terms and formulas are represented as strings of symbols, these rules can be used to write a [[formal grammar]] for terms and formulas. These rules are generally [[Context-free grammar|context-free]] (each production has a single symbol on the left side), except that the set of symbols may be allowed to be infinite and there may be many start symbols, for example the variables in the case of [[#Terms|terms]]. | ||
====Terms==== | ====Terms==== | ||
| Line 144: | Line 144: | ||
====Formulas==== | ====Formulas==== | ||
The set of ''[[formula (mathematical logic)|formulas]]'' (also called ''[[ | The set of ''[[formula (mathematical logic)|formulas]]'' (also called ''[[well-formed formula]]s''<ref>Some authors who use the term "well-formed formula" use "formula" to mean any string of symbols from the alphabet. However, most authors in mathematical logic use "formula" to mean "well-formed formula" and have no term for non-well-formed formulas. In every context, it is only the well-formed formulas that are of interest.</ref> or ''WFFs'') is inductively defined by the following rules: | ||
# ''Predicate symbols''. If ''P'' is an ''n''-ary predicate symbol and ''t''<sub>1</sub>, ..., ''t''<sub>''n''</sub> are terms then ''P''(''t''<sub>1</sub>,...,''t''<sub>''n''</sub>) is a formula. | # ''Predicate symbols''. If ''P'' is an ''n''-ary predicate symbol and ''t''<sub>1</sub>, ..., ''t''<sub>''n''</sub> are terms then ''P''(''t''<sub>1</sub>,...,''t''<sub>''n''</sub>) is a formula. | ||
#* ''[[Equality (mathematics)|Equality]]''. If the equality symbol is considered part of logic, and ''t''<sub>1</sub> and ''t''<sub>2</sub> are terms, then ''t''<sub>1</sub> = ''t''<sub>2</sub> is a formula. | #* ''[[Equality (mathematics)|Equality]]''. If the equality symbol is considered part of logic, and ''t''<sub>1</sub> and ''t''<sub>2</sub> are terms, then ''t''<sub>1</sub> = ''t''<sub>2</sub> is a formula. | ||
| Line 150: | Line 150: | ||
# ''Binary connectives''. If {{tmath|\varphi}} and {{tmath|\psi}} are formulas, then (<math>\varphi\rightarrow\psi</math>) is a formula. Similar rules apply to other binary logical connectives. | # ''Binary connectives''. If {{tmath|\varphi}} and {{tmath|\psi}} are formulas, then (<math>\varphi\rightarrow\psi</math>) is a formula. Similar rules apply to other binary logical connectives. | ||
# ''Quantifiers''. If <math>\varphi</math> is a formula and ''x'' is a variable, then <math>\forall x \varphi</math> (for all x, <math>\varphi</math> holds) and <math>\exists x \varphi</math> (there exists x such that <math>\varphi</math>) are formulas. | # ''Quantifiers''. If <math>\varphi</math> is a formula and ''x'' is a variable, then <math>\forall x \varphi</math> (for all x, <math>\varphi</math> holds) and <math>\exists x \varphi</math> (there exists x such that <math>\varphi</math>) are formulas. | ||
Only expressions which can be obtained by finitely many applications of rules | Only expressions which can be obtained by finitely many applications of rules 1–4 are formulas. The formulas obtained from the first rule are said to be ''[[atomic formula]]s''. | ||
For example: | For example: | ||
| Line 163: | Line 163: | ||
* <math>\land</math> and <math>\lor</math> are evaluated next | * <math>\land</math> and <math>\lor</math> are evaluated next | ||
* Quantifiers are evaluated next | * Quantifiers are evaluated next | ||
* <math>\to</math> | * <math>\to</math> and <math>\lrarr</math> are evaluated last. | ||
Moreover, extra punctuation not required by the definition may be inserted—to make formulas easier to read. Thus the formula: | Moreover, extra punctuation not required by the definition may be inserted—to make formulas easier to read. Thus the formula: | ||
:<math>\lnot \forall x P(x) \to \exists x \lnot P(x)</math> | :<math>\lnot \forall x P(x) \to \exists x \lnot P(x)</math> | ||
| Line 172: | Line 172: | ||
{{Main|Free variables and bound variables}} | {{Main|Free variables and bound variables}} | ||
In a formula, a variable may occur ''free'' or ''bound'' (or both). One formalization of this notion is due to Quine, first the concept of a variable occurrence is defined, then whether a variable occurrence is free or bound, then whether a variable symbol overall is free or bound. In order to distinguish different occurrences of the identical symbol ''x'', each occurrence of a variable symbol ''x'' in a formula φ is identified with the initial substring of φ up to the point at which said instance of the symbol ''x'' appears.<ref name="Quine81">[[Willard Van Orman Quine|W. V. O. Quine]], [https://www.google.com/books/edition/_/6_syEAAAQBAJ?hl=en&gbpv=1&pg=PP1 ''Mathematical Logic''] (1981). [[Harvard University Press]], 0-674-55451-5.</ref><sup>p.297</sup> Then, an occurrence of ''x'' is said to be bound if that occurrence of ''x'' lies within the scope of at least one of either <math>\exists x</math> or <math>\forall x</math>. Finally, ''x'' is bound in φ if all occurrences of ''x'' in φ are bound.<ref name="Quine81" /><sup>pp. | In a formula, a variable may occur ''free'' or ''bound'' (or both). One formalization of this notion is due to Quine, first the concept of a variable occurrence is defined, then whether a variable occurrence is free or bound, then whether a variable symbol overall is free or bound. In order to distinguish different occurrences of the identical symbol ''x'', each occurrence of a variable symbol ''x'' in a formula φ is identified with the initial substring of φ up to the point at which said instance of the symbol ''x'' appears.<ref name="Quine81">[[Willard Van Orman Quine|W. V. O. Quine]], [https://www.google.com/books/edition/_/6_syEAAAQBAJ?hl=en&gbpv=1&pg=PP1 ''Mathematical Logic''] (1981). [[Harvard University Press]], 0-674-55451-5.</ref><sup>p. 297</sup> Then, an occurrence of ''x'' is said to be bound if that occurrence of ''x'' lies within the scope of at least one of either <math>\exists x</math> or <math>\forall x</math>. Finally, ''x'' is bound in φ if all occurrences of ''x'' in φ are bound.<ref name="Quine81" /><sup>pp. 142–143</sup> | ||
Intuitively, a variable symbol is free in a formula if at no point is it quantified:<ref name="Quine81" /><sup>pp. | Intuitively, a variable symbol is free in a formula if at no point is it quantified:<ref name="Quine81" /><sup>pp. 142–143</sup> in {{math|∀''y'' ''P''(''x'', ''y'')}}, the sole occurrence of variable ''x'' is free while that of ''y'' is bound. The free and bound variable occurrences in a formula are defined inductively as follows. | ||
; Atomic formulas : If ''φ'' is an atomic formula, then ''x'' occurs free in ''φ'' if and only if ''x'' occurs in ''φ''. Moreover, there are no bound variables in any atomic formula. | ; Atomic formulas : If ''φ'' is an atomic formula, then ''x'' occurs free in ''φ'' if and only if ''x'' occurs in ''φ''. Moreover, there are no bound variables in any atomic formula. | ||
; Negation : ''x'' occurs free in ¬''φ'' if and only if ''x'' occurs free in ''φ''. ''x'' occurs bound in ¬''φ'' if and only if ''x'' occurs bound in ''φ'' | ; Negation : ''x'' occurs free in ¬''φ'' if and only if ''x'' occurs free in ''φ''. ''x'' occurs bound in ¬''φ'' if and only if ''x'' occurs bound in ''φ'' | ||
| Line 202: | Line 202: | ||
The most common way of specifying an interpretation (especially in mathematics) is to specify a ''structure'' (also called a ''model''; see below). The structure consists of a domain of discourse ''D'' and an interpretation function {{mvar|I}} mapping non-logical symbols to predicates, functions, and constants. | The most common way of specifying an interpretation (especially in mathematics) is to specify a ''structure'' (also called a ''model''; see below). The structure consists of a domain of discourse ''D'' and an interpretation function {{mvar|I}} mapping non-logical symbols to predicates, functions, and constants. | ||
The domain of discourse ''D'' is a nonempty set of "objects" of some kind. Intuitively, given an interpretation, a first-order formula becomes a statement about these objects; for example, <math>\exists x P(x)</math> states the existence of some object in ''D'' for which the predicate ''P'' is true (or, more precisely, for which the predicate assigned to the predicate symbol ''P'' by the interpretation is true). For example, one can take ''D'' to be the set of [[ | The domain of discourse ''D'' is a nonempty set of "objects" of some kind. Intuitively, given an interpretation, a first-order formula becomes a statement about these objects; for example, <math>\exists x P(x)</math> states the existence of some object in ''D'' for which the predicate ''P'' is true (or, more precisely, for which the predicate assigned to the predicate symbol ''P'' by the interpretation is true). For example, one can take ''D'' to be the set of [[integer]]s. | ||
Non-logical symbols are interpreted as follows: | Non-logical symbols are interpreted as follows: | ||
* The interpretation of an ''n''-ary function symbol is a function from ''D''<sup>''n''</sup> to ''D''. For example, if the domain of discourse is the set of integers, a function symbol ''f'' of arity 2 can be interpreted as the function that gives the sum of its arguments. In other words, the symbol ''f'' is associated with the function {{tmath|I(f)}} which, in this interpretation, is addition. | * The interpretation of an ''n''-ary function symbol is a function from ''D''<sup>''n''</sup> to ''D''. For example, if the domain of discourse is the set of integers, a function symbol ''f'' of arity 2 can be interpreted as the function that gives the sum of its arguments. In other words, the symbol ''f'' is associated with the function {{tmath|I(f)}} which, in this interpretation, is addition. | ||
* The interpretation of a constant symbol (a function symbol of arity 0) is a function from ''D''<sup>0</sup> (a set whose only member is the empty [[tuple]]) to ''D'', which can be simply identified with an object in ''D''. For example, an interpretation may assign the value <math>I(c)=10</math> to the constant symbol <math>c</math>. | * The interpretation of a constant symbol (a function symbol of arity 0) is a function from ''D''<sup>0</sup> (a set whose only member is the empty [[tuple]]) to ''D'', which can be simply identified with an object in ''D''. For example, an interpretation may assign the value <math>I(c)=10</math> to the constant symbol <math>c</math>. | ||
* The interpretation of an ''n''-ary predicate symbol is a set of ''n''-tuples of elements of ''D'', giving the arguments for which the predicate is true. For example, an interpretation <math>I(P)</math> of a binary predicate symbol ''P'' may be the set of pairs of integers such that the first one is less than the second. According to this interpretation, the predicate ''P'' would be true if its first argument is less than its second argument. Equivalently, predicate symbols may be assigned [[Boolean-valued function]]s from ''D''<sup>''n''</sup> to <math>\{\mathrm{true, false}\}</math>. | * The interpretation of an ''n''-ary predicate symbol is a set of ''n''-tuples of elements of ''D'', giving the arguments for which the predicate is true. For example, an interpretation <math>I(P)</math> of a binary predicate symbol ''P'' may be the set of pairs of integers such that the first one is less than the second. According to this interpretation, the predicate ''P'' would be true if its first argument is less than its second argument. Equivalently, predicate symbols may be assigned [[Boolean-valued function]]s from ''D''<sup>''n''</sup> to <math>\{\mathrm{true, false}\}</math>. | ||
| Line 262: | Line 260: | ||
Many theories have an ''[[intended interpretation]]'', a certain model that is kept in mind when studying the theory. For example, the intended interpretation of [[Peano arithmetic]] consists of the usual [[natural number]]s with their usual operations. However, the Löwenheim–Skolem theorem shows that most first-order theories will also have other, [[nonstandard model]]s. | Many theories have an ''[[intended interpretation]]'', a certain model that is kept in mind when studying the theory. For example, the intended interpretation of [[Peano arithmetic]] consists of the usual [[natural number]]s with their usual operations. However, the Löwenheim–Skolem theorem shows that most first-order theories will also have other, [[nonstandard model]]s. | ||
A theory is ''[[consistency|consistent]]'' (within a [[First-order logic# | A theory is ''[[consistency|consistent]]'' (within a [[First-order logic#Deductive systems|deductive system]]) if it is not possible to prove a contradiction from the axioms of the theory. A theory is ''[[complete theory|complete]]'' if, for every formula in its signature, either that formula or its negation is a logical consequence of the axioms of the theory. [[Gödel's incompleteness theorem]] shows that effective first-order theories that include a sufficient portion of the arithmetic of the natural numbers can never be both consistent and complete. | ||
===Empty domains=== | ===Empty domains=== | ||
| Line 373: | Line 371: | ||
Unlike [[propositional logic]], first-order logic is [[Decidability (logic)|undecidable]] (although semidecidable), provided that the language has at least one predicate of arity at least 2 (other than equality). This means that there is no [[decision procedure]] that determines whether arbitrary formulas are logically valid. This result was established independently by [[Alonzo Church]] and [[Alan Turing]] in 1936 and 1937, respectively, giving a negative answer to the [[Entscheidungsproblem]] posed by [[David Hilbert]] and [[Wilhelm Ackermann]] in 1928. Their proofs demonstrate a connection between the unsolvability of the decision problem for first-order logic and the unsolvability of the [[halting problem]]. | Unlike [[propositional logic]], first-order logic is [[Decidability (logic)|undecidable]] (although semidecidable), provided that the language has at least one predicate of arity at least 2 (other than equality). This means that there is no [[decision procedure]] that determines whether arbitrary formulas are logically valid. This result was established independently by [[Alonzo Church]] and [[Alan Turing]] in 1936 and 1937, respectively, giving a negative answer to the [[Entscheidungsproblem]] posed by [[David Hilbert]] and [[Wilhelm Ackermann]] in 1928. Their proofs demonstrate a connection between the unsolvability of the decision problem for first-order logic and the unsolvability of the [[halting problem]]. | ||
There are systems weaker than full first-order logic for which the logical consequence relation is decidable. These include propositional logic and [[monadic predicate logic]], which is first-order logic restricted to unary predicate symbols and no function symbols. Other logics with no function symbols which are decidable are the [[guarded fragment]] of first-order logic, as well as [[two-variable logic]]. The [[Bernays–Schönfinkel class]] of first-order formulas is also decidable. Decidable subsets of first-order logic are also studied in the framework of [[description logics]]. | === Decidable fragments === | ||
There are systems weaker than full first-order logic for which the logical consequence relation is decidable. These include propositional logic and [[monadic predicate logic]], which is first-order logic restricted to unary predicate symbols and no function symbols. Other logics with no function symbols which are decidable are the [[guarded fragment]] of first-order logic, as well as [[two-variable logic]]. The [[Bernays–Schönfinkel class]] of first-order formulas is also decidable. Decidable subsets of first-order logic are also studied in the framework of [[description logics]]. See (Pratt-Hartmann, 2023) for a monograph.<ref>{{Cite book |last=Pratt-Hartmann |first=Ian |title=Fragments of first-order logic |date=2023 |publisher=Oxford University Press |isbn=978-0-19-286796-4 |series=Oxford logic guides |location=Oxford}}</ref> | |||
=== | Examples of decidable fragments:<ref>{{Cite thesis |last=Voigt |first=Marco |title=Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates |date=2019-07-31 |degree=PhD |publisher=Universität des Saarlandes |url=https://inria.hal.science/tel-02406821 |language=en |chapter=3. Novel First-Order Fragments with a Decidable Satisfiability Problem}}</ref> | ||
* C<sub>2</sub>, FOL 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> | |||
* monadic first-order fragment (MFO, or Löwenheim fragment): FOL without equality, without function symbols, and with only unary predicate symbols. | |||
* Löb–Gurevich fragment: FOL without equality, with only unary function symbols, and with only unary predicate symbols. | |||
* Rabin fragment: FOL with equality, with exactly one unary function symbol, and with only unary predicate symbols. | |||
* Bernays–Schönfinkel–Ramsey fragment: all relational first-order sentences in prenex normal form with <math>\exists^* \forall^*</math> prefix and with equality. | |||
===Löwenheim–Skolem theorem=== | |||
The [[Löwenheim–Skolem theorem]] shows that if a first-order theory of [[cardinality]] λ has an infinite model, then it has models of every infinite cardinality greater than or equal to λ. One of the earliest results in [[model theory]], it implies that it is not possible to characterize [[countable set|countability]] or uncountability in a first-order language with a countable signature. That is, there is no first-order formula φ(''x'') such that an arbitrary structure M satisfies φ if and only if the domain of discourse of M is countable (or, in the second case, uncountable). | The [[Löwenheim–Skolem theorem]] shows that if a first-order theory of [[cardinality]] λ has an infinite model, then it has models of every infinite cardinality greater than or equal to λ. One of the earliest results in [[model theory]], it implies that it is not possible to characterize [[countable set|countability]] or uncountability in a first-order language with a countable signature. That is, there is no first-order formula φ(''x'') such that an arbitrary structure M satisfies φ if and only if the domain of discourse of M is countable (or, in the second case, uncountable). | ||
The Löwenheim–Skolem theorem implies that infinite structures cannot be [[categorical theory|categorically]] axiomatized in first-order logic. For example, there is no first-order theory whose only model is the real line: any first-order theory with an infinite model also has a model of cardinality larger than the continuum. Since the real line is infinite, any theory satisfied by the real line is also satisfied by some [[nonstandard model]]s. When the Löwenheim–Skolem theorem is applied to first-order set theories, the nonintuitive consequences are known as [[Skolem's paradox]]. | The Löwenheim–Skolem theorem implies that infinite structures cannot be [[categorical theory|categorically]] axiomatized in first-order logic. For example, there is no first-order theory whose only model is the real line: any first-order theory with an infinite model also has a model of cardinality larger than the continuum. Since the real line is infinite, any theory satisfied by the real line is also satisfied by some [[nonstandard model]]s. When the Löwenheim–Skolem theorem is applied to first-order set theories, the nonintuitive consequences are known as [[Skolem's paradox]]. | ||
=== | ===Compactness theorem=== | ||
The [[compactness theorem]] states that a set of first-order sentences has a model if and only if every finite subset of it has a model.<ref>Hodel, R. E., ''An Introduction to Mathematical Logic'' ([[Mineola, New York|Mineola NY]]: [[Dover Publications|Dover]], 1995), [https://books.google.com/books?id=SxRYdzWio84C&pg=PA199 p. 199].</ref> This implies that if a formula is a logical consequence of an infinite set of first-order axioms, then it is a logical consequence of some finite number of those axioms. This theorem was proved first by Kurt Gödel as a consequence of the completeness theorem, but many additional proofs have been obtained over time. It is a central tool in model theory, providing a fundamental method for constructing models. | The [[compactness theorem]] states that a set of first-order sentences has a model if and only if every finite subset of it has a model.<ref>Hodel, R. E., ''An Introduction to Mathematical Logic'' ([[Mineola, New York|Mineola NY]]: [[Dover Publications|Dover]], 1995), [https://books.google.com/books?id=SxRYdzWio84C&pg=PA199 p. 199].</ref> This implies that if a formula is a logical consequence of an infinite set of first-order axioms, then it is a logical consequence of some finite number of those axioms. This theorem was proved first by Kurt Gödel as a consequence of the completeness theorem, but many additional proofs have been obtained over time. It is a central tool in model theory, providing a fundamental method for constructing models. | ||
| Line 396: | Line 403: | ||
==Limitations== | ==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. | 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. | ||
===Expressiveness=== | ===Expressiveness=== | ||
| Line 404: | Line 409: | ||
===Formalizing natural languages=== | ===Formalizing natural languages=== | ||
{{Main|Logic translation#Natural language formalization}} | {{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(.)]]. | 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(.)]]. | ||
| Line 450: | Line 456: | ||
===Many-sorted logic=== | ===Many-sorted logic=== | ||
{{main|Many-sorted logic}} | {{main|Many-sorted logic}} | ||
Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range. ''Many-sorted first-order logic'' allows variables to have different ''sorts'', which have different domains. This is also called ''typed first-order logic'', and the sorts called ''types'' (as in [[data type]]), but it is not the same as first-order [[type theory]]. Many-sorted first-order logic is often used in the study of [[second-order arithmetic]].<ref>{{Cite SEP|url-id=quantification|title=Quantifiers and Quantification|date=October 17, 2018|edition=Winter 2018|last=Uzquiano|first=Gabriel}} See in particular section 3.2, Many-Sorted Quantification.</ref> | Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range. ''Many-sorted first-order logic'' allows variables to have different ''sorts'', which have different domains. This is also called ''typed first-order logic'', and the sorts called ''types'' (as in [[data type]]), but it is not the same as first-order [[type theory]]. Many-sorted first-order logic is often used in the study of [[second-order arithmetic]].<ref>{{Cite SEP|url-id=quantification|title=Quantifiers and Quantification|date=October 17, 2018|edition=Winter 2018|last=Uzquiano|first=Gabriel}} See in particular section 3.2, Many-Sorted Quantification.</ref> | ||
| Line 467: | Line 474: | ||
===Infinitary logics=== | ===Infinitary logics=== | ||
{{Main|Infinitary logic}} | {{Main|Infinitary logic}} | ||
Infinitary logic allows infinitely long sentences. For example, one may allow a conjunction or disjunction of infinitely many formulas, or quantification over infinitely many variables. Infinitely long sentences arise in areas of mathematics including [[topology]] and [[model theory]]. | Infinitary logic allows infinitely long sentences. For example, one may allow a conjunction or disjunction of infinitely many formulas, or quantification over infinitely many variables. Infinitely long sentences arise in areas of mathematics including [[topology]] and [[model theory]]. | ||
| Line 478: | Line 486: | ||
===Non-classical and modal logics=== | ===Non-classical and modal logics=== | ||
{{main|Non-classical logic}} | {{main|Non-classical logic}} | ||
*''[[intuitionistic logic|Intuitionistic first-order logic]]'' uses intuitionistic rather than classical reasoning; for example, ¬¬φ need not be equivalent to φ and ¬ ∀x.φ is in general not equivalent to ∃ x.¬φ . | *''[[intuitionistic logic|Intuitionistic first-order logic]]'' uses intuitionistic rather than classical reasoning; for example, ¬¬φ need not be equivalent to φ and ¬ ∀x.φ is in general not equivalent to ∃ x.¬φ . | ||
| Line 486: | Line 494: | ||
===Fixpoint logic=== | ===Fixpoint logic=== | ||
{{main|Fixed-point logic}} | {{main|Fixed-point logic}} | ||
Fixpoint logic extends first-order logic by adding the closure under the least fixed points of positive operators.<ref>{{cite book | title=Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers | volume=702 | series=Lecture Notes in Computer Science | editor1-first=Egon | editor1-last=Börger | publisher=[[Springer-Verlag]] | year=1993 | zbl=0808.03024 | isbn=3-540-56992-8 | pages=100–114 | first=Uwe | last=Bosse | chapter=An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic }}</ref> | Fixpoint logic extends first-order logic by adding the closure under the least fixed points of positive operators.<ref>{{cite book | title=Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers | volume=702 | series=Lecture Notes in Computer Science | editor1-first=Egon | editor1-last=Börger | publisher=[[Springer-Verlag]] | year=1993 | zbl=0808.03024 | isbn=3-540-56992-8 | pages=100–114 | first=Uwe | last=Bosse | chapter=An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic }}</ref> | ||
| Line 565: | Line 574: | ||
* [[David Hilbert|Hilbert, David]]; and [[Wilhelm Ackermann|Ackermann, Wilhelm]] (1950); ''[[Principles of Mathematical Logic]]'', Chelsea (English translation of ''Grundzüge der theoretischen Logik'', 1928 German first edition) | * [[David Hilbert|Hilbert, David]]; and [[Wilhelm Ackermann|Ackermann, Wilhelm]] (1950); ''[[Principles of Mathematical Logic]]'', Chelsea (English translation of ''Grundzüge der theoretischen Logik'', 1928 German first edition) | ||
* [[Wilfrid Hodges|Hodges, Wilfrid]] (2001); "Classical Logic I: First-Order Logic", in Goble, Lou (ed.); ''The Blackwell Guide to Philosophical Logic'', Blackwell | * [[Wilfrid Hodges|Hodges, Wilfrid]] (2001); "Classical Logic I: First-Order Logic", in Goble, Lou (ed.); ''The Blackwell Guide to Philosophical Logic'', Blackwell | ||
* [[Heinz-Dieter Ebbinghaus|Ebbinghaus, Heinz-Dieter]]; Flum, Jörg; and Thomas, Wolfgang (1994); [https://books.google.com/books?id=4sbSBwAAQBAJ&printsec=frontcover&hl=iw&source=gbs_ge_summary_r&cad=0#v=onepage&q&f=false | * [[Heinz-Dieter Ebbinghaus|Ebbinghaus, Heinz-Dieter]]; Flum, Jörg; and Thomas, Wolfgang (1994); [https://books.google.com/books?id=4sbSBwAAQBAJ&printsec=frontcover&hl=iw&source=gbs_ge_summary_r&cad=0#v=onepage&q&f=false ''Mathematical Logic''], [[Undergraduate Texts in Mathematics]], Berlin, DE/New York, NY: [[Springer-Verlag]], Second Edition, {{ISBN|978-0-387-94258-2}} | ||
* Tarski, Alfred and Givant, Steven (1987); [https://books.google.com/books?id=BgviDgAAQBAJ&printsec=frontcover&hl=cs&source=gbs_ge_summary_r&redir_esc=y#v=onepage&q&f=false ''A Formalization of Set Theory without Variables'']. Vol. 41 of [[American Mathematical Society#Publications|American Mathematical Society colloquium publications]], Providence RI: [[American Mathematical Society]], {{ISBN|978-0821810415}} | * Tarski, Alfred and Givant, Steven (1987); [https://books.google.com/books?id=BgviDgAAQBAJ&printsec=frontcover&hl=cs&source=gbs_ge_summary_r&redir_esc=y#v=onepage&q&f=false ''A Formalization of Set Theory without Variables'']. Vol. 41 of [[American Mathematical Society#Publications|American Mathematical Society colloquium publications]], Providence RI: [[American Mathematical Society]], {{ISBN|978-0821810415}} | ||