FANDOM

1,099 Pages

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

• For every integer n, there is a set of n-ary Predicate symbols: $P_1,P_2,P_3,\ldots$ . These may be letters such as $A,B,C,D,\ldots,Y,Z$
• For every integer $n$ , there is a set of n-ary function symbols.: $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 $a,b,c,d,\ldots,t,u,v,w$

Formation rules

Terms: The set of terms is defined as:

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

Formulas

• Predicates: If $P$ is an n-ary predicate symbols, and $t_1,\ldots,t_n$ are terms, then $P(t_1,\ldots,t_n)$ is a wff (wff is an abbrevation for a well-formed formula).
• Quantifiers: If $\phi$ is a wff and $x$ is a variable, then $\forall x\phi$ and $\exists x\phi$ are wffs.
• Negation: If $\phi$ is a wff then $\neg\phi$ is a wff.
• Binary connectives: If $\phi$ and $\psi$ are wffs and $\Box$ is a binary connective, then $\phi\Box\psi$ is a wff.
• Equality Symbol: if equality is a part of first-order logic and $\phi$ and $\psi$ are wffs, then $\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 $\mathcal A=(A,\sigma,I)$ , where $A$ is the domain of discourse, is the signature, and $I$ is the interpretation function which assigns meaning to the non-logical symbols. The signature is an ordered pair $\sigma=(\sigma_f,\sigma_r,ar)$ where $\sigma_r$ is the set of predicate or relation symbols, $\sigma_f$ is the set of function symbols, and is a mapping $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 $x$ is $I(x)=x^\mathcal A$ .

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

Each function symbol f is assigned an n-ary function $f^\mathcal A:D^n\to D$. If $f$ is a nullary function (that is an individual constant) its interpretation is $f^\mathcal A\in D$ . Individual constants may be assigned a value, such as $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 $v_1,\ldots,v_n$ be the evaluations of the terms $t_1,\ldots,t_n$. Then $P(t_1,\ldots,t_n)$ is true if and only if $(v_1,\ldots,v_n)\in P^\mathcal{A}$ . (Function symbols are evalauted in the following way: Given terms $t_1,\ldots,t_n$ that have been evaulated to $d_1,\ldots,d_n$ , the $n$-ary function value $f(t_1,\ldots,t_n)$ evaulates to $f^\mathcal{A}(d_1,\ldots,d_n)$ .
• $t_1=t_2$is true if and only if $t_1$ and $t_2$ evaulate to the same $x\in D$
• $\forall x\phi(x)$ is true if $\phi(x)$ for all $x\in D$ .
• $\exists x\phi(x)$ is true if and only if there exists $x\in D$ such that $\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.