Abstract FR:

Les regles qui n'engendrent pas de nouvelles formules prouvables dans une logique, sont dites regles admissibles de cette logique. En calcul propositionnel classique, toutes ces regles sont derivables, c'est-a-dire demontables de facon interne, ce qui n'est pas le cas en logique intuitionniste. Cette these veut eclaircir les liens entre admissibilite et derivabilite en calcul propositionnel intuitionniste. La premiere partie donne des conditions simples pour que ces deux notions soient identiques. On utilise une sorte particuliere de substitutions, dont on montrera dans la deuxieme partie qu'elles permettent de caracteriser l'admissibilite. La deuxieme partie utilise la classe de substitutions mentionnee precedemment et des cas particuliers tres simples des resultats montres en premiere partie, pour obtenir une caracterisation de l'admissibilite par la retro-derivation en calcul des sequents. C'est le resultat central de la these. On obtient ainsi certains resultats de decidabilite, en particulier la decidabilite de l'admissibilite, ainsi que d'autres caracterisations. La troisieme partie illustre le resultat precedent et en donne des applications. On decrit completement le cas a une variable. On donne ensuite une axiomatisation denombrable de l'admissibilite, et l'on en deduit l'impossibilite d'une axiomatisation finie