<p>There are two main ways you could take this.</p>
<ol>
<li><p>If you are interested in <em>provability</em>, 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 &quot;provability&quot; 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.</p>
<p>See Mints' paper <a href="https://link.springer.com/chapter/10.1007/978-3-642-30743-0_33" rel="noreferrer"><em>The Gödel-Tarski Translations of Intuitionistic Propositional Formulas</em></a>.</p>
</li>
<li><p>If you are interested in retaining the ability to translate intuitionistic proofs, then one popular idea is to use Tarski's &quot;high school identities&quot; 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.</p>
<p>See Danko Ilik's <a href="https://arxiv.org/abs/1502.04634" rel="noreferrer"><em>The exp-log normal form of types</em></a>.</p>
</li>
</ol>
<p>Both of these papers are about the propositional case. I don't know what happens with first-order quantifiers.</p>

CC BY-SA 3.0
2017-11-23T09:19:01.670Z
Brock-Nannestad and Ilik’s paper [*An Intuitionistic Formula Hierarchy Based on High-School Identities*](https://arxiv.org/abs/1601.04876) “extend[s] the exponential polynomial analogy to the first-order quantifiers, showing that it gives rise to an intuitionistic hierarchy of formulas, resembling the classical arithmetical hierarchy”.
Vej Kse
CC BY-SA 3.0
2017-11-14T11:50:33.460Z
2017-11-14T11:50:33.460Z
2020-06-17T09:38:08.363Z
Neel Krishnaswami
<p>It is well-known that DNFs/CNFs and prenex normal forms generally do not exist for intuitionistic logic.  </p>

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

<lo.logic>
Normal forms for intuitionistic formulas?
user181407
# Normal forms for intuitionistic formulas?

(Asked by: username_0 on 2017-11-14)

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.

**Tags:** lo.logic


---

## 1 answers

### Answer by username_1 on 2017-11-14. Score: 7 | Accepted 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.

   See Mints' paper [*The Gödel-Tarski Translations of Intuitionistic Propositional Formulas*](https://link.springer.com/chapter/10.1007/978-3-642-30743-0_33).
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*](https://arxiv.org/abs/1502.04634).

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

> **Comments:**
> **username_2**: Brock-Nannestad and Ilik’s paper [*An Intuitionistic Formula Hierarchy Based on High-School Identities*](https://arxiv.org/abs/1601.04876) “extend[s] the exponential polynomial analogy to the first-order quantifiers, showing that it gives rise to an intuitionistic hierarchy of formulas, resembling the classical arithmetical hierarchy”.  

---

