9
$\begingroup$

I am looking for the original reference for the following statement:

Let $P$ be a propositional proof system containing $EF$. Then $P$ is equivalent to $EF+Sound(P)$.


Background

A propositional proof system (pps) $Q$ can thought of as an nondeterministic algorithm for $TAUT$ (a certificate for a tautology is called a $Q$-proof for that formula).

A $Frege$ system is a pps similar to those used in the logic textbooks. It has lines which are formulas (using an adequate set of connectives, e.g. $\land, \lor, \lnot$) and a finite complete set of deduction rules and axioms. Extended Frege, usually denoted by $EF$ or $EFrege$, is the pps resulting from adding the extension rule (which allows introducing new propositional variable as shorthand for formulas, i.e. it allows definitions). An equivalent system which might be easier conceptually to imagine is Circuit Frege (denoted by $CF$ and $CFrege$) and has circuits as its lines in place of formulas (refer to Emil Jeřábek's thesis for the definition of $CFrege$).

Soundness formula for a pps $Q$, denoted by $Sound(P)$ is the (family of) propositional tautologies that express the soundness of $Q$, i.e.

if $\varphi$ is provable in $Q$ then $\varphi$ is true.

More explicitly

if $\pi$ is a $Q$-proof of $\varphi$ and $\tau$ is a truth assignment then $\tau$ satisfies $\varphi$.

In symbols

$\pi : Q \vdash \varphi \implies \tau \vDash \varphi$.

The parameter for the family is the length of the proofs. Soundness is also known as the Reflection in the proof complexity literature. We say two ppses are equivalent when the size of shortest proofs of tautologies in them are polynomially related, i.e. each one can simulate the other one with at most a polynomial proof size increase.

The choice of $EF$ is not essential for the equivalence in the question and one can take a weaker pps like Resolution (with some modifications). AFAIK this stronger version is first stated by Jan Krajicek.

The statement in the question is essentially saying that the soundness tautology for $Q$ is universal/complete for $Q$.

$\endgroup$
  • 3
    $\begingroup$ Can you explain a little more about background for people who are not used to logic? What is EF? $\endgroup$ – Tsuyoshi Ito Sep 23 '12 at 1:30
  • $\begingroup$ I have found statements similar to this in Jan Krajicek's recent book "Forcing with Random Variables and Proof Complexity", I am still looking older references. $\endgroup$ – Kaveh Oct 20 '12 at 19:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.