First-order logic

First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable.^[1] This distinguishes it from propositional logic, which does not use quantifiers or relations;^[2] in this sense, propositional logic is the foundation of first-order logic.

"Predicate logic" redirects here. For logics admitting predicate or function variables, see Higher-order logic.

A theory about a topic, such as set theory, a theory for groups,^[3] 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 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.^[4]^: 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 systems for first-order logic which are both sound, i.e. all provable statements are true in all models, and complete, i.e. all statements which are true in all models are provable. Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first-order logic. First-order logic also satisfies several 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 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 numbers or the real line. Axiom systems that do fully describe these two structures, i.e. 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.^[5] For a history of first-order logic and how it came to dominate formal logic, see José Ferreirós (2001).

symbols: $\forall$ for universal quantification, and $\exists$ for existential quantification

Quantifier

: $\land$ for conjunction, $\lor$ for disjunction, $\to$ for implication, $\leftrightarrow$ for biconditional, $\neg$ for negation. Some authors^[11] use Cpq instead of $\to$ and Epq instead of $\leftrightarrow$ , especially in contexts where → is used for other purposes. Moreover, the horseshoe $\supset$ may replace $\to$ ;^[8] the triple-bar $\equiv$ may replace $\leftrightarrow$ ; a tilde ( $~$ ), Np, or Fp may replace $\neg$ ; a double bar $\|$ , $+$ ,^[12] or Apq may replace $\lor$ ; and an ampersand $&$ , Kpq, or the middle dot $\cdot$ may replace $\land$ , especially if these symbols are not available for technical reasons. (The aforementioned symbols Cpq, Epq, Np, Apq, and Kpq are used in Polish notation.)

Logical connectives

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: $x 0, x 1, x 2, ... .$

An equality symbol (sometimes, identity symbol) $=$ (see below).

§ Equality and its axioms

The interpretation of an n-ary function symbol is a function from Dⁿ 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 $I(f)$ which, in this interpretation, is addition.

Reflexivity. For each variable x, x = x.

Substitution for functions. For all variables x and y, and any function symbol f,
x = y → f(..., x, ...) = f(..., y, ...).

