A new characterization of substitution, viz. as a universally conjunctive and universally disjunctive predicate transformer, is proposed. This characterization is also meaningful in point-free models for predicate calculus, and agrees with the classical definition of substitution whenever the latter is applicable.
['A. Bijlsma', 'Carel S. Scholten']
Point-free substitution