A result on propositional logics having the disjunction property.
Robert E. Kirk · Notre Dame Journal of Formal Logic · 1982
It was conjectured in 1952 by Lukasiewicz [5] that the intuitionistic propositional logic (/) was the only consistent logic which has all intuitionistically valid formulas as theorems and also has the disjunction property, i.e., the property that 0 or \jj is a theorem whenever 0 v \jj is.This conjecture was shown to be false by Kreisel and Putnam [3], who exhibited a logic stronger that / having the disjunction property.Since the disjunction property is of some importance in constructive mathematics, a question arising naturally is whether there is a maximal propositional logic having this property.It is the purpose of this article to show that there is not; more precisely, that there is no intermediate logic having the disjunction property which contains as theorems all theorems of such logics.By a propositional logic we always mean a consistent system formulated in the usual way and closed under substitution and detachment, and by an intermediate logic we mean a propositional logic whose theorems include all intuitionistically valid formulas.Our proof will proceed by exhibiting two intermediate logics with the disjunction property whose union fails to have the property.The intermediate logics used are the system KP, used by Kreisel and Putnam to refute Lukasiewicz, which is axiomatized over / by the addition of the formulaand the logic of finite binary trees D x of Gabbay and DeJongh [2], which is axiomatized over/ by the addition of *I would like to thank the referee for pointing out a deficiency in an earlier version of this paper.