Saturation and Extraction

Abstract

The language LPT1 contains also the dyadic saturation functor “(t,t′)”. For all singular terms (names, variables, functional expressions) t and t′ of LPT1, “(t,t′)” is to be read as “the saturation of t by t′”. (Let the word “saturation” connote in this context not the process of saturation, but its result. The same remark applies to the less suggestive word that could here be used instead of “saturation”: “concatenation”: “the concatenation of t with t′.” It is less suggestive because it does not by itself connote an asymmetry between concatenated entities, whereas there are standard applications of the intended functional concept for which commutativity fails.) Note that the saturation functor of LPT1 cannot be defined by the ordered-pair-functor: sometimes the saturation of x by y is identical with the saturation of x by z, although y and z are non-identical.