Algèbre de Lindenbaum-Tarski - Lindenbaum–Tarski algebra
En logique mathématique , l' algèbre de Lindenbaum-Tarski (ou algèbre de Lindenbaum ) d'une théorie logique T se compose des classes d'équivalence d' énoncés de la théorie (c'est-à-dire le quotient , sous la relation d'équivalence ~ définie telle que p ~ q exactement lorsque p et q sont prouvablement équivalents dans T ). C'est-à-dire que deux phrases sont équivalentes si la théorie T prouve que chacune implique l'autre. L'algèbre de Lindenbaum-Tarski est donc l' algèbre quotient obtenue en factorisant l'algèbre des formules par cette relation de congruence .
L'algèbre porte le nom des logiciens Adolf Lindenbaum et Alfred Tarski . Il a été introduit pour la première fois par Tarski en 1935 comme un dispositif pour établir une correspondance entre le calcul propositionnel classique et les algèbres booléennes . L'algèbre de Lindenbaum-Tarski est considérée comme l'origine de la logique algébrique moderne .
Opérations
Les opérations d'une algèbre de Lindenbaum-Tarski A sont héritées de celles de la théorie sous-jacente T . Celles-ci incluent généralement la conjonction et la disjonction , qui sont bien définies sur les classes d'équivalence. Lorsque la négation est également présente dans T , alors A est une algèbre booléenne , pourvu que la logique soit classique . Si la théorie T est constituée des tautologies propositionnelles , l'algèbre de Lindenbaum-Tarski est l' algèbre booléenne libre générée par les variables propositionnelles .
Algèbres apparentées
Les algèbres de Heyting et les algèbres intérieures sont les algèbres de Lindenbaum-Tarski pour la logique intuitionniste et la logique modale S4 , respectivement.
Une logique pour laquelle la méthode de Tarski est applicable, est dite algébrable . Il existe cependant un certain nombre de logiques où ce n'est pas le cas, par exemple les logiques modales S1 , S2 , ou S3 , qui manquent de la règle de nécessité (⊢φ impliquant so), donc ~ (défini ci-dessus) n'est pas un congruence (car ⊢φ→ψ n'implique pas ⊢□φ→□ψ). Un autre type de logique où la méthode de Tarski est inapplicable est la logique de pertinence , car étant donné deux théorèmes, une implication de l'un à l'autre peut ne pas être elle-même un théorème dans une logique de pertinence. L'étude du processus (et de la notion) d'algébrisation comme sujet d'intérêt en soi, pas nécessairement par la méthode de Tarski, a conduit au développement de la logique algébrique abstraite .
Voir également
Les références
- Hinman, P. (2005). Fondements de la logique mathématique . AK Peters. ISBN 1-56881-262-0.