10 S. C.KLEENE
%••• 9^9 ^19•
^th-
£ °9 and showing theproper index £ « ®f£ 9 we
infer "(O^'Xa^,..?,^, ^,...,2^)^ if from "[^(^•••^^•••^^i) - H"
where u 0 and "KO^Tta^a^,...,^,oC1,...,oi%) ^w». Representingthe
statements byquadruple numbers,the"~bottom part ofthe tree (consistingof
the bottom vertex occupied bythe conclusion oftheinference, and two
vertices immediately over that occupied bythe premises) appears asfollows,
with k 0, forsome number u 0:
^^Sj^L* %9l9\9 *k^M2 09^ 9 ^9^19^2' * 9S^ 9L^1» * * * ^JT*^
«0,^,^,a1,...
9
^$Jj^9... #b^,w.
Similarly, ifthefinal inference isanapplication of (S5a),
£mss5$j&}£
and the bottom ofthetree (consisting ofthe bottom vertex occupied by the
conclusion, andone vertex immediately over that occupied bythe premise)
appears asfollows,with k 0:
g,qc-l,a2, .., ,^c,/,b1,.•.,bj,w
«5s^]39^0,a2,... ,ak,/,b1,...,b^,w#
As a third example, suppose thefinal (and only) step isanapplication
of (S7).Then f = 7 and the bottom (andwhole) ofthe tree appearsas
follows, where k 0, t 0, and (b-)Q 0 (sothat (b, ) "1isthe value,for
a..asargument, ofa function ot- such that b-l#,):
«7,k,a1,...
9
§t^f£p\, •.. ,bj, (feL)a~1.
Of course, these examples apply just aswell toanyother inferencein
the tree (instead ofthe final inference), reinterpreting thenotation tomake
^9^9±\9**°9$^9 Jb)h***)L$ 9?P the conclusion of that inference.
Let usreconsider the role ofthenumber £, assumed thus fartobea
proper index, inthe inferences. Fortheexample of (SOb), all that isreally
necessary isthat £ be ofthe form 0,g for some number g. That £ be a proper
index, sothat f will beone, isunnecessary, andwecanspare ourselves work
by not requiring that tobechecked aspart oftheinference inquestion.
Whatever effect £ exerts onthe computation will bethrough higher inferences
leading tothe two premises ofthis inference. Similarly, fortheexampleof
(S5a), itisonly necessary that f beofthe form 5,g,h g andh need notbe
proper indices.
Previous Page Next Page