\documentclass{article}

\usepackage{latexsym,psfig,epic,eepic,alltt}

% \usepackage{prentcsmacro}

\usepackage[T1]{fontenc}

\input{/home/professores/gb/Pub/laser}

\begin{document}

\title{Solution of the WoLLIC 2005 Problem}

\author{There are 400 Theories with 4 Propositional Symbols}

\date{}

\maketitle

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

\section*{First Winner}

Prof. Dr.
Alasdair Urquhart \\
{\bf Contact}: {\tt http://www.cs.toronto.edu/DCS/People/Faculty/urquhart.html} \\
{\bf Photo}: {\tt http://andrej.com/mathematicians/U/Urquhart\_Alasdair.html} \\
{\bf Bibliography}: {\tt http://sun3.lib.uci.edu/eyeghiay/Philosophy/Colloquia/urquhart.html}
pointed to the solution obtained by George Polya
{\tt http://www-groups.dcs.st-and.ac.uk/~history/Mathematicians/Polya.html}
{\tt
  http://www.educ.fc.ul.pt/docentes/opombo/seminario/polya/biografia.htm}
author of the famous book {\tt http://www.cis.usouthal.edu/misc/polya.html}{\it How to solve it}

A copy of the paper can be obtained here.

\begin{verbatim}

Date: Sat, 2 Jul 2005 10:57:58 -0400
From: Alasdair Urquhart <urquhart@cs.toronto.edu>
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

\end{verbatim}

\section*{Second Winner}

Prof. Dr. Vaughan Pratt \\
{\tt http://boole.stanford.edu/pratt.html}
sent us a very interesting solution in the form of a small C program
the calculates the correct answers. He also kindly sent an explanation
of how the program works.

\begin{verbatim}

Date: Tue, 12 Jul 2005 23:00:52 -0700
From: Vaughan Pratt <pratt@cs.stanford.edu>
Subject: WoLLIC'05 problem

Dear Guilherme,

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

Best regards,

Vaughan Pratt

\end{verbatim}

\section*{Motivation}

I found the problem when I was looking for a unique syntactical
representation for propositional theories to be used in Belief Change
operations. This led me the Prime Implicants/Implicates representation
and from there to the observation that they can be classified in
equivalence classes if we ignore the specific identities and signs of
the propositional symbols.

More details of how these classes were calculated can be found here.

A complete list of the 221 prime implicants/implicates pairs that
represent the 400 possible theories with 4 propositional symbols,
together with some interesting properties, can be found here.

\section*{Conclusion}

To my delight and surprise the problem proved to be relevant to pure
{\it Logic}, as George Polya's pre-computational era solution shows,
and to {\it 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.

To complete the WoLLIC acronym we need {\it Language}. I'll try to
fill the gap. In his 1922 {\it 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:

\begin{quote}
  
  (...) 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.  (...)
  
\end{quote}

Im this context, if we lived in a 4 bits world and if we only had
propositional logic as a language, all that could be ``said clearly''
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.)

\end{document}