The concept of software shell for interactive mathematical proof verification systems is presented. The underlying formal logical system, which is approximated to the mathematical practice of constructing proofs, and the mechanisms for its extension are considered. Languages for representation of bases of formalized mathematical knowledge and reasoning methods, as well as the general syntactic structure of proofs are described.
constructing proofs. The mechanisms for its extension that can be used as the basis for such a shell are also described. 2
As known, mathematical dialect and methods of mathematical reasoning are not only unfixed, explicitly specified, but continue to evolve with the development of mathematics. Therefore, there is no possibility to construct such a fixed formal system that could be used as a basis for ITP, and which “projection” from the mathematical dialect language would not be extremely cumbersome and difficult to carry out for most mathematicians. In order to be able to approximate formal logical systems to mathematical practice, they must be extensible. The possibility of extending them should be provided not o nly by the developers of the ITP, but first of all by the users of such systems – members of the mathematical community.
One of the ways to provide such an opportunity is to develop a software shell (an instrumental metasystem) for them that would allow creating applied ITPs, which are already based on the core of a formal system approximate to mathematical practice, and providing mechanisms for extending this system. The following components of formal systems should be extensible and changeable: the language for mathematical knowledge representation, which describes the axioms, theorems, lemmas, definitions, etc., and the set of formalized methods of reasoning, available for mathematicians for constructing theorem proofs. In order to achieve this, the methods of reasoning must be presented explicitly (in declarative form), and the language for formalized reasoning method representation must be extensible. Note that these languages are equivalent to the logical language of higher orders and do not support graphic images, geometric figures and interpretations of various constructions: commutative diagrams, Euler-Venn diagrams, etc.
To ensure the extensibility of formal systems at their development stage, an approach based on context
dependent grammars and ontologies is used. Extensibility is achieved by the fact that context-dependent
grammars of the abstract syntax for the languages of mathematical knowledge representation and formalized
reasoning methods have an explicit declarative representation specified in accordance with the metamodel [
The rest of the paper is devoted to a brief description of the core and the extension mechanisms of the formal system, which can be used as a theoretical basis for applied ITPs created with the use of the shell. Like any formal-logical model, the described formal system defines a formal language for the mathematical knowledge representation – axioms, definitions, theorems, lemmas and other mathematical statements; and the calculus (consistent with this language), in which the correct complete proofs should be constructed. The description of calculus includes the definition of methods for proving mathematical statements; the reasoning methods available to mathematicians in the process of constructing theorem proofs, and the formal language for their representation; proof ontology model – a structure for representing a complete proof.
Finally, it is important to note that the reasoning practice of modern mathematics, which is based on the
principle of structuralism, as well as the concepts of isomorphism, equivalence (identity) of mathematical
objects [
For the purpose of structured storage and accumulation of mathematical knowledge, this section introduces an ontology model that specifies the network structure of various mathematical sections and knowledge bases.
Each section of mathematics has its own name and may contain the following: a set of definitions allowing to
introduce new ones to refer to defined concepts, as well as set meanings of these definitions; a set of axioms; a set
of theorems and lemmas, each of which can have a set of corollaries; a set of named subsections (Figure 1).
Hereinafter, the notation of the labeling of vertices and arcs for the digraphs shown in the figures coincides with
the notation used in [
- else if is a variable, then its declaration must have the form : tt1 … ttm → tt, if m 1, of : tt1 → tt, if m = 1.
The extension of the language for mathematical statement representation is provided by the addition of new types of terms and formulas. It consists of adding a new construct to the grammar digraph of the language, describing the abstract syntax of this new construct, adding the necessary rules to the text grammar of the language, and possibly describing the context conditions associated with the new construct.
The mathematical knowledge base is formed in accordance with its ontology model. Extension of the mathematical knowledge base is to add new mathematical knowledge – definitions, axioms, theorems and lemmas (as well as their corollaries) to existing sections of mathematics; and to create new sections / subsections of mathematics and filling them with relevant mathematical knowledge. 5
Calculus, within which a proof is constructed, includes methods of proving goals based on three rules. Before describing the rules themselves, we define the concept of a goal and a true statement. A goal is a pair: mathematical statement and a possibly empty list of assumptions – a set of mathematical statements, which truth results in the truth of this statement.
By a true statement we mean a mathematical axiom, a definition, a theorem/lemma (as well as its corollary), for which a proof has already been constructed, or a method of reasoning (see section 6 for more details). Definitions and axioms are considered correct by agreement between members of the mathematical community.
Next, we describe the inference rules of the calculus.
1. The rule of implication (natural deduction). It allows to reduce the proving of the goal, for which the mathematical statement has the form of implication f1 & … & fk f, and a list of assumptions is p1, …, pn (n 0), to the proving of a goal which mathematical statement is the consequent of this implication – f, and a list of assumptions is p1, …, pn, f1, … , fk.
2. Matching rule. If is a true statement, and there is a substitution of instead of variables in , such that the
result of applying this substitution to coincides with the mathematical statement f of the goal being proved or is
syntactically equivalent to f, then f is true (f is a concretization of ). The list of assumptions for the goal is empty in
this case. It should be noted that the matching is a unidirectional version of unification [
3. Modus ponens. It is used to decompose a goal, decompose some assumption from the list of assumptions of a goal, or to perform inference.
3.1. Goal decomposition. If it is necessary to prove a goal which list of assumptions is p1, …, pn, (n 0), and mathematical statement f can be matched with the consequent of a true statement, having the form of 1 & … & m , and – is the most general unifier of f and , then this proving is reduced to proving of goals, which mathematical statements f1, …, fm are respectively the results of applying the substitution to statements in the antecedent of this f1 = 1, …, fm = m, and a list of assumptions of each goal is p1, …, pn.
3.2. Assumption decomposition. If it is necessary to prove a goal which mathematical statement is f, and a list of assumptions is p1, …, pi, …, pn (n 1), and assumption pi can be matched with the RHS of the equivalence of the true statement, which has a form of 1 | … | m (1 … m ), (m 2), and is the most general unifier of pi and , then this proving is reduced to proving of m goals, which mathematical statement is f, and lists of assumptions are p1, …, pp1, …, pn, where pp1 is the result of applying the substitution to 1; …; p1, …, ppm, …, pn, where ppm is the result of applying the substitution to m.
3.3. Inference, which is a sequence of inference steps.
An inference step is the following. Let the mathematical statement fi (i = 1, …, m) be either an axiom, or a definition, or a proven theorem/lemma (or its proven corollary), or a statement from the list of assumptions of the goal being proved, or the result of one of the previous inference steps. Then if the statement f1 & … & fm can be matched with the antecedent of a true statement that has the form 1 & … & m , and is the most general unifier for f1 & … & fm and 1 & … & m, then the statement f is true, which is the result of applying the substitution to (inference step result). The goal is considered proven if the result of the last inference step of the conclusion is a statement that coincides with the mathematical statement of the goal, or is syntactically equivalent to it.
In the case of goal decomposition (3.1) and inference (3.3), the Modus ponens application can be generalized to the case when the implication is replaced by equivalence. 6
Methods of reasoning, which are used in the methods of proof, are divided into two classes: - based on propositional tautologies underlying logical reasoning; - based on mathematical principles and statements about syntactic transformations of mathematical expressions.
These methods of reasoning are represented explicitly by propositional formulas, which are tautologies, and metamathematical statements, respectively. Metamathematical statements are considered correct if their validity is established on the basis of an intuitive or conventional (as a result of an agreement between members of the mathematical community) criterion. Thus, the proof is considered correct if the validity of all metamathematical statements used in it is accepted.
Each propositional tautology has the form: v1 … vn pf, where pf is a propositional formula containing the occurrences of propositional variables v1, … vn, and vi (i = 1, …, n) is the description of the propositional variable vi, n 1. The value of a propositional variable can be one of the logical constants – true or false.
There are the following context conditions for propositional variables.
1. For each using occurrence of a variable in a propositional formula, there is a defining occurrence of this variable in the prefix of this formula.
2. For each defining occurrence of a variable in the prefix of a formula, there exists a using occurrence of this variable in the body of this formula.
The generative graph grammar, which describes the abstract syntax of the language for metamathematical statement representation (metalanguage), is shown in figure 3. Each metamathematical statement is represented by a vertex of the graph grammar «Mathematical statement» and has a form: (v1: t1) … (vn: tn) t1 … tk f1 … fs i1 … ip r1 … rq f. Here f – a mathematical formula, containing occurrences of object variables v1, …, vn, as well as occurrences of syntactic variables t1, …, tk of type t, syntactic variables f1, …, fs of type f, syntactic variables i1, …, ip of type i and syntactic variables r1, …, rq of type r. Herein (vi: ti) (i = 0, …, n) is a description of the object variable vi, ti is a mathematical term, which value is a set (range of possible values of the object variable vi); t1 … tk are descriptions of syntactic variables of type t (k 0), which values are terms; f1 … fs are descriptions of syntactic variables of type f (s 0), which values are formulas; i1 … ip are descriptions of syntactic variables of type i (p 0), which values are integer constants; r1 … rq are descriptions of syntactic variables of type r (q 0), which values are real constants; where k + s + p + q 0.
The metalanguage is a superstructure on the language for mathematical statement representation and is obtained by extending the «Formula» and the «Term» constructions of this language. The «Formula» construction is extended by adding two alternatives: «Syntactic variable of type f» and «Modified syntactic variable of type f». The «Term» construction is extended by adding four alternatives: «Syntactic variable of type i», «Syntactic variable of type r», «Syntactic variable of type t», and «Modified syntactic variable of type t».
The modified syntactic variable contains a modifier in addition to the name. The variable is a term or formula depending on its type. The modifier consists of modifier elements, each of which is a term or a formula. The value of such a syntactic variable is a syntactic construction, which corresponds to the variable’s type, and contains formal parameters. Each modifier element corresponds to its own formal parameter, which can be included in the value of Metamathematical statements are considered valid for any legal values of syntactic (including modified) variables.
For the language for metamathematical statement representation, the following context conditions for syntactic variables are formulated: 1. each metamathematical statement must include at least one syntactic variable; 2. for each using occurrence of a syntactic variable in a term or a formula of a metamathematical statement, there is a defining occurrence of this variable in the prefix of this statement;
3. for each defining occurrence of a syntactic variable in the prefix of a metamathematical statement, there is a using occurrence of this variable in the term or formula of this statement;
4. a modifier of a modified syntactic variable cannot contain both direct and indirect occurrences of the same syntactic variable;
5. a syntactic variable can be included in a metamathematical statement either unmodified or modified (but not in both ways); 6. if a syntactic variable is modified, then it must be included in the metamathematical statement at least two times; 7. the number of modifier elements in all occurrences of the same modified syntactic variable in the metamathematical statement is the same, and at appropriate places in the modifier there must be either terms or formulas.
The definition of a metalanguage as a superstructure on the language for mathematical statement representation (that is, as its extended language) is a sufficient condition for the metalanguage to extend automatically when the language for mathematical knowledge representation extends. This is true due to the method of defining the «Formula» and the «Term» metalanguage constructions through the same constructions of the mathematical knowledge representation language, which are extended by the corresponding syntax variables (see figure 3), and also by adhering the context condition 1 for the syntactic variables. Thus, the extension of these two languages occurs simultaneously.
The base of formalized reasoning methods consists of a variety of those, modeled by propositional tautologies, and a variety of those, modeled by metamathematical statements. Extension of the base of formalized reasoning methods is in extending the set of propositional tautologies and/or the set of metamathematical statements. The set of propositional tautologies is extensible due to the possibility of formulating new propositional formulas, which, in case of successful automatic verification of their validity, are added to this set. The set of metamathematical statements is extensible due to the possibility of formulating new statements that are included in this set. In particular, it should be noted that if new quantifiers are added to the language for mathematical knowledge representation, it becomes necessary to add metamathematical statements about the properties of these quantifiers. 7
The complete proof is a syntactic structure, which is a set of related goals. The first goal is the theorem/lemma being proved, for which there is no list of assumptions. Each goal has a proof method, associated with it. The set of admissible methods for proving a goal is an improper subset of the set of methods described in Section 5. The number of methods can vary from three to five – depending on the syntactic form of the goal’s mathematical statement (whether it has the form of implication or not) and the presence or absence of its assumptions. The syntactic structure of each proof method is based on its semantics (see Section 5). In the case of using the Modus ponens rule for goal decomposition or inference, the following is taken into account: the form of true statement (implication or equivalence) and the rules for choosing values for the premises. A premise is conjunct from the implication antecedent or from the equivalence side, which is considered to be an antecedent.
In the case of goal decomposition, the values for the premises can be chosen from the statements stored in the mathematical knowledge base, in the set of proven statements, and in the list of assumptions of the goal being proved (if it has assumptions).
In the case of inference, the values for premises can be selected from all three sets of statements mentioned above, and from statements that are results of already performed inference steps (if at least one inference step has been performed). 8
The paper presents the concept of a software shell for systems of intuitive mathematical proof verification. The core of the formal logical system, which is approximated to the mathematical practice of constructing intuitive mathematical proofs, is specified, and the mechanisms for its extension are considered. This formal system can be used as the basis for proposed shell. The declarative specifications of extensible languages for representation of mathematical knowledge and formalized methods of reasoning, as well as model of complete proofs, have been developed. The language for formalized reasoning method representation consists of two sublanguages: the language for propositional tautology representation and the metalanguage.
Only the language for mathematical knowledge representation has mechanisms of extension. The metalanguage, by the method of definition, extends automatically as the former is extended. The extensibility of the language for mathematical knowledge representation is provided by the extensibility of the set of definitions, allowing to introduce new ones to designate the defined concepts, as well as the extensibility of its grammar. The latter is achieved through the aids for describing the syntax of new constructions of the language for mathematical statement representation, as well as, if necessary, context conditions. The calculus, within which proof is constructed, is presented explicitly and is extensible.
The solution for the problem of the consequence of the mathematical proposition truth from its provability may be entrusted to specialists in mathematical logic. Their task in this case is to verify the methods of reasoning specified by mathematicians on the metalanguage. As a result of the analysis a class of axioms can be distinguished among the metamathematical statements, and the rest are classified either as requiring proof or as incorrect. Thus, proofs that use incorrect or unproved metamathematical statements cannot be considered true.
The results obtained in this research can be used in a project for the development of a QED-system as well as in projects for the development of controlled ITPs, which are approximations to such project.
This work was partially supported by RFBR (projects nos. 17-07-00299 and 19-07-00244) and by PFI "Far East" (project no 18-5-07).