The theory constructed in the article includes the formulation of two natural first-order predicate calculi: intuitionistic and minimal. For these two types of logic, the article defines a new notion of normal natural deduction. A theorem on the normalization of natural deductions in these calculi is proved.
Keywords: system of natural deduction, intuitionistic natural predicate calculus, normal natural deduction, automated theorem proving, search for a natural logical proof
Received September 20, 2024
Revised October 15, 2024
Accepted October 21, 2024
Oleg Alievich Okhotnikov, Ural Federal University, Yekaterinburg, 620000 Russia, e-mail: oleg.okhotnikov@gmail.com
REFERENCES
1. Smirnov V.A. Logicheskie metody analiza nauchnogo znaniya [Logical methods of analysis of scientific knowledge]. Moscow, Editorial URSS, 2002, 264 p. ISBN: 5-8360-0308-4 .
2. Smirnov V.A., Markin V.I., Novodvorskii A.E., Smirnov A.V. Dokazatel’stvo i ego poisk. Kurs logiki i komp’uternyi praktikum [Proof and its search. A course of logic and computer practical work]. In: Logika i komp’uter [Logic and computer], no. 3. Moscow, Nauka Publ., 1996, 256 p. ISBN: 5-02-013603-4 .
3. Troelstra A., Schwichtenberg H. Basic proof theory. Second Edt. Cambridge Univ. Press, 2000, 417 p. doi: 10.1017/CBO9781139168717
4. Pelletier F.J., Hazen A. Natural deduction systems in logic. The Stanford encyclopedia of philosophy, 2021.
5. Vtorushin Yu.I. On the search for inference in the system of natural deduction of predicate logic. Intellektual’nyye sistemy, 2009, vol. 13, no. 1–4, pp. 263–288.
6. Portoraro F. Automated reasoning. The Stanford encyclopedia of philosophy, 2024.
7. Negri S., von Plato J. Structural proof theory. Cambridge, Cambridge Univ. Press, 2001, 274 p. doi: 10.1017/CBO9780511527340
8. Negri S., von Plato J. Proof analysis. A contribution to Hilbert’s last problem. Cambridge, Cambridge Univ. Press, 2011, 278 p. doi: 10.1017/CBO9781139003513
9. Thiele R. Hilbert’s twenty-fourth problem. American Math. Monthly, 2003, vol. 110, iss. 1, pp. 1–24. doi: 10.1080/00029890.2003.11919933
10. Sieg W., Byrnes J. Normal natural deduction proofs (in classical logic). Studia logica, 1998, vol. 60, no. 1, pp. 67–106. doi: 10.1023/A:1005091418752
11. Sieg W., Cittadini S. Normal natural deduction proofs (in non-classical logic). Mech. Math. Resoning., Ser. Lecture notes in computer science, 2005, vol. 2605, pp. 169–191. doi: 10.1007/978-3-540-32254-2_11
12. Serebryannikov O.F. Normal forms of logical proofs and problems of theoretical heuristics. Voprosy gnoseologii, logiki i metodologii nauchnogo issledovaniya, 1972, vol. 3, pp. 89–106 (in Russian).
13. Prawitz D. Natural deduction. A proof-theoretical study, Stockholm, Almqvist & Wiksell, 1965, 113 p. Reprint: NY, Dover Publ., 2006, 128 p. ISBN: 978-0486446554 . Translated to Russian under the title Natural’nyi vyvod, Moscow, Lori Publ., 1997, 108 p. ISBN: 5-85582-026-2 .
14. Serebryannikov O.F. Normal forms of logical proofs. Logicheskiy vyvod, 1979, pp. 267–273 (in Russian).
15. Okhotnikov O. About proof-search in intuitionistic natural deduction calculus using partial Skolemization. J. Phys.: Confer. Ser., 2020, vol. 1680, art. 012038, pp. 1–7. doi: 10.1088/1742-6596/1680/1/012038
16. Okhotnikov O. A new sequent calculus for automated proof search. Appl. Math. Sci., 2014, vol. 8, no. 100, pp. 4977–4984. doi: 10.12988/ams.2014.46497
17. Supplementary Materials for the article O. A. Okhotnikov. “On normal deduction proofs in intuitionistic natural predicate calculus”. The online version contains supplementary material (see PDF) .
Cite this article as: O.A. Okhotnikov. On normal deduction proofs in intuitionistic natural predicate calculus. Trudy Instituta Matematiki i Mekhaniki UrO RAN, 2024, vol. 30, no. 4, pp. 188–206.
