On the Proof Complexities of Strongly Equal Non-classical Tautologies

Abstract

The strong equality of classical tautologies and their proof complexities comparative analysis in certain proof systems were given by first author in previous studies. Here we introduce the analogous notions of strong equality for non-classical (intuitionistic and minimal) tautologies and investigate the relations between the proof complexity measures of strongly equal non-classical tautologies in some proof systems. We prove that 1) the strongly equal tautologies have the same proof complexities in some proof systems and 2) there are such proof systems, in which some measures of proof complexities for strongly equal tautologies are the same, while the other measures differ from each other only as a function of the sizes of tautologies.