Point-free substitution
A. Bijlsma, Carel S. Schölten · TU/e Research Portal · 1994
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.