2.1 A simple logical formalism

  The vocabulary of our simple logical formalism is composed of :

• $\land$, $\lor$, $\neg$ connectors and $\forall$, $\exists$ quantification symbols,
• a set of logical variables and a set of logical constants,
• a set of predicates (equality, etc).

The values domain of logical variables and constants is composed of integers, strings, sets, lists, tables, etc. Before defining logical formulae, we define terms that compose a logical formula :

• a logical variable is a term (if this variable is referenced under a quantification symbol),
• if f is a logical constant in n arguments and t₁,...,t_n some terms then f(t₁,...,t_n) is a term.

Definition of logical formula :

• if P is a predicate in n arguments and t₁,...,t_n some terms then P(t₁,...,t_n) is a (atomic) formula,
• if A is a formula then $\neg A$ is a formula,
• if A is a formula, t a term and x a logical variable then $(\forall x \in t\verb*+ + \vert \verb*+ + A)$ and $(\exists x \in t \verb*+ + \vert \verb*+ + A)$ are formulae,
• if A and B are formulae then $A \land B$ and $A \lor B$ are formulae.

We introduce another notation often used in logic and named the conditional operator. The logical definition of it is :  

$$\mbox{IF } c \mbox{ THEN } a \mbox{ ELSE } b \verb*+ + \rightarrow \verb*+ + (c \land a) \lor (\neg c \land b)$$ (1)