algèbre de Lindenbaum

L'algèbre de Lindenbaum d'une théorie mathématique est l'ensemble des énoncés du langage de celle-ci modulo la relation d'équivalence suivante: deux énoncés A et B sont dans la même classe d'équivalence s'il est possible de démontrer dans la théorie que A a pour conséquence B et que B a pour conséquence A. La relation de conséquence logique sur les énoncés, qui est compatible avec la relation d'équivalence, induit par quotient une relation d'ordre sur l'algèbre de Lindenbaum. Lorsque la théorie est celle du calcul propositionnel en logique classique, l'algèbre de Lindenbaum, munie des conjonction, disjonction et négation (qui sont compatibles avec l'équivalence) forme une algèbre de Boole. Cette algèbre, parfois appelée également algèbre de Lindenbaum-Tarski, a été introduite par Adolf Lindenbaum et Alfred Tarski en 1935.