First-order logic, also known as quantification theory and predicate calculus is a term that refers to predicate logics in which quantified predicates may range over a single domain of discourse that contains distinct objects. There are several first order logics, but the most commonly studied is classical first-order logic, which is supposed to be an "extension" of Propositional logic.

Syntax

Alphabet

Logical symbols:

• The Quantifiers: ${\displaystyle \forall,\exists}$ . Respectively, the Universal Quantifier and the Existential Quantifier.
• The logical connectives: ${\displaystyle \and,\or,\neg,\to,\leftrightarrow }$ Respectively, Conjunction, Disjunction, Material conditional, biconditional. Other logical connectives may also be added.
• A set of infinite variables: ${\displaystyle x_1,x_2,x_3,\ldots}$ . They may be identified with letters such as ${\displaystyle x, y, z}$ .
• A set of parentheses and other punctuation marks.

Non-logical symbols

• For every integer n, there is a set of n-ary Predicate symbols: ${\displaystyle P_1,P_2,P_3,\ldots}$ . These may be letters such as ${\displaystyle A,B,C,D,\ldots,Y,Z}$
• For every integer ${\displaystyle n}$ , there is a set of n-ary function symbols.: ${\displaystyle f_1,f_2,f_3,\ldots}$ . If the arity of these symbols is equal to 0, then it is said to be an individual constant. These may be letters such as ${\displaystyle a,b,c,d,\ldots,t,u,v,w}$

Formation rules

Terms: The set of terms is defined as:

• Any expression ${\displaystyle f(t_1,\ldots,t_n)}$ of ${\displaystyle n}$ arguments (where ${\displaystyle t_n}$ is a term and ${\displaystyle f}$ is a function symbol) is a term.
• Individual constants are terms.
• Any variable is a term.

Formulas

• Predicates: If ${\displaystyle P}$ is an n-ary predicate symbols, and ${\displaystyle t_1,\ldots,t_n}$ are terms, then ${\displaystyle P(t_1,\ldots,t_n)}$ is a wff (wff is an abbrevation for a well-formed formula).
• Quantifiers: If ${\displaystyle \phi}$ is a wff and ${\displaystyle x}$ is a variable, then ${\displaystyle \forall x\phi}$ and ${\displaystyle \exists x\phi}$ are wffs.
• Negation: If ${\displaystyle \phi}$ is a wff then ${\displaystyle \neg\phi}$ is a wff.
• Binary connectives: If ${\displaystyle \phi}$ and ${\displaystyle \psi}$ are wffs and ${\displaystyle \Box}$ is a binary connective, then ${\displaystyle \phi\Box\psi}$ is a wff.
• Equality Symbol: if equality is a part of first-order logic and ${\displaystyle \phi}$ and ${\displaystyle \psi}$ are wffs, then ${\displaystyle \phi=\psi}$ is a wff.

Semantics

The non-logical symbols of a first-order logic are usually interpreted with a first-order model, which is an ordered pair ${\displaystyle \mathcal A=(A,\sigma,I)}$ , where ${\displaystyle A}$ is the domain of discourse, is the signature, and ${\displaystyle I}$ is the interpretation function which assigns meaning to the non-logical symbols. The signature is an ordered pair ${\displaystyle \sigma=(\sigma_f,\sigma_r,ar)}$ where ${\displaystyle \sigma_r}$ is the set of predicate or relation symbols, ${\displaystyle \sigma_f}$ is the set of function symbols, and is a mapping ${\displaystyle ar:\sigma_r\cup\sigma_f\to\N}$ which assigns a natural number called an arity. The notation for an interpretation of a non-logical symbol ${\displaystyle x}$ is ${\displaystyle I(x)=x^\mathcal A}$ .

Each predicate symbol or relation symbol ${\displaystyle R}$ is assigned a n-ary relation ${\displaystyle R^\mathcal A\subseteq A^n}$ or equivalently an n-ary function ${\displaystyle R^\mathcal A:D^n \to \mathbb B}$ (where ${\displaystyle \mathbb{B}}$ is the boolean domain or some other truth set).

Each function symbol f is assigned an n-ary function ${\displaystyle f^\mathcal A:D^n\to D}$. If ${\displaystyle f}$ is a nullary function (that is an individual constant) its interpretation is ${\displaystyle f^\mathcal A\in D}$ . Individual constants may be assigned a value, such as ${\displaystyle f^\mathcal A=100}$ .

A T-Schema could be defined inductively in the following way:

• A logical connective is given a truth value based on it's truth function or truth table, just as in Propostional logic.
• Let ${\displaystyle v_1,\ldots,v_n}$ be the evaluations of the terms ${\displaystyle t_1,\ldots,t_n}$. Then ${\displaystyle P(t_1,\ldots,t_n)}$ is true if and only if ${\displaystyle (v_1,\ldots,v_n)\in P^\mathcal{A}}$ . (Function symbols are evalauted in the following way: Given terms ${\displaystyle t_1,\ldots,t_n}$ that have been evaulated to ${\displaystyle d_1,\ldots,d_n}$ , the ${\displaystyle n}$-ary function value ${\displaystyle f(t_1,\ldots,t_n)}$ evaulates to ${\displaystyle f^\mathcal{A}(d_1,\ldots,d_n)}$ .
• ${\displaystyle t_1=t_2}$is true if and only if ${\displaystyle t_1}$ and ${\displaystyle t_2 }$ evaulate to the same ${\displaystyle x \in D}$
• ${\displaystyle \forall x\phi(x)}$ is true if ${\displaystyle \phi(x)}$ for all ${\displaystyle x \in D}$ .
• ${\displaystyle \exists x\phi(x)}$ is true if and only if there exists ${\displaystyle x \in D}$ such that ${\displaystyle \phi(x)}$ .

Rules of inference

The rules of inference for first-order logic depends on what formal system is being used. It is common to add the rules of inference of propositional logic, universal instantiation, universal generalization, existential instantiation, and existential generalization. Formal systems may also include Change of quantifier.

Axioms

If equality is part of a first-order logic system, then reflexivity, symmetry, transitivity, substitution for formulas, substitution for functions are added as axioms.

External links

• First-order logic article on Wikipedia
• First-Order logic on Philosophy wiki