Craig’s interpolation theorem for logic with the Ruet operator

Abstract

The system with the Ruet operator studied here is a logic, the language of which contains a unary logical connective representing a certain cyclic operation on a set of truth values and simulating with its double iteration the deductive properties of negation of classical propositional logic. This unary connective is called the Ruet operator. The purpose of this article is to prove Craig’s interpolation theorem for a logic with the Ruet operator. The definition of logic with the Ruet operator is given, an adequate sequent axiomatization of this logic is given, a new sequent calculus is constructed in a language enriched with logical constants and Craig’s interpolation theorem for this logic is proved.