# Normal forms for intuitionistic formulas?

It is well-known that DNFs/CNFs and prenex normal forms generally do not exist for intuitionistic logic.

Are there any nice results about formula normalization for IL? I've tried googling this but the results just end up being about normal forms for proofs.

## 1 Answer

There are two main ways you could take this.

1. If you are interested in provability, then what you want is the Gödel-Tarski embedding of intuitionistic logic into classical S4 modal logic. The idea is that you can interpret the box modality of modal logic as a "provability" modality, and then stick a box in front of each connective. Then you can put the formula into whatever variant of modal CNF you need.

2. If you are interested in retaining the ability to translate intuitionistic proofs, then one popular idea is to use Tarski's "high school identities" to put intuitionistic formulas into a normal form related to the exponential polynomials. This gives a normal form for types, whose translation preserves the beta-eta equivalence of proofs of that type.

See Danko Ilik's The exp-log normal form of types.

Both of these papers are about the propositional case. I don't know what happens with first-order quantifiers.