On the Proof Complexities of Strongly Equal Non-classical Tautologies
Anahit Chubaryan *
Department of Informatics and Applied Mathematics, Yerevan State University, Armenia.
Sergey Sayadyan
Department of Informatics and Applied Mathematics, Yerevan State University, Armenia.
*Author to whom correspondence should be addressed.
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.
Keywords: Determinative conjunct, strongly equal tautologies, proof complexity