<p>Tseitin tautologies are unsatisfiable systems of linear equations over <span class="math-container">$\mathbb F_2$</span>, and as such they can be refuted just by summing all the equations together (possibly after reconstructing the equations from a CNF encoding, depending on how exactly they are formulated). This provides a trivial proof in <span class="math-container">$\mathrm{Res}(\oplus)$</span> (resolution with linear equations over <span class="math-container">$\mathbb F_2$</span>, i.e., parities of sets of literals), which is a subsystem of <span class="math-container">$F_d(\oplus)$</span> (constant-depth Frege with parity gates), which is p-simulated by Frege. The crux of the Frege proof is to take polynomial-size formulas for parity, and construct short proofs of their basic properties.</p>

CC BY-SA 4.0
2023-11-10T09:11:53.310Z
2023-11-10T09:11:53.310Z
Emil Jeřábek
<p>Section 6 of the following paper has a sketch:</p>
<blockquote>
<p>Alasdair Urquhart. Hard examples for resolution. Journal of the ACM,
34(1):209–219, 1987. DOI: <a href="https://doi.org/10.1145/7531.8928" rel="noreferrer">https://doi.org/10.1145/7531.8928</a></p>
</blockquote>

CC BY-SA 4.0
2023-11-09T22:32:40.047Z
2023-11-09T22:32:40.047Z
Emre Yolcu
<p>There's a vast literature about super-polynomial lower bounds on proof lengths of Tseitin formulas in bounded-depth Frege systems, but what I'm curious about is: what if we don't restrict the depth of the proof? I found a <a href="https://www.doc.ic.ac.uk/%7Eitzamere/R-lin.pdf" rel="nofollow noreferrer">paper</a> which claims that Tseitin formulas have a polynomial-size proof in the R(lin) (Resolution over Linear Equations) proof system, which was found to p-simulate Frege systems, but the author didn't mention whether Frege systems p-simulate R(lin). So, do we currenly know a concrete polynomial-size proof of Tseitin formulas in <em>unbounded</em>-depth Frege systems?</p>

<reference-request><proof-complexity>
Do we currently know a polynomial-size Frege proof for Tseitin formulas?
Soha
# Do we currently know a polynomial-size Frege proof for Tseitin formulas?

(Asked by: username_0 on 2023-11-09)

There's a vast literature about super-polynomial lower bounds on proof lengths of Tseitin formulas in bounded-depth Frege systems, but what I'm curious about is: what if we don't restrict the depth of the proof? I found a [paper](https://www.doc.ic.ac.uk/%7Eitzamere/R-lin.pdf) which claims that Tseitin formulas have a polynomial-size proof in the R(lin) (Resolution over Linear Equations) proof system, which was found to p-simulate Frege systems, but the author didn't mention whether Frege systems p-simulate R(lin). So, do we currenly know a concrete polynomial-size proof of Tseitin formulas in *unbounded*-depth Frege systems?

**Tags:** reference-request, proof-complexity

---

## 2 answers

### Answer by username_2 on 2023-11-09. Score: 8 | Accepted answer

Section 6 of the following paper has a sketch:

> Alasdair Urquhart. Hard examples for resolution. Journal of the ACM,
> 34(1):209–219, 1987. DOI: <https://doi.org/10.1145/7531.8928>


---

### Answer by username_1 on 2023-11-10. Score: 8

Tseitin tautologies are unsatisfiable systems of linear equations over $\mathbb F\_2$, and as such they can be refuted just by summing all the equations together (possibly after reconstructing the equations from a CNF encoding, depending on how exactly they are formulated). This provides a trivial proof in $\mathrm{Res}(\oplus)$ (resolution with linear equations over $\mathbb F\_2$, i.e., parities of sets of literals), which is a subsystem of $F\_d(\oplus)$ (constant-depth Frege with parity gates), which is p-simulated by Frege. The crux of the Frege proof is to take polynomial-size formulas for parity, and construct short proofs of their basic properties.


---

