A Proof Description Language and Its Reduction System

The normalization of a natural deduction proof of a closed existential formulagives a term t and a proof of A x [t~], This allows us to regard a proof as a program(Goad [9] [10] etc.). But it is not always necessary to completely normalize the givenproof to obtain t. We analyze the situation by introducing the notions called minimalI-reduct, proper reduction etc.; in a word, we define the normal order of proof reductionand study its proof-theoretical property. Then, we present an experimental proof-checker-reducer system that actually uses those principles. In designing a proof-checker(or rather a proof description language), we focussed our attention on the readability ofproofs. § 1. IntroductionA theory in which if a closed existential formula BxA is provable, thenA X \T\ is also provable for some closed term t is said to have ED (explicitdefinability property). So called constructive theories have ED, while classicalones do not have ED in general; e.g. Peano's arithmetic (PA) does not haveED (cf. Godel's Incompleteness Theorem).We take Heyting's arithmetic (HA) as a typical case of constructive theories.There are several methods of extracting the term t from the proof of 3xA:© recursive readability (Kleene [15] [16], Nelson [21])© modified readability (Kreisel [17])© normalization (Prawitz [22] [23])® cut elimination (Gentzen [8])© Dialectica interpretation (Godel [11]).The stability of the E-theorems (i.e. the above methods all compute the same tfor 3xA) is discussed in Mints [20], Diller [6].Among the methods above, Prawitz' normalization of the natural deductionis the most fundamental and the simplest; it is also easily implementable on a