<p>I am looking for the original reference for the following statement:</p>
<blockquote>
<p>Let <span class="math-container">$P$</span> be a propositional proof system containing <span class="math-container">$EF$</span>. Then <span class="math-container">$P$</span> is equivalent to <span class="math-container">$EF+Sound(P)$</span>.</p>
</blockquote>
<hr />
<h3>Background</h3>
<p>A propositional proof system (pps) <span class="math-container">$Q$</span> can thought of as an nondeterministic algorithm for <span class="math-container">$TAUT$</span> (a certificate for a tautology is called a <span class="math-container">$Q$</span>-proof for that formula).</p>
<p>A <span class="math-container">$Frege$</span> 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. <span class="math-container">$\land, \lor, \lnot$</span>) and a finite  complete set of deduction rules and axioms. <em>Extended Frege</em>, usually denoted by <span class="math-container">$EF$</span> or <span class="math-container">$EFrege$</span>, 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 <em>Circuit Frege</em> (denoted by <span class="math-container">$CF$</span> and <span class="math-container">$CFrege$</span>) and has circuits as its lines in place of formulas (refer to Emil Jeřábek's thesis for the definition of <span class="math-container">$CFrege$</span>).</p>
<p>Soundness formula for a pps <span class="math-container">$Q$</span>, denoted by <span class="math-container">$Sound(P)$</span> is the (family of) propositional tautologies that express the soundness of <span class="math-container">$Q$</span>, i.e.</p>
<blockquote>
<p>if <span class="math-container">$\varphi$</span> is provable in <span class="math-container">$Q$</span> then <span class="math-container">$\varphi$</span> is true.</p>
</blockquote>
<p>More explicitly</p>
<blockquote>
<p>if <span class="math-container">$\pi$</span> is a <span class="math-container">$Q$</span>-proof of <span class="math-container">$\varphi$</span> and <span class="math-container">$\tau$</span> is a truth assignment then <span class="math-container">$\tau$</span> satisfies <span class="math-container">$\varphi$</span>.</p>
</blockquote>
<p>In symbols</p>
<blockquote>
<p><span class="math-container">$\pi : Q \vdash \varphi \implies \tau \vDash \varphi$</span>.</p>
</blockquote>
<p>The parameter for the family is the length of the proofs. Soundness is also known as the <em>Reflection</em> 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.</p>
<p>The choice of <span class="math-container">$EF$</span> 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.</p>
<p>The statement in the question is essentially saying that the soundness tautology for <span class="math-container">$Q$</span> is universal/complete for <span class="math-container">$Q$</span>.</p>

CC BY-SA 3.0
2012-09-23T01:30:44.080Z
Can you explain a little more about background for people who are not used to logic?  What is EF?
Tsuyoshi Ito
CC BY-SA 3.0
2012-10-20T19:32:00.597Z
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.
Kaveh
<cc.complexity-theory><reference-request><proof-complexity><soundness>
Reference for a propositional proof system being equivalent to its soundness?
Kaveh
# Reference for a propositional proof system being equivalent to its soundness?

(Asked by: username_0 on 2012-09-22)

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$.

**Tags:** cc.complexity-theory, reference-request, proof-complexity, soundness

> **Comments:**
> **username_1**: Can you explain a little more about background for people who are not used to logic?  What is EF?  
> **username_0**: 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.  

---

## 0 answers

