<p><span class="math-container">$\let\eq\leftrightarrow\def\ru{\mathrel/}\let\ET\bigwedge$</span>Frege systems are required to be implicationally complete to make all such systems p-equivalent, yielding a robust definition of <em>the</em> Frege system that does not depend on insignificant details like the choice of the primitive rules of inference. If you drop implicational completeness, this no longer holds: all such “Frege” systems are still p-simulated by standard Frege, and <em>some</em> are still p-equivalent, but other system are wildly different (weaker). I’m not aware of this being systematically studied anywhere, but for a case in point, it is not hard to check that the system with the following rules is p-equivalent to the <em>cut-free</em> sequent calculus, which is known to be very weak (see e.g. the exponential lower bounds by Statman):
<span class="math-container">$$\begin{gather*}
\dfrac{A}{A\lor B}\qquad
\dfrac{A\lor A}A\qquad
\dfrac{A\lor B}{B\lor A}\qquad
\dfrac{A\lor(B\lor C)}{(A\lor B)\lor C}\qquad
\dfrac{(C\lor A)\lor(B\lor D)}{(C\lor B)\lor(A\lor D)}\\
\dfrac{}{A\lor\neg A}\qquad
\dfrac{C\lor A}{C\lor\neg\neg A}\qquad
\dfrac{C\lor\neg A\quad C\lor\neg B}{C\lor\neg(A\lor B)}
\end{gather*}$$</span>
(If you insist on having <span class="math-container">$\land$</span> in the language, include
<span class="math-container">$$\dfrac{C\lor A\quad C\lor B}{C\lor(A\land B)}\qquad\dfrac{C\lor(\neg A\lor\neg B)}{C\lor\neg(A\land B)}$$</span>
as well.)</p>
<p>As for the second question, the Boolean equational calculus (let me denote it E) is p-equivalent to standard Frege (F). I will sketch the argument below. Let <span class="math-container">$\top$</span> be a fixed tautology. Observe that similar to Frege, if <span class="math-container">$A\equiv B$</span> is any valid constant-size Boolean identity, then for any substitution <span class="math-container">$\sigma$</span>, we can replace <span class="math-container">$\sigma(A)$</span> in <span class="math-container">$C$</span> with <span class="math-container">$\sigma(B)$</span> by an E-derivation of size linear in the size of <span class="math-container">$\sigma$</span> (we just take a <span class="math-container">$\sigma$</span>-instance of a fixed E-derivation of <span class="math-container">$B$</span> from <span class="math-container">$A$</span>).</p>
<blockquote>
<p><strong>Proposition 1.</strong></p>
<ul>
<li>Given an E-derivation of <span class="math-container">$B$</span> from <span class="math-container">$A$</span>, we can construct in polynomial time an F-proof of <span class="math-container">$A\eq B$</span>.</li>
<li>Given an E-derivation of <span class="math-container">$A$</span> from <span class="math-container">$\top$</span>, we can construct in polynomial time an F-proof of <span class="math-container">$A$</span>.</li>
</ul>
</blockquote>
<p><strong>Proof:</strong>
First, if <span class="math-container">$A\ru B$</span> is any basic rule of E, then <span class="math-container">$A\eq B$</span> is a constant-size tautology, hence its substitution instances have linear-size F-proofs. Then a single-step E-derivation <span class="math-container">$C\vdash D$</span>, where we replace a subformula <span class="math-container">$\sigma(A)$</span> with <span class="math-container">$\sigma(B)$</span>, is simulated by a polynomial-size F-proof where we first derive <span class="math-container">$\sigma(A)\eq\sigma(B)$</span>, and then we propagate the equivalence upwards using instances of <span class="math-container">$P\eq Q\ru(P\circ R)\eq(Q\circ R)$</span>, where <span class="math-container">$\circ$</span> is any connective.</p>
<p>Now, given an E-derivation <span class="math-container">$A=A_1,\dots,A_n=B$</span>, we construct F-proofs of <span class="math-container">$A_1\eq A_2,\dots,A_{n-1}\eq A_n$</span> as indicated, and chain them together to a proof of <span class="math-container">$A_1\eq A_n$</span> using instances of <span class="math-container">$P\eq Q,Q\eq R\ru P\eq R$</span>.</p>
<blockquote>
<p><strong>Proposition 2.</strong></p>
<ul>
<li>Given an F-proof of <span class="math-container">$A\eq B$</span>, we can construct in polynomial time an E-derivation of <span class="math-container">$B$</span> from <span class="math-container">$A$</span>.</li>
<li>Given an F-proof of <span class="math-container">$A$</span>, we can construct in polynomial time an E-derivation of <span class="math-container">$A$</span> from <span class="math-container">$\top$</span>.</li>
</ul>
</blockquote>
<p><strong>Proof:</strong>
Let <span class="math-container">$A_1,\dots,A_n=(A\eq B)$</span> be an F-proof. We first construct an E-derivation
<span class="math-container">$$\tag1\label1A\vdash A\land A_1\vdash\dots\vdash A\land A_1\land\dots\land A_n$$</span>
(arbitrarily bracketed). Write <span class="math-container">$C_i=A\land\ET_{j\le i}A_j$</span> for <span class="math-container">$i=0,\dots,n$</span>, where we identify <span class="math-container">$C_0$</span> with <span class="math-container">$A$</span>. In order to derive <span class="math-container">$C_i$</span> from <span class="math-container">$C_{i-1}$</span>, assume that <span class="math-container">$A_i$</span> was derived in the original proof by an instance of an F-rule from <span class="math-container">$A_{j_1},\dots,A_{j_c}$</span>, where <span class="math-container">$j_1,\dots,j_c&lt;i$</span>. We first apply a sequence of instances of associativity and commutativity to reorder the conjunction in <span class="math-container">$C_{i-1}$</span> to the form <span class="math-container">$\dots\land(A_{j_1}\land\dots\land A_{j_c})$</span>. Since
<span class="math-container">$$(A_{j_1}\land\dots\land A_{j_c})\equiv(A_{j_1}\land\dots\land A_{j_c}\land A_i)$$</span>
is an instance of a constant-size Boolean identity, we can construct a linear-size E-derivation <span class="math-container">$\dots\land(A_{j_1}\land\dots\land A_{j_c})\vdash\dots\land(A_{j_1}\land\dots\land A_{j_c}\land A_i)$</span>, and if needed, we apply associativity and commutativity to reorder the conjuction back to form <span class="math-container">$C_i$</span>.</p>
<p>Since <span class="math-container">$A_n$</span> is <span class="math-container">$A\eq B$</span>, we can use the Boolean identity <span class="math-container">$(A\land(A\eq B))\equiv(B\land(A\eq B))$</span> to derive
<span class="math-container">$$\tag2\label2A\land A_1\land\dots\land A_n\vdash B\land A_1\land\dots\land A_n.$$</span>
Finally, we apply the same argument as in <span class="math-container">$\eqref1$</span> backwards to derive
<span class="math-container">$$\tag3\label3B\land A_1\land\dots\land A_n\vdash B\land A_1\land\dots\land A_{n-1}\vdash\dots\vdash B\land A_1\vdash B.$$</span>
Together, <span class="math-container">$\eqref1$</span>, <span class="math-container">$\eqref2$</span>, and <span class="math-container">$\eqref3$</span> yield an E-derivation <span class="math-container">$A\vdash B$</span>.</p>

