Calculational solutions to combinatorial problems

Many numerical identities are proved applying clever but informal combinatorial arguments. A way of proving these identities by a formal representation that closely follows these arguments is presented. Operationals, the main formal tool we use for this purpose, are basically, an abstract and axiomatic generalization of the Sigma (Σ) notation used to express and manipulate summations and counts. Operationals are endowed with algebraic properties that allow performing various natural operations that have a combinatorial significance. In this paper, we give a formal version of the typical combinatorial proof of the Inclusion-Exclusion theorem and some more examples showing how to formally interpret, in a practical way, combinatorial arguments used in the literature.