Formalization of Reasoning and Proofs Through the Lens of Human Thought Physiology and Logic

Introduction

The achievements of the sciences on the functioning of the human body, on the governing functions and properties of his brain, inherited are habitually used in medicine or biology [1,2]. Today, unfortunately, there is no tradition to use this knowledge to analyse mathematical results or ideas about the macro or microcosm in physics. For example, knowledge about the architecture of intellectual activity, in our opinion, should be considered in the process of correct formalization of physical and physiological models in all-natural sciences in order to radically reduce the load on higher mental functions of a person. But in particular, this necessity concerns the permissibility of certain computational operations on the information received in order to obtain a scientifically based true solution to scientific problem problems. The successes of AI sciences have determined high requirements not only for the "purity and reliability" of data, but also for the accuracy and effectiveness of operations on them. For the purposes of AI development in the direction of semantic, intellectual analysis of the received data, an analysis of the means of operating with them is also necessary.

In Stephen Wolfram's reminiscences about Douglas Lenat and his desire to follow the works of Aristotle and Leibniz, we unfortunately learned about the death of Douglas Lenat [3]. Doug's aspiration to utilize mathematical logic to enhance artificial intelligence methods was well-founded and sensible [4,5]. The ultimate goal, the attainment of a universal formal reasoning tool, while not fully achieved, unveiled vast horizons for AI systems. Doug comprehended well that in today's context, efficient algorithms for solving complex problems based on methods of intelligent data analysis and AI are increasingly in demand [6]. However, this quest for algorithms is currently dominated by a behaviourist component [7,8]. This very fact motivated a revaluation of the issue from the vantage point of fundamental sciences, seeking a solution within classical mathematical approaches.

The absence of a well-formed systematic view of the process of cognition, from its physiology to the field of AI, and its careful revision during the epoch of rapid development in these domains, in our view, impedes the transition to the next stage of progress. Alongside the remarkable achievements in theoretical and applied informatics AI, and MLL, these advancements do not influence our understanding of the fundamentals of formalization and the development of a methodology for comprehending the surrounding world as a whole [9-13]. This can be likened to an old house where each successive generation adds a new floor, modernizes it, and adorns it with new furniture, without discarding the old and without strengthening the foundation.

Significant progress in the search for sought-after algorithms can be achieved by focusing on a systematic re-examination of the foundations of our understanding of intelligence, primarily natural intelligence, the thinking process, and knowledge concentration through formalization and formal sciences. The author's attempt to do so ultimately led to a formalization methodology with breakthrough effects in solving intellectual tasks and addressing a range of scientific problems. This endeavour resulted in a highly effective method of intelligent analysis [14,15].

The aim of this article is to outline the fundamental obstacles that slow down the development of mathematical science [16]. Abstract principles regularly employed by researchers in their daily routines affect the accuracy of results and, consequently, the efficiency of the entire scientific chain, in which mathematics serves as a tool [17].

Doubt about the validity of the modus ponens rule (and others discussed in the article), as well as the corresponding logical law (relating to the transition from the statement of a conditional statement and its antecedent to the statement of its subsequent) casts doubt on the truth of existing proofs of theorems where this rule is used as one of the basic ones [18]. Consequently, this implies the necessity for a new formal proof for every scientific assertion and a reassessment of all traditionally substantiated assertions to date. This might seem daunting and implausible; however, the extent of the significance of this matter can only be gauged through a more detailed exploration of the concepts associated with it.

Various works discuss the rules of modus ponens, syllogism, and other fundamental abstractions established as laws during the formalization of scientific theory [19]. In reality, mathematicians employ these abstractions in their day-to-day work and such practice is considered legitimate analysis from the perspective of formalization sciences and brain physiology [20]. This topic is relegated to philosophical discourse, typically unrelated to research practice [21].

In advancing the science of artificial intelligence, it is crucial to contemplate the functioning of natural intelligence, particularly when constructing its models. The aspect of intellectualization in informatics and computer science was addressed in 2019 with interest predominantly observed in the field of brain physiology, engaging neurologists in relation to pathology and philosophers, but not mathematicians [22].

