View source for Natural logical deduction

{{TEX|done}}
A formal deduction approximating as closely as possible the essence of the reasoning usual in mathematics and logic. Criteria for the naturalness and quality of a deduction cannot be specified with complete precision, but they usually concern deductions that can be carried out by the generally accepted rules of logical transformations, that are compact (in particular, do not contain superfluous applications of deduction rules), that are  "glued together"  (corresponding part of deductions must be eliminated, for example by extracting auxiliary lemmas), etc.

Originally, formalizations of mathematical and logical theories did not aim at naturalness (see [[Logical calculus|Logical calculus]]); a decisive advance in this direction was made by the calculus of natural deduction (see [[Gentzen formal system|Gentzen formal system]]), which imitates the form of conventional mathematical argument and allows one to introduce and use assumptions in the usual way. Other quite natural methods are those for handling assumptions in sequent calculi, which have additional advantages — the [[Subformulation property|subformulation property]] — and so form a basis for further advances in the problem of constructing natural logical deductions.

For automating the search for natural logical deductions auxiliary sequent calculi have been proposed [[#References|[2]]] that possess the subformulation property but do not allow the transfer of assumptions to the succedent (see [[Sequent (in logic)|Sequent (in logic)]]). It is easier to construct natural logical deductions in terms of deductions in such a calculus. On this basis a method has been developed for the search for natural deductions, taking account of  "likenesses"  (that is, of equal subformulas in the structure of the formulas being tested) for shortening the deductions and  "gluing"  them together,  "weeding out"  superfluous formulas and applications of rules, the possibility of varying the tactics in establishing deducibility, etc. Within the bounds of the logical means of classical [[Propositional calculus|propositional calculus]] these methods have led to a computer algorithm; the program finds a natural logical deduction for a given assertion from a given list of hypotheses, and records this deduction as a logico-mathematical text in Russian. Problems related to the search for natural logical deductions are those of correction of hypotheses and strengthening of theorems; these concern methods enabling small corrections to be made in a given formula so that it becomes a theorem or is changed into a stronger theorem, and investigations into criteria for the quality of such corrections.

Developments in the field of natural logical deductions have been mainly concerned with classical logics, but the resulting methods have a more general character.

====References====
<table>
<TR><TD valign="top">[1]</TD> <TD valign="top"> , ''Mathematical theory of logical deduction'' , Moscow  (1967)  (In Russian; translated from English)  (Collection of translations)</TD></TR>
<TR><TD valign="top">[2]</TD> <TD valign="top">  N.A. Shanin,   et al.,   "An algorithm for computer search for a natural logical deduction in propositional calculus" , Moscow-Leningrad  (1965)  (In Russian)</TD></TR>
<TR><TD valign="top">[3]</TD> <TD valign="top">  D. Prawitz,   "Natural deduction" , Almqvist &amp; Wiksell  (1965)</TD></TR>
</table>



====Comments====
Cf. also [[Derivation, logical|Derivation, logical]].

====References====
<table>
<TR><TD valign="top">[a1]</TD> <TD valign="top">  K. Schutte,   "Proof theory" , Springer  (1977)</TD></TR>
<TR><TD valign="top">[a2]</TD> <TD valign="top">  G. Gentzen,   M. Szabo (ed.) , ''Collected papers'' , North-Holland  (1969)</TD></TR>
</table>

[[Category:Logic and foundations]]