Miscellaneous
Colloquium Mathematical Philosophy, Grigory K. Olkhovikov (Ural Federal University Yekaterinburg) gives a talk at the MCMP Colloquium (25 April, 2013) titled "On flattening rules in natural deduction calculus for intuitionistic propositional logic". Abstract: Standard versions of natural deduction calculi consist of so called ‘flat’ rules that either discharge some formulas as their assumptions or discharge no assumptions at all. However, non-flat, or ‘higher-order’ rules discharging inferences rather than single formulas arise naturally within the realization of Lorenzen’s inversion principle in the framework of natural deduction. For the connectives which are taken as basic in the standard systems of propositional logic, these higher-order rules can be equivalently replaced with flat ones. Building on our joint work with Prof. P. Schroeder-Heister, we show that this is not the case with every connective of intuitionistic logic, the connective $c(A,B,C) = (A to B)vee C$ being our main counterexample. We also show that the dual question must be answered in the negative, too, that is to say, that existence of a system of flat elimination rules for a connective of intuitionistic logic does not guarantee existence of a system of flat introduction rules.