# Mathematical Foundation of a Functional Implementation of the CNF Algorithm
## 2 Basic Definitions and Preliminary Results  
In this section, we list the main definitions of the basic concepts that will be used in the development of this work, as well as the essential results needed in it.  
Here, the concept of sentencial or propositional language is that of [PERSON] in [10] (see also [11; 12]), but our functors (in the sense of [PERSON] in [8]) will be A and K. Moreover, it is necessary to impose that \(X\), the set of atomic or propositional variables, be a nonfinite numerable set; its elements are notated by the last lower-case letters of the latin alphabet: \(x\), \(y\), \(z\), etc., subindicating them if necessary. We will call \(\mathbf{L_{KA}}\) the above  
Figure 1: Axiom and rules for the definition of \(\mathrm{dak}\).  
Figure 2: Axiom and rules for the definition of \(\mathrm{las}\).  
propropositional language and \(P(L_{KA})\), or simply \(P(L)\), the set of its formulas or sentences. The reader should be thoroughly familiar with the principle of induction for sentences, the construction sequence for sentences, and the unique readability principle. We will also assume the knowledge of the principle of finite induction in its different formulations, as it is exposed, for example, in [6].  
The statements of some particular results (lemmas and theorems), in this and subsequent sections, will be given without complete proofs, because some of them are quite evident, and the rest could be carried out using the principle of finite induction, taking into account, in a meticulous and orderly manner, all the possible cases that can occur, in a similar way as it is carried out in the selected proofs included in this paper.  
Given a set \(\Delta\) of formulas of the language \(L\), consider the smallest set of formulas that, containing it, is at the same time closed for the functors \(A\) (resp. \(K\)); it will be represented by \(A(\Delta)\) (resp. \(K(\Delta)\)). Thus, the elements of \(K(A(X))\) are exactly the set of formulas in _conjunctive normal form_. _Clauses_ are exactly the formulas of the smallest set, \(al(X)\), containing \(X\) and being closed for the functor \(A\) whenever it operates on an element of \(X\) to its right. The set \(kl(X)\) (resp. \(lcnf(X)\)) is the smallest set containing \(X\) (resp. \(al(X)\)) and being closed for the functor \(K\) whenever it operates on an element of \(X\) (\(al(X)\)) to its right.  
Note that \(al(X)\cup kl(X)\subseteq lcnf(X)\) and that \(lcnf(X)\subseteq K(A(X))\).  
For all \(\alpha\in P(L_{KA})\) let \(\operatorname{comp}(\alpha)\) (complexity), the natural value defined as follows:  
\[\operatorname{comp}(\alpha)=\begin{cases}0,&\text{if }\alpha\in X,\\ 1+\operatorname{comp}(\varphi)+\operatorname{comp}(\psi),&\text{if }\alpha\equiv A \varphi\psi\text{ or }\alpha\equiv K\varphi\psi.\end{cases}\]  
and \(\operatorname{comp}_{k}(\alpha)\) (complexity in \(K\)) defined by  
\[\operatorname{comp}_{k}(\alpha)=\begin{cases}0,&\text{if }\alpha\in X,\\ \operatorname{comp}_{k}(\varphi)+\operatorname{comp}_{k}(\psi),&\text{if }\alpha \equiv A\varphi\psi,\\ 1+\operatorname{comp}_{k}(\varphi)+\operatorname{comp}_{k}(\psi),&\text{if } \alpha\equiv K\varphi\psi.\end{cases}\]  
If necessary, consider \(\operatorname{comp}_{a}(\alpha)\) as the dual concept of \(\operatorname{comp}_{k}(\alpha)\).  
Consider the semantic consequence \(\models\) in the classical sense, as in, for example, Ref. [5]. The formula \(\alpha\) and \(\beta\) are _equivalent_, in symbols \(\alpha=\beta\), iff by definition \(\alpha\models\beta\) and \(\beta\models\alpha\). In the following, we will use the symbol \(=\) to indicate equivalence and the symbol \(\equiv\) to indicate syntactic equality (verbatim equal). It is well known that if \(\alpha=A\,\varphi\psi\) and \(\beta=A\,\varphi\xi\), then \(A\,\varphi\,K\,\psi\xi=K\,\alpha\beta\).  
It is well know as a basic theorem of classical logic that if \(\alpha=A\,\varphi\psi\) (resp. \(\alpha=K\varphi\psi\)), then \(A\varphi A\psi\xi=A\alpha\xi\) (resp. \(K\varphi K\psi\xi=K\alpha\xi\)).