MATHEMATICAL CERTAINTY IN CONTEMPORARY FORMAL SYSTEMS: A SYSTEMATIC LITERATURE REVIEW OF AXIOMATIC STRUCTURES, PROOF THEORY, LOGICAL ARCHITECTURES, AND COMPUTATIONAL VERIFICATION
Bengkulu, Indonesia dan Johor Baru, Malaysia
Abstract
Mathematical certainty in formal mathematics is commonly associated with the validity, consistency, and correctness of reasoning within explicitly defined formal systems. However, recent developments in axiomatic foundations, proof theory, non-classical logic, and computational verification suggest that certainty is increasingly discussed as a structured and system-relative phenomenon. This study aims to synthesize how mathematical certainty is conceptualized in contemporary literature through axiomatic structures, proof-theoretic mechanisms, logical architectures, and computational verification. A systematic literature review was conducted using the PRISMA framework. Twenty peer-reviewed studies published between 2020 and 2026 and retrieved from the Scopus database were selected based on predefined inclusion and exclusion criteria. Thematic synthesis identified four interrelated dimensions: axiomatic foundations as formal constraints, proof-theoretic mechanisms as procedures for validating derivations, logical architectures as system-relative frameworks of inference, and computational verification as a mechanism for strengthening reproducibility in formal proof validation. The findings suggest that mathematical certainty in the reviewed literature is not treated solely as a fixed metaphysical guarantee, but may be interpreted as a structurally mediated condition supported by coherence, rule-governed derivation, logical validity, and verifiable formalization. This review contributes a conceptual framework for understanding mathematical certainty within contemporary formal mathematical systems while acknowledging the limitations of a Scopus-based corpus.
Keywords: Axiomatic Systems, Computational Verification, Formal Logic, Mathematical Certainty, Proof Theory
References
Bílková, M., Frittella, S., & Kozhemiachenko, D. (2025). Crisp Bi-Gödel Modal Logic and Its Paraconsistent Expansion. Logic Journal of the IGPL, 33(5). https://doi.org/https://doi.org/10.1093/jigpal/jzad017
Chen, J., Greco, G., Palmigiano, A., & Tzimoulis, A. (2022). Non-normal modal logics and conditional logics: Semantic analysis and proof theory. Information and Computation, 287. https://doi.org/10.1016/j.ic.2021.104756
Dou, G., & Yu, W. (2024). Formalization of the Filter Extension Principle (FEP) in Coq. In L. Zhang, W. Yu, Q. Wang, Y. Laili, & Y. Liu (Eds.), Communications in Computer and Information Science: Vol. 2138 CCIS (pp. 95–106). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-981-97-3951-6_10
Drago, A. (2021). An Intuitionist Reasoning Upon Formal Intuitionist Logic: Logical Analysis of Kolmogorov’s 1932 Paper. Logica Universalis, 15(4), 537–552. https://doi.org/10.1007/s11787-021-00292-3
Figueira, S., & Goren-Roig, G. (2025). Modal logic with relations over paths: A theoretical development through comonadic semantics. Journal of Logic and Computation, 35(6). https://doi.org/10.1093/logcom/exae082
Gherardi, G., Orlandelli, E., & Raidl, E. (2024). Proof Systems for Super- Strict Implication. Studia Logica, 112(1–2), 249–294. https://doi.org/10.1007/s11225-023-10048-3
Giovannini, E. N., & Schiemer, G. (2025). Hilbert’s Early Metatheory Revisited. Erkenntnis. https://doi.org/10.1007/s10670-025-00959-z
Gius, M., & Tompits, H. (2023). Sequent-type rejection systems for finite-valued non-deterministic logics. Journal of Applied Non-Classical Logics, 33(3–4), 606–640. https://doi.org/10.1080/11663081.2023.2244367
Golan, R. (2022). Metainferences from a Proof-Theoretic Perspective , and a Hierarchy of Validity Predicates. 1295–1325. https://link.springer.com/article/10.1007/s10992-021-09616-6
Guan, Y., Fu, Y., & Meng, X. (2026). The Machine-Checked Complete Formalization of Landau’s Foundations of Analysis in Rocq. Mathematics, 14(1). https://doi.org/10.3390/math14010061
Hayashi, D. (2022). On Cut-Elimination Arguments for Axiomatic Theories of Truth. Studia Logica, 110(3), 785–818. https://doi.org/10.1007/s11225-021-09978-7
Ilic, I. D., & Višnjić, J. M. (2025). Towards mathematical foundations of projects: Construction and formalization. Filomat, 39(18), 6103–6121. https://doi.org/10.2298/FIL2518103I
Kelikli, M. (2024). On the structural properties of paradoxes: the distinction between formal language and natural language that comes with the use of the liar paradox. Logical Investigations, 30(1), 27–40. https://doi.org/10.21146/2074-1472-2024-30-1-27-40
Khomskii, Y., & Oddsson, H. V. (2024). Paraconsistent And Paracomplete Zermelo-Fraenkel Set Theory. Review of Symbolic Logic, 17(4), 965–995. https://doi.org/10.1017/S1755020323000382
Kushida, H. (2020). A Proof Theory for the Logic of Provability in True Arithmetic. Studia Logica, 108(4), 857–875. https://doi.org/10.1007/s11225-019-09891-0
Liang, Y., Zhao, D., Zeng, B., Zhu, Z., Ye, H., Wang, S., Zheng, B., & Li, G. (2025). Current Status and Future Prospects of Fuzzy Control. In L. Cao, Q. Zhang, P. Hu, & L. Liu (Eds.), Proceedings of SPIE - The International Society for Optical Engineering (Vol. 13799). SPIE. https://doi.org/10.1117/12.3073238
Lovyagin, Y. N., & Lovyagin, N. Y. (2021). Finite arithmetic axiomatization for the basis of hyperrational non-standard analysis. Axioms, 10(4). https://doi.org/10.3390/axioms10040263
Lyon, T., & Ostropolski-Nalewaja, P. (2024). Decidability of Quasi-Dense Modal Logics. Proceedings - Symposium on Logic in Computer Science. https://doi.org/10.1145/3661814.3662111
Miranda-Perea, F. E., González Huesca, L. D. C., & Linares-Arévalo, P. S. (2022). A dual-context sequent calculus for the constructive modal logic S4. Mathematical Structures in Computer Science, 32(9), 1205–1233. https://doi.org/10.1017/S0960129522000378
Page, M. J., Mckenzie, J. E., Bossuyt, P. M., Boutron, I., Hoffmann, T. C., Mulrow, C. D., Shamseer, L., Tetzlaff, J. M., Akl, E. A., Brennan, S. E., Chou, R., Glanville, J., Grimshaw, J. M., Hróbjartsson, A., Lalu, M. M., Li, T., Loder, E. W., Mayo-wilson, E., Mcdonald, S., … Moher, D. (2021). The PRISMA 2020 statement : an updated guideline for reporting systematic reviews. 1–11.
Quinn, F. (2024). On foundations for deductive mathematics. June, 1–9.
Salehi, S. (2022). Axiomatic (And Non-Axiomatic) Mathematics. Rocky Mountain Journal of Mathematics, 52(4), 1157–1176. https://doi.org/10.1216/rmj.2022.52.1157
van der Berg, I., de Domenico, A., Greco, G., Manoorkar, K. B., Palmigiano, A., & Panettiere, M. (2023). Labelled Calculi for Lattice-Based Modal Logics. In M. Banerjee & A. V Sreejith (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Vol. 13963 LNCS (pp. 23–47). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-26689-8_3
Von Plato, J. (2025). Gödel’s modal interpretation of intuitionistic logic and its proof theory. Monatshefte Fur Mathematik, 208(4), 791–817. https://doi.org/10.1007/s00605-025-02083-0
Zayton, B. (2022). Open texture , rigor , and proof. Synthese, 200(4), 1–20. https://doi.org/10.1007/s11229-022-03842-4
Zhang, C., & Yu, W. (2025). Formal Verification of the Equivalence Between Dedekind’s Fundamental Theorem and the Supremum Theorem Based on Axiomatic Set Theory. ICCMS 2025 - Proceedings of the 2025 17th International Conference on Computer Modeling and Simulation, 23–27. https://doi.org/10.1145/3761668.3761673
