<p>Consider a Boolean circuit <span class="math-container">$C$</span> composed of some finite set of input variables <span class="math-container">$A_1,\ldots, A_n$</span> and the connectives <span class="math-container">$\lor\land\neg\rightarrow$</span> (with <span class="math-container">$X\rightarrow Y=\neg X\lor Y$</span>) (update: assume that <span class="math-container">$\lor$</span> and <span class="math-container">$\land$</span> are fan-in 2; as I understand, connectives with a greater fan-in could be made to work but would make the definitions more complicated).</p>
<p>It turns out that, iff <span class="math-container">$C$</span> evaluates to <span class="math-container">$1$</span> on an all-<span class="math-container">$1$</span> input, we can transform <span class="math-container">$C$</span> into a &quot;normal form&quot; <span class="math-container">$C'$</span> that uses no explicit negation (i.e. only <span class="math-container">$\lor\land\rightarrow$</span>), by applying the following rules:</p>
<ol>
<li>de Morgan's laws (DM),</li>
<li>double negation elimination/introduction (DN),</li>
<li>and replacing <span class="math-container">$\neg X \lor Y\iff X\rightarrow Y$</span> (AR).</li>
</ol>
<p>Furthermore, for each <span class="math-container">$C$</span>, there is only one <span class="math-container">$C'$</span> with this property (update: to be clear, the property &quot;can be transformed from <span class="math-container">$C$</span> using only the mentioned rules&quot;).</p>
<p>This can be proven by induction on the number of connectives of the form <span class="math-container">$\lor\land\rightarrow$</span>.</p>
<p>My question is: What is the standard name of this theorem/construction?</p>
<p>This seems relevant to me in the context of type theory - e.g. the one laid out in chapter 1 of the <a href="https://homotopytypetheory.org/book/" rel="nofollow noreferrer">HoTT book</a>. To my understanding, any Frege-style proof of a tautology (which will always evaluate to <span class="math-container">$1$</span> on an all-<span class="math-container">$1$</span> input) presented in this form can be turned into a type-theoretic construction, where <span class="math-container">$X\rightarrow Y$</span> turns into a function type, <span class="math-container">$A\lor B$</span> into the <span class="math-container">$+$</span> type, and <span class="math-container">$A \land B$</span> into the <span class="math-container">$\times$</span> type. Having eliminated explicit negations, one doesn't need a <span class="math-container">$0$</span> type, or a law of excluded middle, anymore.</p>
<p>What's more, we can (as above) find the normal form of any circuit in a linear number of steps. Given two circuits, equivalence under DM, DN, AR can be decided in linear time, and if they are equivalent, we can find an explicit transformation with a linear number of steps as well. So from a computational/proof complexity perspective, the type-theoretic constrution captures all that is hard about proving tautologies.</p>