CC BY-SA 4.0
2023-09-08T10:16:17.737Z
2023-09-08T10:16:17.737Z
Emil Jeřábek
<p>We know that Frege systems are required to be implicationally complete -- namely, if a set of formulas <span class="math-container">$B_1,B_2,\cdots,B_t$</span> imply formula <span class="math-container">$C$</span>, then this implication can be proven in the system. I'm curious about what happens if we discard this requirement. Is there any research on the relative efficiency of non-implicationally complete Frege systems? As an example, consider the case when we want to prove that a formula with connectives <span class="math-container">$\neg,\lor,\land$</span> is a tautology, using only the equivalence rules of Boolean algebra, like commutativity, associativity, distributivity, etc. But we shouldn't use non-equivalence rules, like <span class="math-container">$a\models a\lor b$</span>. I wonder if the ban of non-equivalence rules results in a superpolynomial explosion of proof size. I think this is important because it may help us understand the nature of Boolean algebra.</p>
<p><em>Update</em>: To clarify, the &quot;Boolean equational calculus&quot; system I defined here is not a Frege system. I define the system to allow applying of laws of Boolean algebra anywhere inside the formula. If I allow the system to have non-equivalence rules, the system would be p-equivalent to Frege systems, so I focus on the system without these rules. I didn't find this system in Krajíček's 2019 book, but I think it's interesting to have a look at.</p>

