View source for Formula



{{MSC|03BXX|68P05}} 

{{TEX|done}}

Formulas  are syntactically correct expressions in a [[Formalized language|formalized language]] defined  over a [[Signature (Computer Science)|signature]], a set of variables, and a logics. In this way,  formulas are quite similar to [[Term (Formalized Language)|terms]]. Since predicates and logics symbols  are included in their inductive definition, they represent [[Truth value|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|Axiomatic set theory]];  [[Arithmetic, formal|Arithmetic, formal]]; [[Predicate  calculus|Predicate calculus]]; [[Types, theory of|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 <i>arity</i> ar$\colon  P\longrightarrow \mathbb{N}_0$ giving the number of arguments of $p$.  Every predicate symbol $p\in P$ is also assigned a <i>predicate  type</i> 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 <i>atomic formulas</i>  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 <i>atoms</i>.

The set  $L(\Sigma,P,X)$ of (general) <i>formulas</i> 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  [[Formula#Sentences and Atomic Formulas|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 <i>substitution</i>  $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 <i>closed</i>, if  $V(p)= \emptyset$. Closed formulas are also called  <i>sentences</i> or, more precisely, <i>$\Sigma$-sentences</i>. 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 <i>universal closure</i> 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)$ {{Cite|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 <i>ground  atom</i>, 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 <i>atomic  sentences</i>.  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 language|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 <i>translation</i> as in the  case of terms.

===References===

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