The perception of mathematics solely evolving by expanding its structure and enlarging its domain, without considering foundational corrections, is currently unsubstantiated. This is associated with the radical complexity of tasks and the challenges posed to it by the sciences leveraging its services. The original role of formalization as a means of knowledge concentration and unifying computational procedures has not been fully realized for the needs of computer science and AI, hence necessitating inevitable changes. In order to move on to these changes, we need to start by analysing the basic computational procedures [23].

Our readiness for such changes and the degree of mobility among representatives of fundamental sciences, without compromising the truth and constructiveness of the scientific structure itself, will determine the prospects of science to dominate in society and society as a whole – for survival. This is not an exaggeration, but a mere acknowledgment of the necessity for radical changes in the foundations of the classical sciences, driven by the advancement of applied sciences.

Deep learning showcases the 'enigmas of intellectualization', contingent upon dimensionality [24,25]. From our perspective, this phenomenon is entirely explicable in terms of the physiology of mental processes and its physics. We envision the solution to demonstrate such a connection in the ability to amalgamate the achievements of physiologists, biologists, AI sciences, and the phenomenon of intellectualization, provided it is experimentally validated, into a singular task.

Only a proficient, scientifically substantiated mathematical for- malization can offer us this possibility, and this is now the concern of mathematicians. The efficiency of the created formalization methodology will determine the timing for unravelling the 'enig- ma of intellectualization' and an effective algorithm for solving intellectual tasks, all within the strict framework of the updated structure of mathematical science.

The objective of this article is to initiate the process of reform starting from fundamental mathematical concepts, defined by the physiology of human thought.

Materials & Methods

The limited applicability of commonly accepted statements and tautologies in classical mathematics for theorem proof

Problem Statement

The article analyses the frequently used standard list of tautologies

The Proposed Method of Solving the Problem

Proof of the unsuitability of the modus ponens rule for proving theorems Formula of the modus ponens rule:

(1) in classical mathematics, it is invariant to the initial truth values of the component sub formulas A and B [22,23]. And it is even more invariant to the components of sub formulas A and B, if these sub formulas are composite. The modus ponens rule itself does not declare the elementary nature of sub formulas A and B [24].

However, in real life, researchers have to work exclusively with axioms (facts of full-scale experimentation with these phenomena) when formulating and proving theorems about the phenomena of the universe, which have received two alternative names in the foundations of mathematics [25]:

• elementary logical formulas,

• one-letter clauses.

And that's when the formula modus ponens:

being left alone exclusively with one-letter disjuncts, it not only does not indicate the way to obtain the truth of the conclusion from the truth of the premises in a purely theoretical way, but also puts the problem solver in front of the fact that when proving theorems, the truth of both the logical variable A and the logical variable B must be known in advance so that there are no contradictions. with the semantics of the predicate logic language, functionally fully presented in the following table 1:

Table 1: Semantics of the predicate logic language

Indeed, in this case, it can be seen from the first line that the formula (1) gets the true value when all premises are true and the conclusion of the theorem is true.

However, the semantics of the first-order predicate logic language indicates that the formula (1) can obtain a true value even with the truth values of one-letter disjuncts corresponding to lines 3 and 4 of the language semantics table. This contradicts the natural logic of human thinking, leading to paradoxical results in theorem proving. False monoliteral disjunctions reflecting the meaning of specific real axioms obtained through natural experimentation are not permissible in theorem premises. In the case of the modus ponens rule, the theorem should be considered incorrectly formulated. However, formulating any theorem correctly within the degrees of freedom in defining the modus ponens rule is fundamentally challenging.

Human thinking operates through physiological algorithms, the ultimate goal of which is survival, both personally and for the offspring (in general) [26]. Studying the surrounding world and improving it for this purpose serve as a means to achieve this goal. The process of prediction, involving hypothesis formation, is part of the cognitive process [27]. However, in each specific case, proof of the truth of our hypothesis is required for its systematic use.