CC BY-SA 4.0
2023-09-05T19:34:54.850Z
I don't know of any work on this specific system, but I do know of a proof system that seems interesting and is not implicationally complete, namely, "Geometric IPS" as defined in Appendix B of https://doi.org/10.1145/3230742. (But I don't know any follow-up work on that yet!)
Joshua Grochow
CC BY-SA 4.0
2023-09-05T23:05:11.697Z
@EmilJeřábek Thanks for your comments. Could you please explain how to formulate an implicationally incomplete Frege system that is p-equivalent to the cut-free sequent calculus? Cut-free sequent calculus turns out to be complete.
Soha
CC BY-SA 4.0
2023-09-06T19:44:05.840Z
@EmilJeřábek I can understand that Frege systems p-simulate Boolean calculus, since if we apply Boolean rules on a node deep in the formula tree, we can gradually go up by using the rules $\let\eq\leftrightarrow\phi\eq\psi\vdash(\phi\circ\chi)\eq(\psi\circ\chi)$. But as for Boolean calculus p-simulating Frege, how can we make sure $\phi\vdash \phi\land\phi_0$ has a polynomial-size Boolean calculus proof?
Soha
CC BY-SA 4.0
2023-09-06T20:07:25.083Z
@EmilJeřábek Yeah we know that if we have $\phi\to\phi_0$ then we have $\phi\leftrightarrow\phi\land\phi_0$. But we have to prove $\phi\to\phi_0$ first.
Soha
CC BY-SA 4.0
2023-09-07T06:35:37.640Z
@EmilJeřábek Oh, I understand now. We're deriving $\phi\leftrightarrow\psi$ from nothing so $\phi_0$ must be an instance of an axiom scheme, hence it must be a tautology. All of $\phi_i$'s must be tautologies because tautologies can only imply tautologies. But, if $\phi_j$ is derived from $\phi_{i_1},\phi_{i_2},\cdots,\phi_{i_t}$ via a Frege rule, how can we add $\phi_j$ to the conjunction by Boolean calculus? The Frege rule might be a weakening rule so the rule itself might not be proved by Boolean calculus. We have to consider the rule and the fact that their inputs are tautologies together.
Soha
CC BY-SA 4.0
2023-09-07T07:44:50.557Z
@EmilJeřábek That's great. By "weakening rule", I mean a rule $\phi_{i_1},\phi_{i_2},\cdots,\phi_{i_t}\vdash\phi_{j}$ such that $\phi_{i_1}\land\cdots\land\phi_{i_t}$ isn't equivalent to $\phi_{j}$.
Soha
CC BY-SA 4.0
2023-09-07T07:47:49.527Z
One last question: does our result mean that Frege systems needn't have weakening rules, so that it needn't be implicationally complete? Because every tautology can be proved with Boolean equational calculus, and we can construct a Frege proof from the calculus, and this Frege system only has non-weakening rules. If we want to prove $B_1,B_2,\cdots,B_n\models C$ with a Frege system, we only need to prove that $\neg B_1\lor\neg B_2\lor\cdots\lor\neg B_n\lor C$ is a tautology, so this implicationally incomplete Frege system is sound and complete.
Soha
CC BY-SA 4.0
2023-09-07T13:37:44.773Z
The reason Frege systems are required to be implicationally complete is not because it would be genuinely needed to make the proof system useful, but because it makes all such systems p-equivalent, yielding a robust definition of *the* Frege system that does not depend on insignificant details like the choice of the primitive rules of inference. If you drop the condition, then *some* Frege systems are still p-equivalent, but others are wildly different (weaker).
Emil Jeřábek
CC BY-SA 4.0
2023-09-07T17:22:07.160Z
@EmilJeřábek Thank you very much. Actually you could post an answer so that I can accept it. :-)
Soha
CC BY-SA 4.0
2023-09-08T10:22:50.017Z
Ok, I converted my comments to an answer (and removed them to clean up the thread).
Emil Jeřábek
<reference-request><algebra><proof-complexity><boolean-formulas>
Power of non-implicationally-complete Frege systems and Boolean equational calculus
Soha
# Power of non-implicationally-complete Frege systems and Boolean equational calculus

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

We know that Frege systems are required to be implicationally complete -- namely, if a set of formulas $B\_1,B\_2,\cdots,B\_t$ imply formula $C$, then this implication can be proven in the system. I'm curious about what happens if we discard this requirement. Is there any research on the relative efficiency of non-implicationally complete Frege systems? As an example, consider the case when we want to prove that a formula with connectives $\neg,\lor,\land$ is a tautology, using only the equivalence rules of Boolean algebra, like commutativity, associativity, distributivity, etc. But we shouldn't use non-equivalence rules, like $a\models a\lor b$. I wonder if the ban of non-equivalence rules results in a superpolynomial explosion of proof size. I think this is important because it may help us understand the nature of Boolean algebra.

