Аннотация:Бимодальные логики CSM и CSMP были введены работах по логике доказуемости Т. Карлсона и К. Сморинского и Л.Д. Беклемишева, соответственно. Первая из них является наименьшей бимодальной логикой доказуемости для пар расширений арифметики Пеано (T,U), где U доказуемо содержит T. Вторая – для таких же теорий, где к тому же U является расширением T с помощью арифметических П1 аксиом.
В данной дипломной работе предложены системы без правила сечения для логик CSM и CSMP и доказана соответствующая теорема о полноте по Крипке. Предложенные системы удовлетворяют свойству подформульности в случае CSM и «почти подформульности» в случае CSMP. Эти результаты могут быть полезны в дальнейших исследованиях бимодальных логик доказуемости.