We propose to collectively analyse, as a scientific community, the author's hypothesis regarding the inadequacy of the considered abstractions or rules by which we construct standard mathematical reasoning. This is how we formally think today when proving statements, both in mathematics and in other fields of knowledge, and forms the second, more significant goal of this article.

Our collective decision, if confirmed, will inevitably lead to a revision of proof rules and will affect the foundations of sciences. Everyone should be prepared for such a resolution. Special attention from the mathematical community to this issue will be the key to success.

Such reasoning indicates the limited applicability of the modus tollens rule:

in theorem proving, as the formula [2] can attain a true value even when the truth values of the single-letter disjuncts corresponding to rows 1, 2, and 4 of Table 1 in the language's semantics are true. This does not align with the natural logic of human thinking, leading to paradoxical results during theorem proving.

Similar reasoning indicates the limited applicability of the syllogism rule:

in theorem proving, as the formula (3) can attain a true value even when the truth values of the single-letter disjuncts corresponding to rows 1, 2, and 4 of Table 1 in the language's semantics are true. This also does not align with the natural logic of human thinking, leading to paradoxical results during theorem proving. Similar reasoning points to the limited applicability of contraposition: in theorem proving, as the formula [4] can attain a true value even when the truth values of the single-letter disjuncts corresponding to rows 1, 2, 3, and 4 of Table 1 in the language's semantics are true. This does not align with the natural logic of human thinking, leading to paradoxical results during theorem proving.

Thus, a profound paradox arises in the foundations of mathematics. Indeed, only one correct solution emerges from this paradox, but it fundamentally alters the understanding of the modus ponens rule, excluding it from the list of universals and triggering a crisis. The way out of the crisis lies in limiting the number of degrees of freedom when defining operands in the modus ponens rule. This rule should use exclusively true axioms that fully functionally characterize all permissible states of the observed phenomenon. These axioms should be obtained solely through natural experimentation with this phenomenon. Importantly, this requirement should apply equally to the axioms serving as premises of the theorem and those serving as conclusions. However, even with this limitation, which allows for a proper formulation of the theorem, the challenge remains to achieve a purely theoretical formal proof of the truth of the theorem's conclusion based on the truth of the conjunction of its premises in the present time.

Results

The outcome of the foregoing can be defined as an urgent necessity to consider the nature of human thinking in the creation of a modern mathematical toolkit for understanding the surrounding world. The article presents facts that, at first glance, may seem rather simple but have the potential to represent a revolution. However, identifying their presence as facts and the collection of these facts define an entirely new perspective on formalization and set a new course for the development of the sciences of thought.

Discussion

In this article, we have investigated issues related to formalization and mathematical abstractions used in fundamental sciences and artificial intelligence. Our results underscore the necessity of revisiting fundamental mathematical concepts used in scientific theory and practical applications, especially in the context of the rapid development of artificial intelligence and machine learning.

First and foremost, we raise an important question regarding the need for formal proof of statements, as the existing method of theorem proving, relying on rules like modus ponens and similar ones discussed in the article, can no longer meet the requirements for precision in modern science. Additionally, the need for cost- effectiveness in solving highly complex problems dictates a departure from spontaneity in deciding which mathematical structure or method to apply for solving an intellectual task, moving away from the behaviouristic component in the search for efficient algorithms. Despite the fantastic advancements in theoretical and practical informatics today, there is a sense that we are constructing new floors on an existing building without paying sufficient attention to the reinforcing foundation.

Our analysis of fundamental mathematical rules such as modus ponens or modus tollens, for example, shows that their initial use as abstract laws leads in certain cases to unsatisfactory results especially in mathematics itself and in the context of the development of artificial intelligence [28,29]. Rethinking these rules may require new approaches to proving theorems, perhaps clarifying existing results, but undoubtedly this is another natural step towards improving mathematical theory and formalizing our knowledge.

