Abstract

In this paper we consider two rules of substitution for predicate symbols as introduced by Church, Introduction to mathematical logic, Princeton 1956, and by Pogorzelski, Prucnal, Structural completness of the first-order predicate calculus, Bulletin de l' Academie Polonaise des Sciences, serie des sci. math., ast. at phys., vol XXII, No.3, 215-217. We show that the rules are not equivalent over a standard system of predicate logic.