in logic, the process (method) of establishing the truth; the grounding of the validity of a proposition.
Corresponding to the different possible aspects and levels in the investigation and use of the concepts “truth” (“validity”) and “grounding,” the term “proof allows a number of interpretations that differ from one another in degree of generality and definiteness. However, in all the modifications of the concept of proof, two opposed (but interconnected) tendencies can be clearly traced. The first is conditioned by the relativity and the contextual nature of the concept of truth, since it designates a more or less exact and complete correspondence to some part of reality. The second is connected with the requirement that a proof (precisely as a proof, and not simply as a reason in favor of the assertion in question) should guarantee the truth of the thesis—in this lies the specific character of the concept of a proof that distinguishes it from the broader class of procedures that could more naturally be called confirmation of theses and happen to be more or less convincing. In other words, a proof should serve as a complete confirmation of the truth of the proposition being proved and therefore should be of a deductive nature—hence the tendency to an increasingly greater formalization of the concept of a proof.
Thus, the concept of a proof contains a profound contradiction: this concept is genuinely necessary for solving problems that in principle do not permit a complete, exhaustive, definitive solution. However, one can find this concept in the ideal form of complete definiteness only in those situations in which the solution, in some sense, has been predetermined and is already contained in the very statement of the problem—when it is possible to achieve a proof of logically true propositions, the only ones for which one can carry out a proof that is completely formalized (and thus leaves nothing indefinite or inexplicit).
The opposition of the contextual and formal aspects of the concept of proof appears primarily in the difference between the broad and narrow senses of this term.
Proof in the broad sense is any procedure for establishing the truth of a proposition (which is called the thesis, or conclusion, of the given proof) both with the aid of certain logical inferences and by means of sense perception of certain physical objects and phenomena, as well as of references to (indications or mentions of) such perceptions. This is precisely the character of proofs in legal practice, where the term “proof applies to singular indications of this kind and even to the naming of the objects indicated—hence the expressions “to produce proof (evidence)” and “material proof.” Such is the mode of grounding most assertions in the humanities, and, in an even more distinct form, the empirical (experimental, based on observational data) proofs in the natural sciences. All such proofs (if we do not consider the proofs of certain singular facts leading to an immediate inference from a single “production of evidence”) have as components deductive fragments—inferences that connect the references to experience with the thesis being proved (or an intermediate thesis). Nevertheless, all these proofs can be considered inductive: there occurs in them a transition from particular premises to general conclusions (induction), a transition carried out (most frequently in an implicit form) according to the rules of inductive logic.
Proofs in the narrow sense of the word, which are characteristic of the deductive sciences (logic, mathematics, and the divisions of theoretical physics and theoretical cybernetics that are structured according to their example and on their basis), are chains of (correct) inferences that lead from true premises (propositions primitive to the given proof) to the theses being proved (the conclusions). The premises of a proof are also called its grounds, arguments, or reasons. However, these terms are no less applicable to the designation of the intermediate transitions from premises to a conclusion or of any type of explanation (commentaries) that accompanies such transitions in these proofs. The truth of premises should not be substantiated in the proof itself, but should in some way be established beforehand.
The consistent development of this traditional conception of proof (derived from Aristotle), when it was connected with the axiomatic method, required at the end of the 19th century its considerable refinement and even revision. Although the acceptance of axioms as true propositions still agreed with classical notions (it was sufficient, it seemed, to require that they be empirically grounded), the discovery of the possibility of constructing different axiomatic systems (for example, non-Euclidian geometries) that are suitable, at least in principle, for describing the same physical reality, made it necessary to abandon the notion of axioms as either “self-evident truths” or empirical truths. Such a notion (which proceeds from as far back as Greek science) contradicted, so it turned out, the possibility of accepting as axioms of the different geometric systems (but, of course, not of one and the same system) assertions that are negations of each other. It also contradicted the possibility discovered in this connection of placing at the basis of scientific theories (and thereby also as premises of a proof) propositions the question of whose truth is not only not predetermined from the beginning but may not even be raised. In other words, there emerged a relativity in the opposition of the concepts of a deduction (from a hypothesis) and a proof—since axioms (independently of their hypothetical “truth” or “falsity”) are the hypotheses on which the proof is based.
But this revision of the concept of proof, which was carried out at the turn of the century by D. Hilbert, was not entirely consistent. In connection with the increasingly acute problems of the noncontradiction of scientific theories (confidence in which could no longer be based on confidence in the truth of the fundamental propositions of the theory), Hilbert advanced a program for formalizing the proof of deductive theories that proposed not only a clear indication of all the primitive concepts and primitive propositions (axioms) of any given theory but also an equally clear indication of all the logical procedures used in the deductions (in particular, in the proofs) of this theory. With such a formulation of the question, the problem of the persuasiveness (correctness) of a proof takes on (for the first time!) a completely objective character.
The proof (more correctly, the formal proof) is regarded simply as a “string” of formulas each of which either is an axiom (that is, belongs to some previously isolated list of well-formed formulas) or immediately follows one of the rules of inference (which are also precisely listed) from the preceding formulas of the string. The conclusion of the given proof is simply its last formula (in particular, the proof of any axiom consists of one formula—itself). With such a treatment, the scientific theory being examined ceases to be a theory in the ordinary sense: it turns out to be represented in the form of a calculus, or formal system, that consists of formulas obtained from formulas of some basic store (axioms) by means of the purely “mechanical” application of the rules of inference (the application of which, like the verification of the correctness of this application, does not pre-suppose any material understanding of them). A formula for which there is a formal proof is called a proved formula or a formal theorem.
Thus, the carrying out of this part of Hilbert’s program permitted the realization of the ideal advanced much earlier by G. W. von Leibniz: “to replace reasoning by calculation.” To ascertain whether a given string of formulas is a proof, there is a simple, uniform, and moreover, strictly mechanical method—the algorithm. Such an algorithm for determining whether a given arbitrary formula is a theorem is possible only for a few, relatively simple, formal theories, but this fact does not exclude the possibility of a search by a machine for a deduction (a search for a proof) for many important classes of formulas. The elaboration of such mechanical algorithms of inference is one of the goals of mathematical logic, the theory of algorithms, and theoretical cybernetics.
The presentation of proofs as strings (linear sequences) of formulas is not the only possible one; often it is more convenient to define formal proofs as “trees” of formulas whose “branches” are formed by the premises through applications of the rules of inference. Such a form of proof turned out to be convenient, in particular, for the study of logical inferences that the German mathematician G. Gentzen undertook in 1934 within the framework of Hilbert’s proof theory. In his modifications of the logical calculus in the form of the so-called calculus of natural deduction, the formal logical means are closer in their structure to traditional (material) methods of inference than in Hilbert’s initial scheme. There are no axioms (or very few of them) in these calculi, but auxiliary rules of inference are introduced, so that as a result the overall “store of theorems” derivable by the new and the former means proves to be the same. Thus, the difference between formal axioms and material rules also proves to be relative.
The consistent formalization of the concept of proof reveals the possibility of transferring many “creative” human functions to computers. But this does not result in the conclusion that it is possible to reduce all material aspects of the concept of proof to formal aspects—the rules of inference, although they do deal with formal objects (formulas), are formulated in a natural language, while all problems concerning the nature of formal calculi as a whole are raised and resolved by purely intuitive means. These intuitive arguments (and intuitive proofs) constitute an object of proof theory itself.
Moreover, it turned out (K. Godel, 1931) that the task of a complete and consistent formalization of even such relatively simple mathematical theories as arithmetic (number theory) is in principle unrealizable. Therefore, in them there is always some “remainder that cannot be formalized.” Finally, no formalization of deductive theories eliminates the problem of their interpretation, that is, finding the correspondence to some reality that they describe and that is external to them (and, perhaps, consists of objects of a high level of abstraction). In the final analysis, the adequacy of this correspondence can only be shown by the grounding of the truth of the theory as a whole. It is natural that within the framework of mathematical logic ever-increasing influence has been exerted by that part of the doctrine (an alternative to Hilbert’s conception) of mathematical intuitionism (a doctrine that, to a considerable extent, is accepted by the representatives of the constructivist trend) according to which the concept of rigorous mathematical proof (to say nothing of the general concept of proof) cannot in general be exhausted by any formal definition given once and for all.
An even more resolute revision of the notions about the essence of axiomatic-deductive methods has been undertaken within the framework of the so-called ultraintuitionistic program. Ultraintuitionism is characterized by the attempt at a consistent and strict observance, as applied to the deductive sciences, of the principle of sufficient reason. On the one hand, it suggests an extremely broad understanding of intuitive (deductive) proof and, on the other, advances a conception of formal proof that, taking into account both Hilbert’s “formalistic” scheme and the intuitionistic criticism of that scheme, is at the same time so flexible that its use allows us to hope that in problems of the foundation of mathematics and logic the limitations stipulated by Gódel’s results, which previously seemed insurmountable, will be overcome.
IU. A. GASTEV