Editing First-order logic (section)

===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>