Логика Гжегорчика с операторами арифметических доказательств

Аксиоматизируется логика с модальным оператором “\ldots истинно и доказуемо” и маркированными модальными операторами доказательств "$p$ является доказательством \ldots". Устанавливается полнота по Крипке, разрешимость и арифметическая полнота этой логики.