[FOM] FTGI1:Classical Propositional Calculus

[Alasdair Urquhart]

Here are some brief comments on Harvey Friedman's
first posting in his new FTGI series.  They all relate
to complexity aspects of CPC.

> 4. Nevertheless, there seems to be a cost in doing this, as 
> mathematicians find it very convenient to use "not". Is there 
> anything to be gained by removing "not"?

In complexity theory, yes!  We have exponential lower
bounds for monotone circuits for NP-complete problems
(due to deep results of Razborov, Boppana, Sipser, and others),
but we have only very weak (linear) lower bounds for the
size of general circuits.  

> It is well known (due to Cook, who is an FOM subscriber) that testing 
> for tautologies is co-NP complete. So P = NP is equivalent to 
> "tautologies can be tested in polynomial time".
> 
> One should be able to prove that no simple minded polynomial time 
> algorithm for testing tautologies. For instance, one might do the 
> following. It is more convenient to think about satisfiability. Take 
> an atom that appears, and split into two formulas, the first obtained 
> by replacing the atom by T and simplifying, and the second obtained 
> by replacing the atom by F and simplifying. Continue in this way, 
> with the second atom, getting four nodes. Continue through all nodes. 
> In theory one may have an exponential tree. However, generally some 
> of the nodes that are not too high off of the root (root at the 
> bottom) are going to have formulas that have been fully resolved as T 
> or F. Of course, if any are resolved as T then the original formula 
> is satisfiable. So in general, we hope that either that happens, 
> instead we get a lot of F's, and the tree may well have paths of 
> length = to the number of distinct atoms in the original formula, but 
> still has far fewer than exponentially many nodes.
> 
> Presumably such schemes have been analyzed for SAT in the literature, 
> and shown to fail, in that sometimes the tree is exponential. Has the 
> literature also discussed anything about the distribution of the 
> sizes of these trees over the input formulas?

The scheme above, when it is applied to formulas in CNF (sets of clauses),
is the well known procedure sometimes called the "Davis-Putnam procedure",
and sometimes "DLL procedure" (after "Davis, Logemann and Loveland").
There are well known examples where a refutation tree for a contradictory
set of clauses has to be of exponential size.

One of the most interesting cases is where we choose sets of clauses
with k literals at random.  Then if the set of clauses is not too big,
say of size cn, where c > 5, and n is the number of variables, then
almost surely, it is unsatisfiable, but any refutation tree has size
exponential in n.  Quite a lot of work has been done recently
on how hard the random instances are as you increase the number of 
clauses.  For some recent results, see, for example, the paper of
Achlioptas, Beame and Molloy, Proceedings of STOC 2001: "A sharp
threshold in proof complexity."

> For that matter, what results are there concerning the number of 
> formulas of a given size that are tautologies? Is it conceivable that 
> we could get an exact count of this efficiently without butting up 
> against P = NP and the like?

This is probably not a very good question for formulas of conventional
structure.  The random clause model mentioned above seems to give
a better model of "random contradictions," or "random tautologies."

For FOM subscribers interested in these topics, I strongly recommend
the excellent recent book by Peter Clote and Evangelos Kranakis,
"Boolean Functions and Computation Models", Springer 2002.

Alasdair Urquhart