S.L. Katrechko
FREGE'S SYSTEM AND PROOF-SEARCH THEORY
Logic is interested, first of all, in studying the question "what is
a proof ?". It is important that in any proof system the truth of premises
guarantees the truth of conclusion. The first system of this kind was built by
G. Frege in 1879. Later Hilbert type systems was built on the basis of
Frege's system.
But logic isn't interested in the question "how is it possible to
build a proof ?". This task is considered in the proof-search theory which
deals with the heuristic component of proof systems. On the one hand, the
emergence and development of the proof-search theory is connected with the
emregence of more manageable systems for the proof-search: natural deduction
systems and Gentzen type systems, in which the proof building is possible by
means of the analytic method "subgoal reduction" (backwards proof).
The method leads to a modification of the concept of derivation. Instead of the
concept of linear derivation as sequence of formulas in Hilbert type systems
the concept of structural derivation is introduced in these systems: the
concept of sybordinate derivation in natural deduction systems and derivation
tree in Gentzen type systems. Structural modification of the concept of
derivation develops the heuristic component of proof systems, because a number
of possible derivations of a formula decreases. On the other hand, further
development the proof-search theory was connected with attemps to eliminate all
non-analytic rules of inference (so-called cut-type rules) from proof systems
and to build mechanizable systems of inference (systems of automated
theorem-proving). But in the theory of complexity [1] researchers have come at
some essential limitations of the purely analitic approach towards proof building.
In [2] some limitation results have been proved:
·
all Hilbert
type systems, natural deduction systems and Gentzen type systems with cut
polinominally simulate each other.
·
proof
systems with the non-analytic substitution rule are more "powerful"
then proof systems without such rules.
These results of the proof-search theory (heuristic significance of
structural derivation and "power" of substitution rule) emphasize the
importance of Frege's system in the further development of the proof-search
theory, because this system contains substitution rule and the deduction of the
system is represented as a two-dimensial (structural) derivation.
REFERENCES: