S.L. Katrechko

FROM LOGIC TO PROOF-SEARCH THEORY

Proof-search theory (PST) - the area of intersection of Logic and Heuristic, which investigates possible methods of «problem solving» («how is it possible to build a proof?») in some logical calculus.

Let me illustrate specifity and basic ideas PST with the help of the simple example of a derivation of the formula [р É р] in Church’s calculus P1 [1]. On p.75 the sequence from 9 formulas is given. The question of PST is following: «Why on 1 (2, 3... 8) step were selected those or other axioms, rules of inference and substitutions?», i.e. in this case it is interesting not a problem about a regularity of a logical deduction (it is interesting for Logic), but a problem of understanding of the process of a construction (search) of a derivation. The applied value of this question consists in learning a student or computer to build (to search) similary derivations.

Basic idea of PST - transition from logical calculi to metacalculi (calculi of proof-search) , within the framework of which there is a possibility to take into account a structural information of logical formulas useful for proof-search. This idea can be realized by two modes:

· by introduction purely admissible (derived) metarules of inferences;

· by method of a dummy variables (metavariables), function of which consists in fixing (complete or incomplete at the given stage of a derivation) information about a possible structure of the derivated formula, and in consequent, with obtaining an additional necessary (complete) information, replacement metavariables on variables or formulas of initial calculus.

Let's stop in more detail on the second possibility (in [2] is realized the first mode - by a proof the metatheorem of deduction). For it we enter dummy metavariables, which substitute separate variables (or subformulas) in following way: each equivalent variable (subformula) are substituted with the same dummy metavariable. The analog of a rule of a substitution is aplicable to metavariables. This suggest the following proof-search tactics: for a derivation of a formula it is necessary to substitute this formula in a «tail» of base formula - any axiom or derivated formula by this time. Thus we the initial task is reducible to a solution of subtasks: to receive antecedents of the base formula, which then can sequentially be eliminated by means of modus pоnens.

We start the derivation р É р and use above tactics by selecting as the base formula an axiom <+103>. Then first metaformula is [p É [A É p]] É [[p É A] É [p É p]], where A - dummy metavariable. Let's formulate the task of searching: in order to receive a derivation р É р it is necessary to receive two formulas: the structure first of which has an aspect p É [A É p], and structure second - p É A. Let's remark, that the first of the indicated tasks is solved a trivial, as metaformula p É [A É p] on it’s structure equivalences variant of an axiom <+102>. For a solution of the second subtask, we shall replace dummy A - on metaformula B É p. Then the metaformula p É [B É p] can be converted into variant of an axiom <+102> by substitution the dummy B on variable q. Thus on a structure of the metavariable A is superimposed the restriction: A @ B É p, i.e. the dummy A substitutes on the formula q É p. Both subtasks are solved successfully. Thus the set of substitutions in an axiom <+103> is clear: variables s and q is substituted on p, and p - on q É p. In an outcome of such substitutions we receive the formula [p É [q É p] É p]] É [[p É [q É p] É [p É p]], and after two applications modus pоnens (rule <*100> in [1]) we obtain more short (only 6 step) and understandable (for student or computer) the derivation of the formula р É р.

References:

1.    Church A. Introduction to mathematical Logic. - Princepton, New Jersey, Princepton University Press, 1956. V.1. pp. 65-86.