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.