*Update*: To clarify, the "Boolean equational calculus" system I defined here is not a Frege system. I define the system to allow applying of laws of Boolean algebra anywhere inside the formula. If I allow the system to have non-equivalence rules, the system would be p-equivalent to Frege systems, so I focus on the system without these rules. I didn't find this system in Krajíček's 2019 book, but I think it's interesting to have a look at.

**Tags:** reference-request, algebra, proof-complexity, boolean-formulas

> **Comments:**
> **username_1**: I don't know of any work on this specific system, but I do know of a proof system that seems interesting and is not implicationally complete, namely, "Geometric IPS" as defined in Appendix B of https://doi.org/10.1145/3230742. (But I don't know any follow-up work on that yet!)  
> **username_0**: @EmilJeřábek Thanks for your comments. Could you please explain how to formulate an implicationally incomplete Frege system that is p-equivalent to the cut-free sequent calculus? Cut-free sequent calculus turns out to be complete.  
> **username_0**: @EmilJeřábek I can understand that Frege systems p-simulate Boolean calculus, since if we apply Boolean rules on a node deep in the formula tree, we can gradually go up by using the rules $\let\eq\leftrightarrow\phi\eq\psi\vdash(\phi\circ\chi)\eq(\psi\circ\chi)$. But as for Boolean calculus p-simulating Frege, how can we make sure $\phi\vdash \phi\land\phi_0$ has a polynomial-size Boolean calculus proof?  
> **username_0**: @EmilJeřábek Yeah we know that if we have $\phi\to\phi_0$ then we have $\phi\leftrightarrow\phi\land\phi_0$. But we have to prove $\phi\to\phi_0$ first.  
> **username_0**: @EmilJeřábek Oh, I understand now. We're deriving $\phi\leftrightarrow\psi$ from nothing so $\phi_0$ must be an instance of an axiom scheme, hence it must be a tautology. All of $\phi_i$'s must be tautologies because tautologies can only imply tautologies. But, if $\phi_j$ is derived from $\phi_{i_1},\phi_{i_2},\cdots,\phi_{i_t}$ via a Frege rule, how can we add $\phi_j$ to the conjunction by Boolean calculus? The Frege rule might be a weakening rule so the rule itself might not be proved by Boolean calculus. We have to consider the rule and the fact that their inputs are tautologies together.  
> **username_0**: @EmilJeřábek That's great. By "weakening rule", I mean a rule $\phi_{i_1},\phi_{i_2},\cdots,\phi_{i_t}\vdash\phi_{j}$ such that $\phi_{i_1}\land\cdots\land\phi_{i_t}$ isn't equivalent to $\phi_{j}$.  
> **username_0**: One last question: does our result mean that Frege systems needn't have weakening rules, so that it needn't be implicationally complete? Because every tautology can be proved with Boolean equational calculus, and we can construct a Frege proof from the calculus, and this Frege system only has non-weakening rules. If we want to prove $B_1,B_2,\cdots,B_n\models C$ with a Frege system, we only need to prove that $\neg B_1\lor\neg B_2\lor\cdots\lor\neg B_n\lor C$ is a tautology, so this implicationally incomplete Frege system is sound and complete.  
> **username_2**: The reason Frege systems are required to be implicationally complete is not because it would be genuinely needed to make the proof system useful, but because it makes all such systems p-equivalent, yielding a robust definition of *the* Frege system that does not depend on insignificant details like the choice of the primitive rules of inference. If you drop the condition, then *some* Frege systems are still p-equivalent, but others are wildly different (weaker).  
> **username_0**: @EmilJeřábek Thank you very much. Actually you could post an answer so that I can accept it. :-)  
> **username_2**: Ok, I converted my comments to an answer (and removed them to clean up the thread).  

---

## 1 answers

### Answer by username_2 on 2023-09-08. Score: 2 | Accepted answer

$\let\eq\leftrightarrow\def\ru{\mathrel/}\let\ET\bigwedge$Frege systems are required to be implicationally complete to make all such systems p-equivalent, yielding a robust definition of *the* Frege system that does not depend on insignificant details like the choice of the primitive rules of inference. If you drop implicational completeness, this no longer holds: all such “Frege” systems are still p-simulated by standard Frege, and *some* are still p-equivalent, but other system are wildly different (weaker). I’m not aware of this being systematically studied anywhere, but for a case in point, it is not hard to check that the system with the following rules is p-equivalent to the *cut-free* sequent calculus, which is known to be very weak (see e.g. the exponential lower bounds by Statman):
$$\begin{gather\*}
\dfrac{A}{A\lor B}\qquad
\dfrac{A\lor A}A\qquad
\dfrac{A\lor B}{B\lor A}\qquad
\dfrac{A\lor(B\lor C)}{(A\lor B)\lor C}\qquad
\dfrac{(C\lor A)\lor(B\lor D)}{(C\lor B)\lor(A\lor D)}\\
\dfrac{}{A\lor\neg A}\qquad
\dfrac{C\lor A}{C\lor\neg\neg A}\qquad
\dfrac{C\lor\neg A\quad C\lor\neg B}{C\lor\neg(A\lor B)}
\end{gather\*}$$
(If you insist on having $\land$ in the language, include
$$\dfrac{C\lor A\quad C\lor B}{C\lor(A\land B)}\qquad\dfrac{C\lor(\neg A\lor\neg B)}{C\lor\neg(A\land B)}$$
as well.)

