Reading “Extended frames and separations of logical principles”
by Makoto Fujiwara, Hajime Ishihara, Takako Nemoto, Nobu-yuki Suzuki and Keita Yokoyama
The authors introduce a new notion of model, called extended frame, that consists of two Kripke frames and a monotone map between them. They then use it to show the intuitionistic non-provability of certain omniscience principles, variants of the excluded middle, of double-negation elimination, of de Morgan laws, and their first-order counterparts MP, LPO, WLPO, LLPO, $\Delta_1$-PEM.
It is a new, simple and uniform method for separating these semi-classical principles, because previously the separation results had to obtained by building dedicated realizability models. For the moment, the approach seems to be limited to principles which are obtained from propositional formulas, by replacing a proposition with a $\Sigma_1$-predicate, which does not cover essentailly first-order principles like the Double Negation Shift.
Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net