El sistema formal $L$ del cálculo de enunciados se define por:

1. Vocabulario: es un conjunto numerable de simbolos $\{\neg,\rightarrow,(,),p_0,....\}$.
2. Conjunto de formulas bien formadas (fbf). Se define de manera inductiva como sigue.
   1. $p_0$, $p_1$,…. son fbf's
   2. Si $A$ y $B$ son fbf, entonces $(\neg A)$ y $(A\rightarrow B)$ lo son.
   3. El conjunto de fbf's esta definnido aplicando de manera inductiva las dos reglas anteriores (a) y (b).
3. Definiciones:
   1. $(A\wedge B):=(\neg(A\rightarrow(\neg B)))$
   2. $(\vee B):=((\neg A)\rightarrow B)$
   3. $A\rightarrow B:=\neg((A\rightarrow B)\rightarrow(\neg(A\rightarrow B)))$