Editing First-order logic (section)

{{Short description|Type of logical system}}
{{Redirect|Predicate logic|logics admitting predicate or function variables|Higher-order logic}}
{{Transformation rules}}
'''First-order logic''', also called '''predicate logic''', '''predicate calculus''', or '''quantificational logic''', is a collection of [[formal system]]s 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, propositional logic is the foundation of 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.

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|metalogical]] 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]].

The foundations of first-order logic were developed independently by [[Gottlob Frege]] and [[Charles Sanders Peirce]].<ref>Eric M. Hammer: Semantics for Existential Graphs, ''Journal of Philosophical Logic'', Volume 27, Issue 5 (October 1998), page 489: "Development of first-order logic independently of Frege, anticipating prenex and Skolem normal forms"</ref> For a history of first-order logic and how it came to dominate formal logic, see José Ferreirós (2001).