I doubt if there's anything like the best of all possible formal languages for boolean expressions, but there are many ways of coming up with calculi that are more efficient than most of the ones currently in common use.

You might enjoy exploring the possibilities of using [minimal negation operators][1] as the fundamental primitives of a propositional calculus.

A calculus that is very efficient from both conceptual and computational standpoints is based on just two types of logical connectives, both of variable $k$-ary scope.  The formulas of this calculus parse into a family of graph-theoretical data structures whose underlying graphs are called "painted and rooted cacti" (PARCs).  Hence the name "[cactus language][2]" for this style of propositional calculus, in either its traversal string or parse graph forms.


----------

**temporary work area for testing images, latex, unicode …**

<center>

![Cactus Graph Lobe Connective][3]

![Cactus Graph Node Connective][4]

</center>

$$⦗e 1﹐e 2﹐…﹐e k−1﹐e k⦘$$

$$\nu_k (x_1, \ldots, x_k)$$

$$\nu_k (x_1, \ldots, x_k) \quad \iff \quad x_j = 0 ~\text{for exactly one}~ j \in [1, k]$$


  [1]: http://ncatlab.org/nlab/show/minimal+negation+operator
  [2]: http://ncatlab.org/nlab/show/differential+logic#cactus_language_for_propositional_logic_3
  [3]: http://mywikibiz.com/images/5/5e/Cactus_Graph_Lobe_Connective.jpg
  [4]: http://mywikibiz.com/images/9/98/Cactus_Graph_Node_Connective.jpg