Substitution for formulas. For any variables x and y and any formula φ(x), if φ' is obtained by replacing any number of free occurrences of x in φ with y, such that these remain free occurrences of y, then:
x = y → (φ → φ').

A logical system satisfying Lindström's definition that contains first-order logic and satisfies both the Löwenheim–Skolem theorem and the compactness theorem must be equivalent to first-order logic.

A logical system satisfying Lindström's definition that has a semidecidable logical consequence relation and satisfies the Löwenheim–Skolem theorem must be equivalent to first-order logic.

Because $\exists x\varphi (x)$ can be expressed as $\neg \forall x\neg \varphi (x)$ , and $\forall x\varphi (x)$ can be expressed as $\neg \exists x\neg \varphi (x)$ , either of the two quantifiers $\exists$ and $\forall$ can be dropped.

Since $\varphi \lor \psi$ can be expressed as $\lnot (\lnot \varphi \land \lnot \psi )$ and $\varphi \land \psi$ can be expressed as $\lnot (\lnot \varphi \lor \lnot \psi )$ , either $\vee$ or $\wedge$ can be dropped. In other words, it is sufficient to have $\neg$ and $\vee$ , or $\neg$ and $\wedge$ , as the only logical connectives.

Similarly, it is sufficient to have only $\neg$ and $\rightarrow$ as logical connectives, or to have only the (NAND) or the Peirce arrow (NOR) operator.

Sheffer stroke

It is possible to entirely avoid function symbols and constant symbols, rewriting them via predicate symbols in an appropriate way. For example, instead of using a constant symbol $\;0$ one may use a predicate $\;0(x)$ (interpreted as $\;x=0$ ) and replace every predicate such as $\;P(0,y)$ with $\forall x\;(0(x)\rightarrow P(x,y))$ . A function such as $f(x_{1},x_{2},...,x_{n})$ will similarly be replaced by a predicate $F(x_{1},x_{2},...,x_{n},y)$ interpreted as $y=f(x_{1},x_{2},...,x_{n})$ . This change requires adding additional axioms to the theory at hand, so that interpretations of the predicate symbols used have the correct semantics.

[32]

(2010), A Concise Introduction to Mathematical Logic (3rd ed.), New York, NY: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6

Rautenberg, Wolfgang

(2002); An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed., Berlin: Kluwer Academic Publishers. Available from Springer.

Andrews, Peter B.

Avigad, Jeremy; Donnelly, Kevin; Gray, David; and Raff, Paul (2007); "A formally verified proof of the prime number theorem", ACM Transactions on Computational Logic, vol. 9 no. 1 :10.1145/1297658.1297660

doi

(1977). "An Introduction to First-Order Logic". In Barwise, Jon (ed.). Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. Amsterdam, NL: North-Holland (published 1982). ISBN 978-0-444-86388-1.

Barwise, Jon

Monk, J. Donald (1976). . New York, NY: Springer New York. doi:10.1007/978-1-4684-9452-5. ISBN 978-1-4684-9454-9.

Mathematical Logic

Barwise, Jon; and (2000); Language Proof and Logic, Stanford, CA: CSLI Publications (Distributed by the University of Chicago Press)

Etchemendy, John

(2007); A Précis of Mathematical Logic, Dordrecht, NL: D. Reidel, translated from the French and German editions by Otto Bird

Bocheński, Józef Maria

Ferreirós, José (2001); , Bulletin of Symbolic Logic, Volume 7, Issue 4, 2001, pp. 441–484, doi:10.2307/2687794, JSTOR 2687794

The Road to Modern Logic — An Interpretation

(1991), Logic, Language, and Meaning, Volume 2: Intensional Logic and Logical Grammar, Chicago, Illinois: University of Chicago Press, ISBN 0-226-28088-8

Gamut, L. T. F.

; and Ackermann, Wilhelm (1950); Principles of Mathematical Logic, Chelsea (English translation of Grundzüge der theoretischen Logik, 1928 German first edition)

Hilbert, David

(2001); "Classical Logic I: First-Order Logic", in Goble, Lou (ed.); The Blackwell Guide to Philosophical Logic, Blackwell

Hodges, Wilfrid

; Flum, Jörg; and Thomas, Wolfgang (1994); Mathematical Logic, Undergraduate Texts in Mathematics, Berlin, DE/New York, NY: Springer-Verlag, Second Edition, ISBN 978-0-387-94258-2

Ebbinghaus, Heinz-Dieter

Tarski, Alfred and Givant, Steven (1987); A Formalization of Set Theory without Variables. Vol.41 of American Mathematical Society colloquium publications, Providence RI: American Mathematical Society, 978-0821810415

ISBN

, Encyclopedia of Mathematics, EMS Press, 2001 [1994]

"Predicate calculus"

: Shapiro, Stewart; "Classical Logic". Covers syntax, model theory, and metatheory for first-order logic in the natural deduction style.

Stanford Encyclopedia of Philosophy

Magnus, P. D.; . Covers formal semantics and proof theory for first-order logic.

forall x: an introduction to formal logic

: an ongoing online project to reconstruct mathematics as a huge first-order theory, using first-order logic and the axiomatic set theory ZFC. Principia Mathematica modernized.

Metamath

Podnieks, Karl;

Introduction to mathematical logic

(typeset by John Fremlin). These notes cover part of a past Cambridge Mathematical Tripos course taught to undergraduate students (usually) within their third year. The course is entitled "Logic, Computation and Set Theory" and covers Ordinals and cardinals, Posets and Zorn's Lemma, Propositional logic, Predicate logic, Set theory and Consistency issues related to ZFC and other set theories.

Cambridge Mathematical Tripos notes

can validate or invalidate formulas of first-order logic through the semantic tableaux method.