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

Abstract

Viktoria Kondratenko and Leonid Slovianov

The intellectual activity of a person is realized by some kind of biological tools, suggesting the possibility of its inheritance, and scientific knowledge forms and concentrates its intellectual assets. Biological tools are able not only to operate with the assets of human intelligence, but also to carry out a complex of computational operations on the received signal information, determined by the functions of the vital activity of the human body. The description of this process through abstractions defines the foundation of mathematical science.

Knowledge about the architecture of intellectual activity must 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. In particular, this necessity concerns the permissibility of certain operations mentioned in order to obtain a scientifically based solution to problematic tasks. 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. The proof of the truth of certain statements and the rules applied as obvious means for it must also meet the high bar of modern knowledge about the biological essence of intellectual activity. Otherwise, operating errors, increasing many times when scaled by AI, will inevitably generate errors and dead ends in improving scientific knowledge and means of intellectualization. The article is devoted to the paradoxes in mathematical science that create conflict due to the increased requirements for the formalization of knowledge and the mathematical tools available for them today, as well as proposals for their elimination.

This article is the first step in justifying the need to use a formal stereotypical logical proof due to the shortcomings of a meaningful proof of theorems. The article shows how the formal proof will look like using the given example. Thanks to the appearance of this structure of thinking, it becomes possible to formulate a logical objective theorem for the numerical solution of a system of linear algebraic equations using the Gauss method. The formulation of this theorem in a logical format does not violate the structure of the substantial proof that exists today and allows us to formally verify this substantial proof for truth or propose a logical solution with mandatory formal verification.

PDF