Online research in philosophy

We show that Intuitionistic Open Induction iop is not closed under the rule DNS(∃ - 1 ). This is established by constructing a Kripke model of iop + $\neg L_y(2y > x)$ , where $L_y(2y > x)$ is universally quantified on x. On the other hand, we prove that iop is equivalent with the intuitionistic theory axiomatized by PA - plus the scheme of weak ¬¬LNP for open formulas, where universal quantification on the parameters precedes double negation. We also show (...) that for any open formula φ(y) having only y free, $(PA^-)^i \vdash L_y\varphi(y)$ . We observe that the theories iop, i∀ 1 and iΠ 1 are closed under Friedman's translation by negated formulas and so under VR and IP. We include some remarks on the classical worlds in Kripke models of iop. (shrink)

We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.