ABSTRACT
Explanation, D 95-98: Defined 33; 33; pr; fU. In contradistinc tion to the auxiliary terms which were defined at an earlier stage, the terms defined here refer to based TNsymbols only.
§ 2 3 . R u le s o f T r a n s f o r m a t io n *
The following definitions constitute the formalization of the previously stated transformation-rules of Language I (§11 and § 12). For this purpose substitution must first be defined (D 102); D 99-101 introduce auxiliary terms for the definition of sub stitution. D 99. 1. stfrei (0, s, x) = (K/z) lng (#) [Frei (s> x> n) • ~ (3 m) lng (#)
(Gr (;m, n) • Frei (s, x, m))] 2. stfrei (U,s,x) — (Kw) stfrei (k, s, x) [^ (n = stfrei (k, s, x))•
Frei (5, x, n) • ~ (3 m) stfrei (k, s, x) [m = stfrei (ky sy #)] • Gr (m, n) • Frei (s> xy w))]
D i 00. anzfrei (s, x) = (Kn) lng (x) (stfrei (n,s>x) = 0 ) D 101. 1. sb (0, Xy s, y) = x
2. sb (k[, Xy s,y) = ers (sb (kf xf sfy)f stfrei (kf st x),y)
Explanation, D 99-101: Let 5 be tn 3i. stfrei (k, s, x) is the positionnumber of the (k+ i)th 3X (counted from the end of the expression x) which occurs freely in x (0 in the case where there are not k + 1 free 3X in x). anzfrei (sy x) is the number of the 3X which occur freely
* Key to the symbols: stfrei: position-number of free 3
(Stellennummer des freien 3) anzfrei: number of free 3 (An-
zahlfreier 3) sb, subst: substitution (Substitu
tion) G rS : primitive sentence (Grund-
satz) AErs: expression-replacement
(Ausdrucksersetzung)
KV: no free variable (keinefreie Variable)
UAblb: directly derivable (unmittelbar ableitbar)
Abl: derivation (Ableitung) Ablb: derivable (ableitbar) Bew: proof (Beweis) Bewb: demonstrable (beweisbar)
in x, sb (k,x,s,y) is that expression which results from the expres sion x when, starting with the last free fo, the k last free fa of x are successively replaced by the expression y.