Abstract
Johannes Köbler and Jochen Messner
Abstract:
We investigate the question whether there is a (p-)optimal proof system for
SAT or for TAUT and its relation to completeness and collapse results for
nondeterministic function classes. A p-optimal proof system for SAT is shown to
imply (1) that there exists a complete function for the class of all total
nondeterministic multi-valued functions and (2) that any set with an optimal
proof system has a p-optimal proof system. By replacing the assumption of the
mere existence of a (p)optimal proof system by the assumption that certain
proof systems are (p-)optimal we obtain stronger consequences, namely
collapse results for various function classes. Especially we investigate
the question whether the standard proof system for SAT is p-optimal.
We show that this assumption is equivalent
to a variety of complexity theoretical assertions studied before, and to the
assumption that every optimal proof system is p-optimal. Finally, we
investigate whether there is an optimal proof system for TAUT that admits
an effective interpolation, and show some relations between various
completeness assumptions.