One of the key points of discussion is the necessity to rethink the concept of proving statements. Aligning the mathematical apparatus that implements the formalization of thinking with the level of modern knowledge about thinking is a significant task that will undoubtedly be the subject of professional debate. The value of such discussions is beyond doubt for mathematicians, as this represents a new direction in the natural process of development, as well as for a range of modern sciences where they will serve as the starting impulse for comprehensive processes of formalization and automatic formal proof of statements.

The traditional perception of mathematics as an unchanging tool for expanding knowledge may face challenges and complexities in the sciences that utilize its methods. In reality, by proposing the classical mathematical structure with a 2500-year history of formalization, we only strengthen the position of mathematics as the 'queen of sciences,' opening new possibilities for contemporary knowledge. Our work emphasizes that formalization should be at the forefront to ensure the efficient functioning of AI and related sciences.

As a demonstration of the possibility to move away from the traditional proofs defined by the rules discussed in the article for equivalent transformations during the proof of statements, we propose examining the author's formal proof method [30]. This method offers an alternative approach to establishing the validity of mathematical statements, departing from conventional rules while still ensuring rigorous reasoning and logical coherence.

Example: Solving a System of Linear Algebraic Equations using the Gaussian Elimination Method

The algorithm for solving a system of linear algebraic equations using the Gaussian elimination method [31].

In the first stage, the so-called forward elimination is performed. Through elementary row operations, the system is transformed into a row echelon or triangular form, or it is determined that the system is inconsistent. Specifically, among the elements of the first column of the matrix, a nonzero element is selected, moved to the topmost position by permuting the rows, and then subtracted from the remaining rows. This subtraction involves multiplying the first row (after permutation) by a factor equal to the ratio of the first element of each of these rows to the first element of the first row, effectively zeroing out the column below it. After these operations, the first row and the first column are mentally eliminated, and the process continues until the matrix becomes of zero size. If, during any iteration, a nonzero element is not found among the elements of the first column, the process moves to the next column, and a similar operation is performed.

In the second stage, the so-called back substitution is performed. Its essence is to express all obtained basic variables in terms of non-basic ones and to construct the fundamental solution set, or if all variables are basic, to express the unique solution of the system of linear equations in numerical form. This procedure starts from the last equation, where the corresponding basic variable is expressed (there is only one basic variable in that equation) and substitutes it into the previous equation, and so on, moving up the 'steps'. Each row corresponds to exactly one basic variable, so at each step, except the last (the topmost one), the situation precisely mirrors the case of the last row.

Let's demonstrate how the Gauss method can be used to solve the following system:

The Transformation of a Numerical Problem-Solving Algorithm into Logical Reasoning

Let's denote the equation #1 by the subject variable R1: (2x + y – z = 8) = R1 Let's denote the equation #2 by the subject variable R2: (-3x – y +2z = -11) = R2 Let's denote the equation #3 by the subject variable R3: (-2x + y + 2z = -3) = R3 According to the Gaussian elimination algorithm, the matrix is transformed into a triangular form through a step-by-step elimination of unknowns using valid elementary row operations, followed by applying row addition or subtraction operations.

Let's denote the resulting new equations that arise from transforming the matrix into a triangular form using new identifiers:

((R1 *1.5) + R2) = R4 = ((0.5y + 0.5) = 1)

(R1 + R3) = R5 = ((2y + z) = 5)

(R5 - (R4 * 4)) = R6 = (z= -1)

Substituting the value of z into R5, we obtain the value of y = 3. Substituting the values of z and y into R3, we obtain the value of x = 2.

Let's transform the provided algebraic solution model into a logical model. To do this, we will replace the subject physical variables identifying algebraic equations R1 – R6 with the corresponding logical variables, called predicates.

p1(R1, (R2, R3, R4, R5, R6, y, z)) – equation R1 is solvable in conjunction with equations (R2, R3, R4, R5, R6) and known values of variables y, z.

