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.


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.


Your Answer

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

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