On characterizations of the first-order functional calculus
Juliusz Reichbach · Notre Dame Journal of Formal Logic · 1961
In papers [5] and [7] I have presented some characterizations of theses of the first-order functional calculus; in this paper I give a generalization of two characterizations of one.We consider the first-order functional calculus with the symbolism described in [4] and besides signs accepted in the logic literature we use the following ones: (0,1) E, F, G, Ep Fp Gj . . .-variables representing expressions, (0 7 2) Sw {E\ -the set of all symbols occurring in the expression E, (0 9 3) Skt -the set of all formulas 3 of the form Σfi^ . . .Σ^ H^z +ί Πβi F, where F is a quantifierless expression containing no free variables and Πtf is the sign of the universal quantifier binding the apparent variable a-, and Σtf G = (Ha.G 9 ) 9 , for 7 = 1, . . ., k. (0,4) C(E) -the set of all significant parts of the formula E: F ε C(E) = • F = E or there exist such G, H that: (F = G) Λ (E = G 9 ) v [(F = G) v (F = //)] Λ (E = G + H) v (3z) {F = G( Xi /a)\ Λ (F = ίlaG).5 (0,5) w(E) -the number of different free variables occurring in the expression E, (0,6) p(E) -the number of different apparent variables occurring in the expression E, (0J) i ly . . ., i w{E γ or j v . . ., j w(E) or Z r . . ., l^( E) -different indices of these and only these free variables which occur in the expression E, (0,8) i(E)^max{i 1 , . . ., i w(E) \ , (0,9) m(E) = w(E)+:p(E), (0,10) n(E) = max{m(E),i(E)\ , (0,11) E(x/y) -the expression resulting from E by the substitution of x for each occurrence of y in E; if y is an apparent variable, then y does not belong in E to the scope of the quantifier Πy; if x is an apparent variable, then y does not belong to the scope of the quantifier ΐίx, (0,12) Σ(F) = 0, if F is a quantifierless formula; X(F + G) = max \1(F), Σ(G)} ; Σ(ΠtfF) = ϊ\F(x/a)}, where xT^E}; Σ(Σ*F) = w(F) +1, if Σ{F(x/α)} = 0; 6 Σ(ΣtfF) = Σ{F(x/a)|, if ^T^(F) andΣ{F(x/a)} =;/0;