Formula

Atomic Formula

A finite sequence (or string) of symbols is an atomic formula of $\mathcal{L}$ iff it is one of the following forms: (i) $t_1=t_2$, where $t_1$ and $t_2$ are terms; (ii) $r(t_1,\dots ,t_n)$, where r is an $n$-ary relation symbol and the $t_i$ are terms.

Formula

A finite sequence of symbols is a formula of $\mathcal{L}$ iff it is one of the following forms: (i) an atomic formula; (ii) $(\neg \phi )$, where $\phi$ is a formula; (iii)${\phi }_1\wedge {\phi }_2$ where ${\phi }_1$ and ${\phi }_2$ are formulas; (iv) $\forall v\phi$ where $v$ is a variable and $\phi$ is a formula

Remark

Here we consider primitive logical symbol as $\neg \wedge \forall$. So we have other property as $({\phi }_1\vee {\phi }_2),({\phi }_1\to {\phi }_2),({\phi }_1\leftrightarrow {\phi }_2)$ where ${\phi }_1$ and ${\phi }_2$ are formulas, $\exists v\phi$ where $v$ is a variable and $\phi$ is a formula.

Formula Complexity Function

For formulas define the formula complexity function $h$ by: $h(\phi )=1$ if $\phi$ is atomic; $h(\neg \phi )=1+h(\phi )$; $h(\forall v\phi )=1+h(\phi )$; $h(\phi \wedge \psi )=1+\max \{h(\phi ),h(\psi )\}$,

Subformula

The set of subformulas of a given formula is defined inductively. In particular, the set of subformulas:

• of an atomic formula just contains the formula itself,
• of $\neg \phi$ is $\{\neg \phi \}\cup \{\text{subformulas of }\phi \}$,
• of $\phi \wedge \psi$ is $\{\phi \wedge \psi \}\cup \{\text{subformulas of }\phi \}\cup \{\text{subformulas of }\psi \}$,
• of $\forall v\phi$ is $\{\forall v\phi \}\cup \{\text{subformulas of }\phi \}$.