ABSTRACT
In Chapter 1.5 I discussed how to code, or arithm etize, formulas by num bers, and it is not hard to see that such arithm etization can be carried out also for sequences and sequents of formulas as well as for trees and for derivations of K tP and KUP ; an example for the arithmetization of another calculus can be found in FELSCHER 93 . If D is a derivation, then rD n shall be its code, and the same notation shall be used for the formation of codes of other objects. Since the basic coding and decoding functions are elementa ry recursive functions, I can define elementary functions all of which will have the value 0 unless the following circumstances h o ld :
SEQ(x) = 1 if x - r s 1 for a sequent s MEM(x,k) = y + 1 if SEQ(x)= 1 and y = rv 1 is the k -th member of that sequent DEDU(x) = 1 if x = r D 1 for a derivation D CDEDU(x) = 1 if x = rD 1 for a cutfree derivation D ,
w?M = 4 v v ,P = 4 p v , Q =4 q
'Ow , M ? Q =4 q
LE(x) = n + 1 if x = r D 1 and n is the length of D , LE0(x) = n + 1 if x = rD n and n is the length of the tree underlying D , CDEG(x) = n + 1 if x = rD n and n is the cut degree of D ENDS(x) = y if x = rD n and y is code of the endsequent of D , RULE(x) = r if x = r D 1 and r is (a number for) the last rule applied in D , BRA^x) = y if x = r D 1 and LE(x) > 1 and y is code of the subderivation of
the left or the only prem iss of D ;s endsequent BRAr(x) = y analogously in case there is a second right premiss JOIN^XjZ,r) — u if u = rD \ x = BRA^u), z = ENDS(x), RULE(u) = r and this is
a 1 -p rem iss rule J0IN2(x ,y ,z,r) = u if u = r D 1, x = BRA^u), y = BRAr(u), z = ENDS(x), RULE(u) =
r and this is a 2-prem iss rule.
