Une axiomatisation de la substitution

We investigate the notion of substitution in an abstract way, without defining it explicitly. We single out the essential features of the operation of performing a substitution in order to define a concept of substitutive structure. called logos. We then prove a completeness theorem making precise and justifying the intuition that formulas true for the usual substitution can be proved from the logos axioms only. (C) 2004 Academie des sciences. Publie par Elsevier SAS. Tous droits reserves.