[Axiomatisation of 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.
Nous examinons la notion de substitution de façon abstraite, sans la définir explicitement. Nous épinglons les traits essentiels de la substitution afin de définir un concept de structure substitutive, appelé logos. Nous formulons ensuite un théorème de complétude en vue de préciser et de justifier le sentiment que les propriétés de la substitution usuelle peuvent être dérivées uniquement des axiomes de logos.
Accepted:
Published online:
Marcel Crabbé 1
@article{CRMATH_2004__338_6_433_0, author = {Marcel Crabb\'e}, title = {Une axiomatisation de la substitution}, journal = {Comptes Rendus. Math\'ematique}, pages = {433--436}, publisher = {Elsevier}, volume = {338}, number = {6}, year = {2004}, doi = {10.1016/j.crma.2004.01.021}, language = {fr}, }
Marcel Crabbé. Une axiomatisation de la substitution. Comptes Rendus. Mathématique, Volume 338 (2004) no. 6, pp. 433-436. doi : 10.1016/j.crma.2004.01.021. https://comptes-rendus.academie-sciences.fr/mathematique/articles/10.1016/j.crma.2004.01.021/
[1] Explicit substitutions, J. Funct. Programming, Volume 1 (1991), pp. 375-416
[2] Prelogic of logoi, Studia Logica, Volume 35 (1976), pp. 219-226
Cited by Sources:
Comments - Policy