Editing First-order logic (section)

==Syntax==
{{Formal languages}}
{{seealso|Formal language}}Unlike natural languages, such as English, the language of first-order logic is completely formal, so that it can be mechanically determined whether a given expression is [[Well-formedness|well formed]]. There are two key types of well-formed expressions: ''terms'', which intuitively represent objects, and ''formulas'', which intuitively express statements that can be true or false. The terms and formulas of first-order logic are strings of ''[[Symbol (formal)|symbols]]'', where all the symbols together form the ''[[Alphabet (formal languages)|alphabet]]'' of the language. 

===Alphabet===
{{seealso|Alphabet (formal languages)|Symbol (formal)}}

As with all [[formal language]]s, the nature of the symbols themselves is outside the scope of formal logic; they are often regarded simply as letters and punctuation symbols.

It is common to divide the symbols of the alphabet into ''logical symbols'', which always have the same meaning, and ''non-logical symbols'', whose meaning varies by interpretation.<ref>{{Cite book |last=Davis |first=Ernest |title=Representations of Commonsense Knowledge |publisher=Morgan Kauffmann |year=1990 |isbn=978-1-4832-0770-4 |pages=27–28}}</ref> For example, the logical symbol <math>\land</math> always represents "and"; it is never interpreted as "or", which is represented by the logical symbol <math>\lor</math>. However, a non-logical predicate symbol such as Phil(''x'') could be interpreted to mean "''x'' is a philosopher", "''x'' is a man named Philip", or any other unary predicate depending on the interpretation at hand.

