Some Properties of Several Proof Systems for Intuitionistic, Johanssons and Monotone Propositional Logics

Abstract

In this paper we investigate two properties of some propositional systems of Intuitionistic, Johansson’s and Monotone logics: 1) the relations between the proofs complexities of strongly equal tautologies (valid sequents) and 2) the relations between the proofs complexities of minimal tautologies (valid sequents) and of results of substitutions in them. We show that 1) strongly equal tautologies (valid sequents) can have essential different proof complexities in the same system and 2) the result of substitution can be proved easier, than corresponding minimal tautology (valid sequents), therefore the systems, which are considered in this paper, are no monotonous neither by lines nor by size.