Solution of the WoLLIC 2005 Problem

There are 400 Theories with 4 Propositional Symbols

I would like to thank very much all the participants. We had three correct solutions to the WoLLIC 2005 Problem.

Alasdair Urquhart

Prof. Dr. Alasdair Urquhart (Contact, Photo, Bibliography) pointed to the solution obtained by George Polya (in portuguese) author of the famous book How to solve it.

He also pointed to the book Harrison, M. A. Introduction to Switching and Automata Theory. New York: McGraw-Hill, p. 188, 1965, that gives the solution for the 5 and 6 propositional symbols cases (respectively, 1,228,156 and 400,507,806,843,726).

A copy of Polya's paper can be obtained here.

Date: Sat, 2 Jul 2005 10:57:58 -0400
From: Alasdair Urquhart <>
Subject: WoLLIC'05 problem

A theory in a finite number of propositional symbols
can be axiomatized by a single axiom, and any two
such theories are logically equivalent if and only if
their single axioms are logically equivalent.
The problem is therefore equivalent to asking how
many non-equivalent formulas there are in 4 variables,
excluding tautologies and contradictions.

This problem was solved by George Polya (Journal of
Symbolic Logic Volume 5 (1940), pp. 98-103).  Polya showed
that there are 402 distinct Boolean formulas with respect to
the group of permutations and complementations.
The answer to the problem is therefore 400.

More extensive computations are in Michael Harrison's
book "Introduction to Switching and Automata Theory."

Alasdair Urquhart

Vaughan Pratt

Prof. Dr. Vaughan Pratt sent us a very interesting solution in the form of a small C program that calculates the correct answer. He also kindly sent an explanation of how the program works.

He also pointed to the paper: Pratt, V.R., and L.J. Stockmeyer, A Characterization of the Power of Vector Machines, JCSS, 12, 2, 1976, 198-221, where his solution found applications.

Date: Tue, 12 Jul 2005 23:00:52 -0700
From: Vaughan Pratt <>
Subject: WoLLIC'05 problem

Dear Guilherme,

Thanks for your clarification of the problem.  The attached program 
reports 400 theories.

Best regards,

Vaughan Pratt

Marcus Ritt

Dipl.-Inform. Marcus Ritt sent us the correct answer and pointed to relevant papers, among them a recent one (J. Feldman, A catalog of boolean concepts, J. of Mathematical Psychology 47, 2003) that discuss some psychological properties of related Boolean concepts.

Date: Tue, 19 Jul 2005 22:45:37 -0300
From: Marcus Ritt 
Subject: WoLLIC'05 problem

|L_4|=400; all boolean functions of four variables can be visualized as
subsets of the vertices of the 4-cube; if we disregard permutation or
negation of propositional variables we ask for the number of unique
configurations modulo automorphisms of the 4-cube. Pólya shows in [1]
how to approach this kind of counting problem; [2] contains the explicit
solution for this problem. A nice list of all configurations is given in

[1] G. Pólya, Anzahlbestimmungen von Gruppen, Graphen und chemischen
Verbindungen, Acta Math. 68, 145-254, 1937.
[2] G. Pólya, Sur les types des propositiones composées, J. Symbolic
Logic 5-3, 98-103, 1940.
[3] J. Feldman, A catalog of boolean concepts, J. of Mathematical
Psychology 47, 2003.


Marcus Ritt
Prof. Cristiano Fischer 120/407, Petrópolis
91410-000 Porto Alegre
RS, Brazil


To my surprise and delight the problem proved to be relevant to Logic, as George Polya's pre-computational era solution shows, and methods for solving it to Information and Computation, as the applications of Prof. Pratt solution in the characterization of the power of Vector Machines and in the implementation of Sun's Pixrect graphics interface shows. Finally, the paper pointed by Dipl.-Inform. Marcus Ritt completes the WoLLIC acronym showing the relevance of the problem with respect to Language.

To end in a philosophical note, I would like to evoke Ludwig Wittgenstein (1889-1951). In his 1922 Tractatus Logico-Philosophicus, the "young" Wittgenstein states that philosophical problems arise because of misuse of language, and it is only when we understand everyday language that these questions may be dealt with:

(...) The whole sense of the book might be summed up the following words: what can be said at all can be said clearly, and what we cannot talk about we must pass over in silence. Thus the aim of the book is to draw a limit to thought, or rather - not to thought, but to the expression of thoughts: for in order to be able to draw a limit to thought, we should have to find both sides of the limit thinkable (i.e. we should have to be able to think what cannot be thought). It will therefore only be in language that the limit can be drawn, and what lies on the other side of the limit will simply be nonsense. (...)

If we lived in a 4 bits world and if we only had propositional logic as a language, whatever the meaning these 4 bits could have to us, all that we would be able to "say clearly" to each other would be those 400 theories and "wovon man nicht sprechen kann, darüber muß man schweigen." (whereof one cannot speak, thereof one must be silent.)

PS: How the idea of the problem came to me can be found here.