# Boolean logic: What is the name of this trick to replace explicit negations by implications?

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

• The logic of types is not classical. What is the point you're trying to make? Apr 17 at 15:19
• I never heard a special name for this. Apr 17 at 16:57
• Also, $C'$ is certainly not unique. E.g., $(A\to B)\lor C$ and $(A\to C)\lor B$ are equivalent. Apr 17 at 17:00
• @EmilJeřábek To my understanding, there is no transformation between these expressions involving only the mentioned rules?
– DuY
Apr 17 at 17:18
• @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.
– DuY
Apr 17 at 17:27