Proof Versus Understanding in Mathematical Proof
The interpretation of the nature of mathematical proof contrasts its two interpretations: as understanding and as calculations. The concept of rigorous proof is due to Alfred Tarski; according to it, mathematical proof is a sequence of sentences starting with axioms, each of which is a logical consequence of previous sentences. According to this ideal, rigorous proof breaks the real "train of thought" of the mathematician into small steps, each of which is authorized by the rules for deriving the formal system. But real mathematical practice completely avoids the realization of such an ideal, while implying that the ideal is true "in principle". Thus, in a real mathematical proof there are two hypostases: (1) a "substantive" proof that operates with concepts, definitions, informal verbal turns and (2) a "formal" proof, whose signs are devoid of any meaningful meaning. Both hypostases are connected by the concept of interpretation, giving intentional meaning to signs of formal evidence. One is intended to convey the thought, content of concepts, and the other is to observe the rigor of this transmission in order to prevent its distortion and, even more so, the loss of truth of statements. Formal proof in itself does not give understanding since the signs in the sequence of formulas do not matter for a logical conclusion. Of course, there is an implied or intentional interpretation of these signs, but it joins the signs from the outside; it joins the already existing formal system, which has a kind of autonomy. Therefore, it can be assumed that mathematical understanding is not based on the practice of mathematical derivation, but on some other aspect of mathematical practice. It is the fact that non-logical constants have many potential interpretations that requires maximum rigor from mathematical discourse. In addition, according to Gottlob Frege, mathematicians develop systems of written signs not to do without any content, but to express the content in such a way that rigorous reasoning can be built on the basis of this content. This means that the sources of semantics can be based on notational features. Thus, mathematical proof, although it is constructed as a strictly defined sequence of syntactic operations, implies the "entry" of semantic content into syntactic means, for example, in the case of notation and interpretation of non-logical constants.