CC BY-SA 4.0
2022-04-17T15:19:08.130Z
The logic of types is not classical. What is the point you're trying to make?
Andrej Bauer
CC BY-SA 4.0
2022-04-17T16:57:37.587Z
I never heard a special name for this.
Emil Jeřábek
CC BY-SA 4.0
2022-04-17T17:00:47.203Z
Also, $C'$ is certainly not unique. E.g., $(A\to B)\lor C$ and $(A\to C)\lor B$ are equivalent.
Emil Jeřábek
CC BY-SA 4.0
2022-04-17T17:18:42.483Z
@EmilJeřábek To my understanding, there is no transformation between these expressions involving only the mentioned rules?
Duyal Yolcu
CC BY-SA 4.0
2022-04-17T17:27:28.093Z
@AndrejBauer I claim that, whenever there is a dag-like classical Frege proof of a tautology C using K symbols, there is an intuitionist type-theoretic construction of NormalForm(C) using poly(K) symbols. By contraposition, a lower bound on the type-theoretic proof complexity of NormalForm(C) implies a lower bound on the Frege system proof complexity of C. Finding those is a [relevant problem](https://en.wikipedia.org/wiki/Frege_system#:~:text=Frege%20systems%20are%20considered%20to%20be%20fairly%20strong%20systems).
Duyal Yolcu
CC BY-SA 4.0
2022-04-17T19:36:13.473Z
In this case type theory is a red herring.
Andrej Bauer
CC BY-SA 4.0
2022-04-18T11:35:06.813Z
@EmilJeřábek To be more precise, I think that to get from one of your formulas to the other, one needs to consider associativity of $\lor$. For my choice of definitions, my original claim that the normal form always exists was not correct if one allows $\lor$ with a fan-in bigger than 2. Are you aware of a usage of this normal form/a literature reference in which it is discussed?
Duyal Yolcu
<type-theory><proof-complexity><boolean-formulas><circuits>
Boolean logic: What is the name of this trick to replace explicit negations by implications?
Duyal Yolcu
# Boolean logic: What is the name of this trick to replace explicit negations by implications?

(Asked by: username_0 on 2022-04-17)

Consider a Boolean circuit $C$ composed of some finite set of input variables $A\_1,\ldots, A\_n$ and the connectives $\lor\land\neg\rightarrow$ (with $X\rightarrow Y=\neg X\lor Y$) (update: assume that $\lor$ and $\land$ are fan-in 2; as I understand, connectives with a greater fan-in could be made to work but would make the definitions more complicated).

It turns out that, iff $C$ evaluates to $1$ on an all-$1$ input, we can transform $C$ into a "normal form" $C'$ that uses no explicit negation (i.e. only $\lor\land\rightarrow$), by applying the following rules:

1. de Morgan's laws (DM),
2. double negation elimination/introduction (DN),
3. and replacing $\neg X \lor Y\iff X\rightarrow Y$ (AR).

Furthermore, for each $C$, there is only one $C'$ with this property (update: to be clear, the property "can be transformed from $C$ using only the mentioned rules").

This can be proven by induction on the number of connectives of the form $\lor\land\rightarrow$.

My question is: What is the standard name of this theorem/construction?

This seems relevant to me in the context of type theory - e.g. the one laid out in chapter 1 of the [HoTT book](https://homotopytypetheory.org/book/). To my understanding, any Frege-style proof of a tautology (which will always evaluate to $1$ on an all-$1$ input) presented in this form can be turned into a type-theoretic construction, where $X\rightarrow Y$ turns into a function type, $A\lor B$ into the $+$ type, and $A \land B$ into the $\times$ type. Having eliminated explicit negations, one doesn't need a $0$ type, or a law of excluded middle, anymore.

What's more, we can (as above) find the normal form of any circuit in a linear number of steps. Given two circuits, equivalence under DM, DN, AR can be decided in linear time, and if they are equivalent, we can find an explicit transformation with a linear number of steps as well. So from a computational/proof complexity perspective, the type-theoretic constrution captures all that is hard about proving tautologies.

**Tags:** type-theory, proof-complexity, boolean-formulas, circuits
> **Comments:**
> **username_1**: The logic of types is not classical. What is the point you're trying to make?  
> **username_2**: I never heard a special name for this.  
> **username_2**: Also, $C'$ is certainly not unique. E.g., $(A\to B)\lor C$ and $(A\to C)\lor B$ are equivalent.  
> **username_0**: @EmilJeřábek To my understanding, there is no transformation between these expressions involving only the mentioned rules?  
> **username_0**: @AndrejBauer I claim that, whenever there is a dag-like classical Frege proof of a tautology C using K symbols, there is an intuitionist type-theoretic construction of NormalForm(C) using poly(K) symbols. By contraposition, a lower bound on the type-theoretic proof complexity of NormalForm(C) implies a lower bound on the Frege system proof complexity of C. Finding those is a [relevant problem](https://en.wikipedia.org/wiki/Frege_system#:~:text=Frege%20systems%20are%20considered%20to%20be%20fairly%20strong%20systems).  
> **username_1**: In this case type theory is a red herring.  
> **username_0**: @EmilJeřábek To be more precise, I think that to get from one of your formulas to the other, one needs to consider associativity of $\lor$. For my choice of definitions, my original claim that the normal form always exists was not correct if one allows $\lor$ with a fan-in bigger than 2. Are you aware of a usage of this normal form/a literature reference in which it is discussed?  

---

## 0 answers