As for the second question, the Boolean equational calculus (let me denote it E) is p-equivalent to standard Frege (F). I will sketch the argument below. Let $\top$ be a fixed tautology. Observe that similar to Frege, if $A\equiv B$ is any valid constant-size Boolean identity, then for any substitution $\sigma$, we can replace $\sigma(A)$ in $C$ with $\sigma(B)$ by an E-derivation of size linear in the size of $\sigma$ (we just take a $\sigma$-instance of a fixed E-derivation of $B$ from $A$).

> **Proposition 1.**
>
> * Given an E-derivation of $B$ from $A$, we can construct in polynomial time an F-proof of $A\eq B$.
> * Given an E-derivation of $A$ from $\top$, we can construct in polynomial time an F-proof of $A$.

**Proof:**
First, if $A\ru B$ is any basic rule of E, then $A\eq B$ is a constant-size tautology, hence its substitution instances have linear-size F-proofs. Then a single-step E-derivation $C\vdash D$, where we replace a subformula $\sigma(A)$ with $\sigma(B)$, is simulated by a polynomial-size F-proof where we first derive $\sigma(A)\eq\sigma(B)$, and then we propagate the equivalence upwards using instances of $P\eq Q\ru(P\circ R)\eq(Q\circ R)$, where $\circ$ is any connective.

Now, given an E-derivation $A=A\_1,\dots,A\_n=B$, we construct F-proofs of $A\_1\eq A\_2,\dots,A\_{n-1}\eq A\_n$ as indicated, and chain them together to a proof of $A\_1\eq A\_n$ using instances of $P\eq Q,Q\eq R\ru P\eq R$.

> **Proposition 2.**
>
> * Given an F-proof of $A\eq B$, we can construct in polynomial time an E-derivation of $B$ from $A$.
> * Given an F-proof of $A$, we can construct in polynomial time an E-derivation of $A$ from $\top$.

**Proof:**
Let $A\_1,\dots,A\_n=(A\eq B)$ be an F-proof. We first construct an E-derivation
$$\tag1\label1A\vdash A\land A\_1\vdash\dots\vdash A\land A\_1\land\dots\land A\_n$$
(arbitrarily bracketed). Write $C\_i=A\land\ET\_{j\le i}A\_j$ for $i=0,\dots,n$, where we identify $C\_0$ with $A$. In order to derive $C\_i$ from $C\_{i-1}$, assume that $A\_i$ was derived in the original proof by an instance of an F-rule from $A\_{j\_1},\dots,A\_{j\_c}$, where $j\_1,\dots,j\_c. We first apply a sequence of instances of associativity and commutativity to reorder the conjunction in $C\_{i-1}$ to the form $\dots\land(A\_{j\_1}\land\dots\land A\_{j\_c})$. Since
$$(A\_{j\_1}\land\dots\land A\_{j\_c})\equiv(A\_{j\_1}\land\dots\land A\_{j\_c}\land A\_i)$$
is an instance of a constant-size Boolean identity, we can construct a linear-size E-derivation $\dots\land(A\_{j\_1}\land\dots\land A\_{j\_c})\vdash\dots\land(A\_{j\_1}\land\dots\land A\_{j\_c}\land A\_i)$, and if needed, we apply associativity and commutativity to reorder the conjuction back to form $C\_i$.

Since $A\_n$ is $A\eq B$, we can use the Boolean identity $(A\land(A\eq B))\equiv(B\land(A\eq B))$ to derive
$$\tag2\label2A\land A\_1\land\dots\land A\_n\vdash B\land A\_1\land\dots\land A\_n.$$
Finally, we apply the same argument as in $\eqref1$ backwards to derive
$$\tag3\label3B\land A\_1\land\dots\land A\_n\vdash B\land A\_1\land\dots\land A\_{n-1}\vdash\dots\vdash B\land A\_1\vdash B.$$
Together, $\eqref1$, $\eqref2$, and $\eqref3$ yield an E-derivation $A\vdash B$.


---

