http://lambda-the-ultimate.org/node/4003 で紹介されている "An intuitionistic logic that proves Markov's principle" という論文が興味深いです。
典型的な intuitionistic logic では、double negation elimination を表す論理式は証明できません(実際、double negation elimination を公理に加えると任意の classical logic の定理が証明できるようになります)。この論文ではある intuitionistic predicate logic のバリエーションを定義し、その上で Markov's principle を表す論理式を証明できることを明らかにしています。これらの論理式は universal quantifier と implication を含まない式についての二重否定の除去を表しています。
提案されている証明系が intuitionistic logic のバリエーションと呼べるのは、
を満たしているからだということです。
そこで気になってくるのは、制限付きの double negation elimination の代わりに、制限付きの Peirce's law が成り立つような、上記2つの性質を満たす intuitionistic logic のバリエーションがあり得るかということです。