A Propositional Proof System for Log Space

The proof system G∗ 0 of the quantified propositional calculus corresponds to NC1 , and G∗ 1 corresponds to P, but no formula-based proof system that corresponds log space reasoning has ever been developed. This paper does this by developing GL∗ . We begin by defining a class ΣCNF(2) of quantified formulas that can be evaluated in log space. Then GL∗ is defined as G∗ 1 with cuts restricted to ΣCNF(2) formulas and no cut formula that is not quantifier free contains a non-parameter free variable. To show that GL∗ is strong enough to capture log space reasoning, we translate theorems of ΣB 0 -rec into a family of tautologies that have polynomial size GL∗ proofs. ΣB 0 -rec is a theory of bounded arithmetic that is known to correspond to log space. To do the translation, we find an appropriate axiomatization of ΣB 0 -rec, and put ΣB 0 -rec proofs into a new normal form. To show that GL∗ is not too strong, we prove the soundness of GL∗ in such a way that it can ...

• Type: Conference
• Year: 2005
• Where: CSL
• Authors: Steven Perron
• Keywords: CSL 2005, Log Space, Log Space Reasoning, Propositional Calculus Corresponds