0
$\begingroup$

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.

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

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.