Reading “Effect of the choice of connectives on the relation between classical logic and intuitionistic logic”
by Kawano, Tomoaki; Matsuda, Naosuke; Takagi, Kento
The paper studies the equivalence of intuitionistic and classical validity in propositional logic for a language that contains as the only logicial connectives the ones that represent monotonic Boolean formulas.
It is shown that, for this class of formulas, intuitionistic and classical validity coincide. The notion of classical validity is the usual one (sometimes called Tarski semantics), while, for the notion of intuitionistic validity, the authors use what they call extended Kripke interpretation: the interpretation consists in, for every connective, prefixing a universal quantification $v\ge w$ (meaning ``in a possible world $v$ extending the world $w$'') before the classical interpretation of the connective.
The result is interesting, because usually intuitionistic and classical validity are shown to coincide for classes of formulas such as the so called “negative” formulas (that exclude the authentically intuitionistic connectives of disjunction and existential quantification). The class of monotone Boolean formulas thus in a way generalizes the class of negative ones.
The result shown is said to answer an open question posed by van der Giessen about the proof theory of inuitionistic and classical natural deduction calculi, however in the paper the link between the model theory developed in the paper and the proof theory of the open question is not made in sufficient detail (is there a soundness and completeness theorem for the notion of validity used with respect to the calculi?).
Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net