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.
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 <firstname.lastname@example.org> 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
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 <email@example.com> Subject: WoLLIC'05 problem Dear Guilherme, Thanks for your clarification of the problem. The attached program reports 400 theories. Best regards, Vaughan Pratt
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  how to approach this kind of counting problem;  contains the explicit solution for this problem. A nice list of all configurations is given in .  G. Pólya, Anzahlbestimmungen von Gruppen, Graphen und chemischen Verbindungen, Acta Math. 68, 145-254, 1937.  G. Pólya, Sur les types des propositiones composées, J. Symbolic Logic 5-3, 98-103, 1940.  J. Feldman, A catalog of boolean concepts, J. of Mathematical Psychology 47, 2003. Regards, ================================================================================ 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.