ИСТИНА

Логика доказательств первого порядка FOLP, найденная авторами доклада, описывает свойства предикатов доказательств для формальной арифметики. Для этого в язык введена конструкция, позволяющая в выводах управлять списками переменных, открытых и закрытых для подстановки. Логика FOLP является точным аналогом модальной логики первого порядка S4, для нее описана естественная доказуемостная интерпретация и доказана корректность. ============================= The propositional logic of proofs LP (S. Artemov, 1995) revealed an explicit provability reading of modal logic S4 and thereby provided a provability semantics for the propositional intuitionistic logic. In the first-order case it was established that the most natural axiomatizability questions for the first-order logic of proofs have negative answers (S. Artemov, T. Yavorskaya, 2001). The questions of provability reading for first-order S4 and the first-order intuitionistic logic HPC remained open until 2011. In my talk I am going to present the first-order logic of proofs FOLP and its exact interpretation in formal systems (e.g., in Peano Arithmetic). FOLP is capable of realizing the first-order S4 and, therefore, HPC. This provides a semantics of explicit proofs for first-order S4 and HPC compliant with Brouwer-Heyting-Kolmogorov requirements. (Joint work with S. Artemov.)