Loop-free calculus for modal logic S4. I

In the article, loop-free calculus for modal logic S4 is presented. To restrict applications of reflexivity and transitivity rules, several types of indexes are used. The use of indexes replaces the need to keep the history of previous applications of the rules. The article details the purpose of each type of index and proves that derivation search in the calculus is finite.