Formula

2020 Mathematics Subject Classification: Primary: 03BXX Secondary: 68P05 [MSN][ZBL]

Formulas are syntactically correct expressions in a formalized language defined over a signature, a set of variables, and a logics. In this way, formulas are quite similar to terms. Since predicates and logics symbols are included in their inductive definition, they represent truth values instead of sort values, however.

For examples of the exact definition of the concept of a formula in several formalized languages, see the articles Axiomatic set theory; Arithmetic, formal; Predicate calculus; Types, theory of. In mathematical practice, formulas also have a semantic meaning. They can be either names, or forms of statements, definition-abbreviations, etc.

Definition of Formulas

Let $\Sigma =(S,F)$ be a signature and $P$ be a set of predicate symbols for $S$ with range $\mathbb{B}$ representing the set of truth values of the underlying logics. As usual, it holds $P\cap S=\emptyset$ and $P\cap F= \emptyset$. The notions of arity and type defined for the function symbols $f\in F$ may also be defined for the predicate symbols $p\in P$: Every $p\in P$ is assigned an arity ar$\colon P\longrightarrow \mathbb{N}_0$ giving the number of arguments of $p$. Every predicate symbol $p\in P$ is also assigned a predicate type type$\colon s_1\times\cdots\times s_{ar(p)} \longrightarrow \mathbb{B}$.

Let $X_s$ be a set of free variables of sort $s\in S$ with $X_s\cap F=\emptyset$, $X_s\cap P=\emptyset$, and $X_s\cap S=\emptyset$. Furthermore, let the set of free variables be defined as disjoint union $X:= \bigcup_{s\in S} X_s$. Then the set $Q(\Sigma,P,X)$ of atomic formulas consists of all $p(t_1,\ldots,t_n)$ for predicates $p\in P$ with type$(p)= s_1\times\cdots\times s_{ar(p)}$ and $t_i\in T_{s_i}(\Sigma,X)$. Examples for such predicates $p\in P$ are properties, equalities, inequalities etc. Atomic formulas are also called atoms.

The set $L(\Sigma,P,X)$ of (general) formulas depends on the underlying logics. For PL1, it is the smallest set containing

• the atomic formulas $Q(\Sigma,P,X)$
• the expressions $p_1\vee p_2$, $p_1\wedge p_2$, $\neg p$ for $p,p_1,p_2\in L(\Sigma,P,X)$
• the expressions $\forall x_1\in X_{s_1},\ldots,x_n\in X_{s_n}\colon p(x_1,\ldots,x_n)$ and $\exists x_1\in X_{s_1},\ldots,x_n\in X_{s_n}\colon p(x_1,\ldots,x_n)$ for predicates $p\in P$ with type$(p)= s_1\times\cdots\times s_{ar(p)}$

Identifying and Manipulating Free Variables

Analogous to terms, the existence or nonexistence of free variables in a formula makes a fundamental difference (see for example section Sentences and Atomic Formulas). Thus, procedures for determining and manipulating free variables in formulas exist corresponding to the ones defined for terms. These procedure are somewhat more complicated as in the case of terms, however, for handling the additional logics symbols and the existence of bound variables.

A mapping $V\colon L(\Sigma,P,X) \longrightarrow 2^X$ for identifying the free variables in a formula is inductively defined as follows:

• For a predicate $p(t_1,\ldots,t_n)$ with $p\in P$ of type$(p)= s_1\times\cdots\times s_{ar(p)} $ and terms $t_i\in T_{s_i}(\Sigma,X)$, it holds $V(p(t_1,\ldots,t_n)) := V(t_1)\cup\cdots\cup V(t_n)$
• For a formula $p\in L(\Sigma,P, X)$, it holds $V(\neg p) = V(p)$
• For a formula $p_1,p_2\in L(\Sigma,P, X)$, it holds $V(p_1\vee p_2) = V(p_1)\cup V(p_2)$ and $V(p_1\wedge p_2) = V(p_1)\cup V(p_2)$.
• For a formula $p\in L(\Sigma,P, X)$, it holds $V(\forall x\colon p) = V(p)\setminus \{x\}$ and $V(\exists x\colon p) = V(p)\setminus \{x\}$

Let $p\in L(\Sigma,P,X)$ be a formula, $w\in T(\Sigma,X)$ be a term, and $x\in X$ be a variable. The substitution $p[x\leftarrow w]$ of $x$ with $w$ is inductively defined as follows:

• $x[x\leftarrow w]:= w$
• $y[x\leftarrow w]:= y$ for $y\in X$ with $x\neq y$
• $p(t_1,\ldots,t_n)[x\leftarrow w] := p(t_1[x\leftarrow w],\ldots,t_n[x\leftarrow w])$ for a predicate $p\in P$ of type$(p)= s_1\times\cdots\times s_{ar(p)} $ and terms $t_i\in T_{s_i}(\Sigma,X)$.
• $(\neg p)[x\leftarrow w] = \neg (p[x\leftarrow w])$ for a formula $p\in L(\Sigma,P, X)$
• $(p_1\vee p_2)[x\leftarrow w] = p_1[x\leftarrow w]\vee p_2[x\leftarrow w]$ and $(p_1\wedge p_2)[x\leftarrow w] = p_1[x\leftarrow w]\wedge p_2[x\leftarrow w]$ for formulas $p_1,p_2\in L(\Sigma,P, X)$
• $(\forall y\colon p)[x\leftarrow w] = \forall y\colon p[x\leftarrow w]$ and $(\exists y\colon p)[x\leftarrow w] = \exists y\colon p[x\leftarrow w]$ for a formula $p\in L(\Sigma,P, X)$ and a variable $y\in X$, $y\neq x$
• $(\forall x\colon p)[x\leftarrow w] = \forall x\colon p$ and $(\exists x\colon p)[x\leftarrow w] = \exists x\colon p$ for a formula $p\in L(\Sigma,P, X)$

The last rule of the definition holds, since $x$ is already used as a bound variable in the quantified expressions. Multiple substitutions $p[x_1\leftarrow w_1,\ldots, x_n\leftarrow w_n]$ can be defined analogously. One has to note, that the substitutions of $x_1,\ldots,x_n$ with $w_1,\ldots,w_n$ are executed simultaneously and not consecutively. Otherwise, in the case of $x_j\in V(w_k)$, different results have to be expected.

Sentences and Atomic Formulas

A formula $p\in L(\Sigma,P,X)$ is called closed, if $V(p)= \emptyset$. Closed formulas are also called sentences or, more precisely, $\Sigma$-sentences. They do not necessarily belong to the set $L(\Sigma,P,\emptyset)$, however, because bound variables can exist in $p$ (e.g. quantifier variables). For a $\Sigma$-formula $p(x_1,\ldots,x_n)\in L(\Sigma,P,X)$ with free variables $x_i\in X_{s_i}$ of sorts $s_i\in S$, its universal closure gives a $\Sigma$-sentence $\forall x_1\in X_{s_1}\cdots \forall x_n\in X_{s_n} \colon p(x_1,\ldots,x_n)$ [W90]. Sentences may assigned a fixed truth value contrary to general formulas. Since one can instantiate free variables with any truth value, the truth value of a general formula can vary according to the specific instantiation as well.

An atom $p(t_1,\ldots,t_n)\in Q(\Sigma,P,X)$ is called a ground atom, if the terms $t_i$ do not contain a free variable (i.e. if $V(t_i)=\emptyset$ for $i=1,\ldots,n$). The ground atoms are the closed atomic formulas. They are also called atomic sentences. Sentences are defined inductively based on atomic sentences by application of connective and quantifier symbols.

Morphisms

A signature morphism $m\colon \Sigma_1\longrightarrow \Sigma_2$ can be extended to a morphism between formulas, if some weak additional assumptions are fulfilled. This shows that basically the existence of a signature morphism suffices to relate the formalized languages of formulas (and terms) defined over $\Sigma_1$ and $\Sigma_2$ as well. The extension of $m$ is composed of the following parts:

• For the terms contained in a formula, the corresponding extension of $\sigma$ to terms have to be used.
• For predicates, some kind of compatibility is required.
• Connectives and quantifiers remain unchanged.

Formally, this leads to the following statement: Let $m\colon \Sigma_1\longrightarrow \Sigma_2$ be a signature morphism for signatures $\Sigma_1=(S_1,F_1), \Sigma_2=(S_2,F_2)$. The morphism $m$ may be extended to a mapping, which is defined for sets $X = \bigcup_{s\in S_1} X_s$, $X'= \bigcup_{s\in S_2} X_s'$ of variables as well with $m(x)\in X'_{m(s)}$ for $x\in X_s$, $s\in S_1$. Furthermore, the extension may be defined also for predicates $P_1$ defined over $S_1$ and $P_2$ defined over $S_2$ such that the predicate type is preserved under $m$ according to $\forall p\in P_1\colon \mbox{type}(m(p)) = m_S(\mbox{type}(p)) := m_S(s_1)\times\cdots\times m_S(s_{ar(p)}) \longrightarrow m_S(s)$ for predicates $p\in P_1$ with type$(p)= s_1\times\cdots\times s_{ar(p)}$. Then the signature morphism $m$ can also be extended to a morphism $m^\ast\colon L(\Sigma_1,P_1,X)\longrightarrow L(\Sigma_2,P_2,X')$ between formulas. Such an extension is called a translation as in the case of terms.

References

[EM85]	H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 1, Springer 1985
[EM90]	H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 2, Springer 1990
[M89]	B. Möller: "Algorithmische Sprachen und Methodik des Programmierens I", lecture notes, Technical University Munich 1989
[W90]	M. Wirsing: "Algebraic Specification", in J. van Leeuwen: "Handbook of Theoretical Computer Science", Elsevier 1990