Proofs in mathematics which are noneffective by making use of the law-of-excluded-middle schema (LEM) in most concrete cases use only rather restricted forms of LEM, e.g. LEM applied only to formulas of very low complexity. For a fine analysis of the specific uses of classical logic made in proofs, also a number of principles different from LEM (though being derivable from sufficiently strong forms of LEM) have been introduced and studied since 1990's. To show that (over some intuitionistic base system) one noneffective principle A does not imply another principle B, one typically uses so-called proof interpretations (appropriate forms of realizability or functional interpretations) to show that A has a certain semi-constructive interpretation in the sense of the interpretation used which B does not. In fact, by the sophisticated use of such a proof interpretations and the models of finite-type arithmetic, one can prove a lot of underivability between weak fragments of the logical principles LEM, De Morgan's law (DML), the double negation elimination (DNE), the double negation shift (DNS) and so on. On the other hand, in the context of pure (intermediate) logics, such logical principles can be separated in many cases just by using very simple Kripke models. Motivated by this fact, we consider a uniform way to obtain the underivability results for weak fragments of the logical principles in arithmetic by using Kripke models which separate the corresponding intermediate logics.
This is a joint work partly with Ulrich Kohlenbach and partly with Hajime Ishihara, Takako Nemoto, Nobu-Yuki Suzuki and Keita Yokoyama.