A substitution free axiom set for second order logic.
Nino B. Cocchiarella · Notre Dame Journal of Formal Logic · 1969
NINO B. COCCHIARELLA (properly) substituting ζ for a in φ, with that formula ψ which is obtained from φ by proper substitution of ζ for a if there exists such a formula ψ; Γal and otherwise φ is to be φ.If there is a formula ψ which is obtained from φ by proper substitution of ζ for a, we say that ζ can be properly substituted for a in φ.Where n is a natural number, a 0 , . . ., a n ^1} β 0 , . . ., ft,-! are pairwise distinct individual variables, φ is a formula, ζ 0 , . . ., ζVi are terms, β 0 , . . ., β n _! are the first n individual variables which do not occur in φ, ζ 0 , ., ζ»-i, we define the result of the simultaneous proper substitution of ζ 0 , . . ., ζVi for α? 0 , . . ., #"_!, respectively, in φ, in