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 1


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.

  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.

  • 2
    $\begingroup$ Brock-Nannestad and Ilik’s paper An Intuitionistic Formula Hierarchy Based on High-School Identities “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”. $\endgroup$
    – Vej Kse
    Commented Nov 23, 2017 at 9:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.