Logique
Une axiomatisation de la substitution
[Axiomatisation of substitution]
Comptes Rendus. Mathématique, Volume 338 (2004) no. 6, pp. 433-436.

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.

Received:
Accepted:
Published online:
DOI: 10.1016/j.crma.2004.01.021
Crabbé, Marcel 1

1 Université catholique de Louvain, ISP-Centre de Logique, place Mercier, 14, 1348 Louvain-la-Neuve, Belgique
@article{CRMATH_2004__338_6_433_0,
     author = {Crabb\'e, Marcel},
     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},
     url = {http://www.numdam.org/articles/10.1016/j.crma.2004.01.021/}
}
TY  - JOUR
AU  - Crabbé, Marcel
TI  - Une axiomatisation de la substitution
JO  - Comptes Rendus. Mathématique
PY  - 2004
SP  - 433
EP  - 436
VL  - 338
IS  - 6
PB  - Elsevier
UR  - http://www.numdam.org/articles/10.1016/j.crma.2004.01.021/
DO  - 10.1016/j.crma.2004.01.021
LA  - fr
ID  - CRMATH_2004__338_6_433_0
ER  - 
%0 Journal Article
%A Crabbé, Marcel
%T Une axiomatisation de la substitution
%J Comptes Rendus. Mathématique
%D 2004
%P 433-436
%V 338
%N 6
%I Elsevier
%U http://www.numdam.org/articles/10.1016/j.crma.2004.01.021/
%R 10.1016/j.crma.2004.01.021
%G fr
%F CRMATH_2004__338_6_433_0
Crabbé, Marcel. 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. http://www.numdam.org/articles/10.1016/j.crma.2004.01.021/

[1] Abadi, M.; Cardelli, L.; Curien, P.-L.; Lévy, J.-J. Explicit substitutions, J. Funct. Programming, Volume 1 (1991), pp. 375-416

[2] Crabbé, M. Prelogic of logoi, Studia Logica, Volume 35 (1976), pp. 219-226

Cited by Sources: