Intuitionistic predicate logic with the connective “tomorrow”

We formulate a Gentzen-type system for an intuitionistic logic with an additional unary connective. This connective is interpreted in the class of tree-like Kripke models by the notion “tomorrow”. The logicis sound and complete in this class of models.