On the Proof Complexities of Strongly Equal Non-classical Tautologies

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.