p2(R2, (R1, R3, R4, R5, R6, z)) - equation R2 is solvable in conjunction with equations (R1, R3, R4, R5, R6) and the known value of variable z.

p3(R3, (R1, R2, R4, R5, R6)) - equation R3 is solvable in conjunction with equations (R1, R2, R4, R5, R6)

p4(y, R5, z) – the value of y is computed by substituting z into R5.

p5(x, R3, z) – the value of x is computed by substituting z and y into R3.

Other authors have previously written about the disadvantages of the modus ponens and modus tollens rules [32-34]. The point of recognizing a certain inconsistency of these rules is to obtain grounds for moving to mandatory formal verifications of the truth of all scientific statements. And these formal checks can be in the format of automatic proofs of 1st-order logic theorems. In order to use these tools, it is necessary to find a stereotypical opportunity that allows you to move from a meaningful proof to a formal one. This task was solved by the author's stereotype of the logical construction of thinking for meaningful and formal proof of theorems, created considering the peculiarities of human thinking [14].

The logical conjunction of predicates p1...p5 ensures obtaining the solution (predicate p6(x, y, z)) of the system of equations R1...R3 using the Gauss method.

((p1(…) p2(…) p3(…) p4(…) p5(…)) p6(x,y,z)) ((p1(…) p2(…) p3(…) p4(…) p5(…)) p6(2,3,- 1)) (1)

Using formulas for equivalent transformations, let's simplify the expression of formula (1).

We will denote the formula by the identifier F1 (...):

(p1(…) p2(…) p3(…) p4(…) p5(…))

F1 (…) = (p1(…) p2(…) p3(…) p4(…) p5(…)).

Then formula [1] will have the form:

(F1 (…) p6(x,y,z)) (F1 (…) p6(2,3,-1)) (2)

There are 27 formulas of equivalent transformations in the first- order predicate logic language. Let's use several formulas to transform formula (2) into a canonical form:

(F1 (…) p6(x,y,z)) ( F1 (…) V p6(2,3,-1)) (3.1)

F1 (…) V p6(2,3,-1)                                       (3.2)

p6(x,y,z))                                                        (3.3)

F1 (…)                                                              (3.4)

From the set of formulas (3.2) – (3.4), we obtain an empty resolvent, which will correspond to a successful proof of the theorem. Comparing (3.2) first with (3.4), and then with (3.3), we obtain an empty resolvent on the second step.

The results of solving the problem are assigned to the corresponding variables at the moment of eliminating empty resolvents. In our case, on the last step, the variables obtained their values:

                                                                        x = 2; y = 3; z = -1.

The statement is proven.

The more detailed description of the formal method of proof could be the subject of a future article. The purpose of this article is to emphasize the importance of transitioning from traditional theorem proving to a formalized procedure.

In addition, we emphasize the need to integrate various disciplines, including physiology, biology, artificial intelligence and mathematics, for a deeper understanding of intellectualization. Proper mathematical formalization can provide a path to the creation of effective algorithms for solving intellectual problems in all spheres of society.

Thus, the purpose of our article is to initiate a scientific discussion about the prospects of research. We are faced with the task of clarifying fundamental mathematical concepts in order to better adapt them to modern challenges and tasks. This is a difficult task that requires flexibility and the active participation of scientists to ensure the stability and development of society [34-38].

Author Contributions

Conceptualization and methodology, Viktoria Kondratenko; validation, Viktoria Kondratenko, Leonid Slovianov; formal analysis, Viktoria Kondratenko; investigation and resources, Viktoria Kondratenko; data curation, Leonid Slovianov; writing— original draft preparation, Viktoria Kondratenko; visualization and supervision, Leonid Slovianov. All authors have read and agreed to the published version of the manuscript.

Conflicts of Interest

The authors declare no conflict of interest

Acknowledgements

Authors want to thank Professor Alan Bundy and Professor Igor Goryanin for their guidance, patience, enthusiastic encouragement, and constructive critique of this research work. In addition, their generosity in donating his time has been greatly appreciated. We also want to thank them for their encouragement and support.