====Logical symbols====
{{Main|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>
* [[Quantifier (logic)|Quantifier]] symbols: {{math|[[Universal quantification|∀]]}} for universal quantification, and {{math|[[Existential quantification|∃]]}} 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 → 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.
* 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>, ...&nbsp;.}}
* An ''equality symbol'' (sometimes, ''identity symbol'') {{math|{{=}}}} (see {{section link|#Equality_and_its_axioms}} below).

Not all of these symbols are required in first-order logic. Either one of the quantifiers along with negation, conjunction (or disjunction), variables, brackets, and equality suffices.

Other logical symbols include the following:
* Truth constants: T, or {{math|⊤}} for "true" and F, or {{math|⊥}} for "false". Without any such logical operators of valence 0, these two constants can only be expressed using quantifiers.
* Additional logical connectives such as the [[Sheffer stroke]], D''pq'' (NAND), and [[exclusive or]], J''pq''.

====Non-logical symbols====<!-- This section is linked from [[Axiom of empty set]] -->
[[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''&nbsp;≥&nbsp;0, there is a collection of [[arity|''n''-''ary'']], or ''n''-''place'', ''[[predicate symbol]]s''. Because they represent [[Finitary relation|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>, ...
* For every integer ''n''&nbsp;≥&nbsp;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>, ...

When the arity of a predicate symbol or function symbol is clear from context, the superscript ''n'' is often omitted.

In this traditional approach, there is only one language of first-order logic.<ref>More precisely, there is only one language of each variant of one-sorted first-order logic: with or without equality, with or without functions, with or without propositional variables, ....</ref> This approach is still common, especially in philosophically oriented books.

A more recent practice is to use different non-logical symbols according to the application one has in mind. Therefore, it has become necessary to name the set of all non-logical symbols used in a particular application. This choice is made via a ''[[signature (logic)|signature]]''.<ref>The word ''language'' is sometimes used as a synonym for signature, but this can be confusing because "language" can also refer to the set of formulas.</ref>

Typical signatures in mathematics are {1, ×} or just {×} for [[group (mathematics)|group]]s,<ref name="Tarski53"/> or {0, 1, +, ×, <} for [[ordered field]]s. There are no restrictions on the number of non-logical symbols. The signature can be [[empty set|empty]], finite, or infinite, even [[uncountable]]. Uncountable signatures occur for example in modern proofs of the [[Löwenheim–Skolem theorem]].

Though signatures might in some cases imply how non-logical symbols are to be interpreted, [[#Semantics|interpretation]] of the non-logical symbols in the signature is separate (and not necessarily fixed). Signatures concern syntax rather than semantics.

In this approach, every non-logical symbol is of one of the following types:

* A ''predicate symbol'' (or ''relation symbol'') with some ''valence'' (or ''arity'', number of arguments) greater than or equal to 0. These are often denoted by uppercase letters such as ''P'', ''Q'' and ''R''. Examples:
** In ''P''(''x''), ''P'' is a predicate symbol of valence 1. One possible interpretation is "''x'' is a man".
** In ''Q''(''x'',''y''), ''Q'' is a predicate symbol of valence 2. Possible interpretations include "''x'' is greater than ''y''" and "''x'' is the father of ''y''".
** Relations of valence 0 can be identified with [[propositional variable]]s, which can stand for any statement. One possible interpretation of ''R'' is "Socrates is a man".
* A ''function symbol'', with some valence greater than or equal to 0. These are often denoted by lowercase [[Latin script|roman letters]] such as ''f'', ''g'' and ''h''. Examples:
** ''f''(''x'') may be interpreted as "the father of ''x''". In [[arithmetic]], it may stand for "-x". In set theory, it may stand for "the [[power set]] of x".
** In arithmetic, ''g''(''x'',''y'') may stand for "''x''+''y''". In set theory, it may stand for "the union of ''x'' and ''y''".
** Function symbols of valence 0 are called ''constant symbols'', and are often denoted by lowercase letters at the beginning of the alphabet such as ''a'', ''b'' and ''c''. The symbol ''a'' may stand for Socrates. In arithmetic, it may stand for 0. In set theory, it may stand for the [[empty set]].

The traditional approach can be recovered in the modern approach, by simply specifying the "custom" signature to consist of the traditional sequences of non-logical symbols.

===Formation rules===
{{seealso|Formal grammar|Formation rule}}
{| class="wikitable collapsible collapsed floatright"
|-
! [[Backus-Naur form|BNF]] grammar
|- 
| <syntaxhighlight lang="bnf">
<index>             ::= "" 
                      | <index> "'"
<variable>          ::= "x" <index>
<constant>          ::= "c" <index>
<unary function>    ::= "f1" <index>
<binary function>   ::= "f2" <index>
<ternary function>  ::= "f3" <index>
<unary predicate>   ::= "p1" <index>
<binary predicate>  ::= "p2" <index>
<ternary predicate> ::= "p3" <index>
<term>              ::= <variable> 
                      | <constant> 
                      | <unary function> "(" <term> ")" 
                      | <binary function> "(" <term> "," <term> ")" 
                      | <ternary function> "(" <term> "," <term> "," <term> ")"
<atomic formula>    ::= "TRUE" 
                      | "FALSE"
                      | <term> "=" <term>
                      | <unary predicate> "(" <term> ")" 
                      | <binary predicate> "(" <term> "," <term> ")" 
                      | <ternary predicate> "(" <term> "," <term> "," <term> ")"
<formula>           ::= <atomic formula> 
                      | "¬" <formula>
                      | <formula> "∧" <formula>
                      | <formula> "∨" <formula>
                      | <formula> "⇒" <formula>
                      | <formula> "⇔" <formula>
                      | "(" <formula> ")"
                      | "∀" <variable> <formula>
                      | "∃" <variable> <formula>
</syntaxhighlight>
|-
| style="width:600px;" | The above [[context-free grammar]] in Backus-Naur form defines the language of syntactically valid first-order formulas with function symbols and predicate symbols up to arity 3. For higher arities, it needs to be adapted accordingly.<ref>{{cite book | author=Eberhard Bergmann and Helga Noll | title=Mathematische Logik mit Informatik-Anwendungen | location=Heidelberg | publisher=Springer | series=Heidelberger Taschenbücher, Sammlung Informatik | volume=187 | year=1977 | language=DE | pages=[https://books.google.com/books?id=I4qfBgAAQBAJ&pg=PA300&redir_esc=y#v=onepage&q&f=false 300–302]}} 
</ref>{{citation needed|reason=A reference to an English textbook is still missing.|date=September 2019}}
|-
| The example formula <code>∀x ∃x' (¬x=c) ⇒ f2(x,x')=c'</code> describes multiplicative inverses when <code>f2'</code>, <code>c</code>, and <code>c'</code> are interpreted as multiplication, zero, and one, respectively.
|}

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====
The set of ''[[Term (logic)|terms]]'' is [[inductive definition|inductively defined]] by the following rules:<ref>G. Takeuti, 'Proof Theory' (1989, p.6)</ref>
# ''Variables''. Any variable symbol is a term.
# ''Functions''. If ''f'' is an ''n''-ary function symbol, and ''t''<sub>1</sub>, ..., ''t''<sub>''n''</sub> are terms, then ''f''(''t''<sub>1</sub>,...,''t''<sub>''n''</sub>) is a term. In particular, symbols denoting individual constants are nullary function symbols, and thus are terms.
Only expressions which can be obtained by finitely many applications of rules 1 and 2 are terms. For example, no expression involving a predicate symbol is a term.

====Formulas====
The set of ''[[formula (mathematical logic)|formulas]]'' (also called ''[[Well-formed formula|well-formed formulas]]''<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.
# ''[[logical equality|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.
# ''Negation''. If <math>\varphi</math> is a formula, then <math>\lnot\varphi</math> is a formula.
# ''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.
Only expressions which can be obtained by finitely many applications of rules 1–5 are formulas. The formulas obtained from the first two rules are said to be ''[[atomic formula]]s''.

For example:
:<math>\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z)))</math>
is a formula, if ''f'' is a unary function symbol, ''P'' a unary predicate symbol, and Q a ternary predicate symbol. However, <math>\forall x\, x \rightarrow</math> is not a formula, although it is a string of symbols from the alphabet.

The role of the parentheses in the definition is to ensure that any formula can only be obtained in one way—by following the inductive definition (i.e., there is a unique [[parse tree]] for each formula). This property is known as ''unique readability'' of formulas. There are many conventions for where parentheses are used in formulas. For example, some authors use colons or full stops instead of parentheses, or change the places in which parentheses are inserted. Each author's particular definition must be accompanied by a proof of unique readability.

====Notational conventions====
For convenience, conventions have been developed about the precedence of the logical operators, to avoid the need to write parentheses in some cases. These rules are similar to the [[order of operations]] in arithmetic. A common convention is:
* <math>\lnot</math> is evaluated first
* <math>\land</math> and <math>\lor</math> are evaluated next
* Quantifiers are evaluated next
* <math>\to</math> is evaluated last.
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>
might be written as:
:<math>(\lnot [\forall x P(x)]) \to \exists x [\lnot P(x)].</math>

===Free 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 &phi; is identified with the initial substring of &phi; 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 &phi; if all occurrences of ''x'' in &phi; 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.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.
; 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 ''φ''
; Binary connectives : ''x'' occurs free in (''φ'' → ''ψ'') if and only if ''x'' occurs free in either ''φ'' or ''ψ''. ''x'' occurs bound in (''φ'' → ''ψ'') if and only if ''x'' occurs bound in either ''φ'' or ''ψ''. The same rule applies to any other binary connective in place of →.
; Quantifiers : ''x'' occurs free in {{math|∀''y'' ''φ''}}, if and only if x occurs free in ''φ'' and ''x'' is a different symbol from ''y''. Also, ''x'' occurs bound in {{math|∀''y'' ''φ''}}, if and only if ''x'' is ''y'' or ''x'' occurs bound in ''φ''. The same rule holds with {{math|∃}} in place of {{math|∀}}.

For example, in {{math|∀''x'' ∀''y'' (''P''(''x'') → ''Q''(''x'',''f''(''x''),''z''))}}, ''x'' and ''y'' occur only bound,<ref>''y'' occurs bound by rule 4, although it doesn't appear in any atomic subformula</ref>  ''z'' occurs only free, and ''w'' is neither because it does not occur in the formula.

Free and bound variables of a formula need not be disjoint sets: in the formula {{math|''P''(''x'') → ∀''x'' ''Q''(''x'')}}, the first occurrence of ''x'', as argument of ''P'', is free while the second one, as argument of ''Q'', is bound.

A formula in first-order logic with no free variable occurrences is called a ''first-order [[sentence (mathematical logic)|sentence]]''. These are the formulas that will have well-defined [[truth value]]s under an interpretation. For example, whether a formula such as Phil(''x'') is true must depend on what ''x'' represents. But the sentence {{math|∃''x'' Phil(''x'')}} will be either true or false in a given interpretation.

===Example: ordered abelian groups===
In mathematics, the language of ordered [[abelian group]]s has one constant symbol 0, one unary function symbol −, one binary function symbol +, and one binary relation symbol ≤. Then:
*The expressions +(''x'', ''y'') and +(''x'', +(''y'', −(''z''))) are ''terms''. These are usually written as ''x'' + ''y'' and ''x'' + ''y'' − ''z''.
*The expressions +(''x'', ''y'') = 0 and ≤(+(''x'', +(''y'', −(''z''))), +(''x'', ''y'')) are ''atomic formulas''. These are usually written as ''x'' + ''y'' = 0 and ''x'' + ''y'' − ''z'' &nbsp;≤&nbsp; ''x'' + ''y''.
*The expression <math>(\forall x \forall y \, [\mathop{\leq}(\mathop{+}(x, y), z) \to \forall x\, \forall y\, \mathop{+}(x, y) = 0)]</math> is a ''formula'', which is usually written as <math>\forall x \forall y ( x + y \leq z) \to \forall x \forall y (x+y = 0).</math> This formula has one free variable, ''z''.

The axioms for ordered abelian groups can be expressed as a set of sentences in the language. For example, the axiom stating that the group is commutative is usually written <math>(\forall x)(\forall y)[x+ y = y + x].</math>