References

1. Sniekers, S., Stringer, S., Watanabe, K., Jansen, P. R., Coleman,J. R., Krapohl, E., ... & Posthuma, D. (2017). Genome-wide association meta-analysis of 78,308 individuals identifies new loci and genes influencing human intelligence. Nature genetics, 49(7), 1107-1112.
2. Carson, J. (2017). Genetics: Recipe for intelligence. Nat Hum Behav 1, 0135
3. Wolfram, Stephen. "Remembering Doug Lenat (1950– 2023) and His Quest to Capture the World with Logic." Stephen Wolfram Writings. September 5, 2023. writings. stephenwolfram.com/2023/09/remembering-doug-lenat- 1950-2023-and-his-quest-to-capture-the-world-with-logic.
4. Douglas Lenat on MCC and Artificial Intelligence. Computer compacts 3.3 (1985): 102–103.
5. Elkan, C., & Greiner, R. (1993). Building large knowledge- based systems: Representation and inference in the cyc project. Artificial Intelligence, 61(1), 41–52.
6. Lytvynenko, Volodymyr, and Sergii Babichev, eds. Lecture Notes in Data Engineering, Computational Intelligence, and Decision Making: 2022 International Scientific Conference “Intellectual Systems of Decision-Making and Problems of Computational Intelligence”, Proceedings / Sergii Babichev and Volodymyr Lytvynenko, Editors. Cham, Switzerland: Springer Nature Switzerland AG, 2022. Print.
7. Liu, Dongjingdian et al. (2020). “A behavioral recognition algorithm based on 2D spatiotemporal information extraction.” Zhineng Xitong Xuebao = CAAI Transactions on Intelligent Systems 15.5, 900–. Print.
8. Wechsler, S. P., & Bhandawat, V. (2023). Behavioral algorithms and neural mechanisms underlying odor- modulated locomotion in insects. Journal of experimental biology, 226(1), jeb200261.
9. Hu, Z., Petoukhov, S., Yanovsky, F., & He, M. (2022). Advances in computer science for engineering and manufacturing. In Lecture notes in networks and systems.
10. Atanasov, Krasimir, ed. Research in Computer Science in the Bulgarian Academy of Sciences / Krassimir T. Atanassov, Editor. Cham, Switzerland: Springer, 2021. Print.
11. Varbanescu, A. L., Bhatele, A., Luszczek, P., & Marc,B. (Eds.). (2022). High Performance Computing: 37th International Conference, ISC High Performance 2022, Hamburg, Germany, May 29–June 2, 2022, Proceedings (Vol. 13289). Springer Nature.
12. Outerbounds Introduces New Platform Features to Help Organizations Build Custom Generative AI and LLM Solutions: Platform Innovations Help Enterprise Customers Prepare for Rapid Growth in Their Data, ML, and AI Initiatives. New York: NASDAQ OMX Corporate Solutions, Inc, 2023. Print.
13. Vital Releases Doctor-to-Patient Translator That Uses AI and LLMs to Transform Medical Jargon into Simple, Accurate Content for Patients. New York: Business Wire, 2023. Print.
14. Kondratenko, Viktoria. Creation of a single stereotype of the logical construction of thinking for meaningful and formal proof of theorems. Kyiv. “Aleph". 2010, 267 p. Print.
15. Kondratenko, Viktoria, Tarinskaya, Olga. Formalization of knowledge on the physiology of the human body on the example of providing the human body with the necessary dynamic balance of minerals. Computer mathematics. – 2014 Issue 2, p.29. Print.
16. Cifarelli, V. V., & Cai, J. (2005). The evolution of mathematical explorations in open-ended problem-solving situations. The Journal of Mathematical Behavior, 24(3-4), 302-324. Web,
17. Byers, W. (2010). How mathematicians think: Using ambiguity, contradiction, and paradox to create mathematics.
18. Foukzon, J. (2022). Internal set theory IST# based on hyper infinitary logic with restricted modus ponens rule: nonconservative extension of the model theoretical NSA. Journal of Advances in Mathematics and Computer Science, 16-43.
19. Alfred North Whitehead and Bertrand Russell 1927 Principia Mathematica to *56 (Second Edition) paperback edition 1962, Cambridge at the University Press, London UK. No ISBN, no LCCCN.
20. Koenig, E. C. (1995). Analysis for correct reasoning in interactive man-robot systems: Disjunctive syllogism with modus ponens and modus tollens. In Artificial Intelligence in Industrial Decision Making, Control and Automation (pp. 89- 97). Dordrecht: Springer Netherlands.
21. Walton, D. (2002). Are some Modus Ponens arguments deductively invalid?. Informal Logic, 22(1).
22. Zhaoping, L. (2020). Artificial and natural intelligence: from invention to discovery. Neuron, 105(3), 413-415.
23. Thomason, R. (1989). Philosophical logic and artificial intelligence. In Philosophical Logic and Artificial Intelligence (pp. 1-7). Dordrecht: Springer Netherlands.
24. Woschank, M., Rauch, E., & Zsifkovits, H. (2020). A review of further directions for artificial intelligence, machine learning, and deep learning in smart logistics. Sustainability, 12(9), 3760.
25. Kotsiopoulos, T., Sarigiannidis, P., Ioannidis, D., & Tzovaras,D. (2021). Machine learning and deep learning in smart manufacturing: The smart grid paradigm. Computer Science Review, 40, 100341.
26. Daley, Alexandra. (2015). Survival Instinct. Crazyhorse (Little Rock, Ark.) 87: 28–. Print.
27. Mumford, M. D., Giorgini, V., Gibson, C., & Mecca, J. (2013). Creative thinking: Processes, strategies and knowledge. In Handbook of research on creativity (pp. 249-264). Edward Elgar Publishing.
28. McGee, Vann. (1985). A Counterexample to Modus Ponens.The Journal of philosophy 82.9 462–471.
29. Yalcin, S. (2012). A counterexample to modus tollens. Journal of Philosophical Logic, 41, 1001-1024.
30. Kondratenko, Viktoria, Kondratenko, Oleksandr. “Theory and Practice of Artificial Intelligence in Automated Theorem Proving””. Scientific publication "Poligrafkniha", Kyiv, 2006, Print.
31. Gauss elimination method. https://byjus.com/maths/gauss- elimination-method/#:~:text=(1)%20Write%20the%20 given%20system,as%20an%20upper%20triangular%20 matrix. Web.
32. Kolodny, N., & MacFarlane, J. (2010). Ifs and oughts. The Journal of philosophy, 107(3), 115-143.
33. Walton, D. (2002). Are some Modus Ponens arguments deductively invalid?. Informal Logic, 22(1).
34. Charlow, N. (2023). Modus Ponens and the Logic of Decision.Journal of Philosophical Logic, 52(3), 859-888.
35. Li, W. H., Qin, F., & Xie, A. F. (2022). Modus Ponens property of T-power based implications. Fuzzy Sets and Systems, 431, 129-142.
36. Fisher, T. K. (20219). “Counterfactual Dependence and Causation’s Arrows.” ProQuest Dissertations Publishing.
37. Gispert, J., & Torrens, A. (2014). Lattice BCK logics with Modus Ponens as unique rule. Mathematical Logic Quarterly,60(3), 230-238.
38. Kahle, Reinhard., Thomas. Strahm, and Thomas. Studer, eds. Advances in Proof Theory Edited by Reinhard Kahle, Thomas Strahm, Thomas Studer. 1st ed. 2016. Cham: Springer International Publishing, 2016. Web, https:// ed. primo. exlibrisgroup. com/ view/ action/ uresolver. do? operation = resolveService & package service_id = 44451048670002466 &institutionId = 2466&customerId = 2465 & VE = true.