EPFL Logo
fr|en
Se Connecter
Concept

Théorème de compacité

Théorème de compacité — Wikipédia
Théorème de compacité — Wikipédia

vignette|420x420px|Si toute partie finie d'une théorie est satisfaisable (schématisée à gauche), alors la théorie est satisfaisable (schématisée à droite). En logique mathématique, un théorème de compacité énonce que si toute partie finie d'une théorie est satisfaisable alors la théorie elle-même est satisfaisable. Il existe des logiques où il y a un théorème de compacité comme le calcul propositionnel ou la logique du premier ordre (on parle de logiques compactes). Il existe aussi des logiques sans théorème de compacité. Commençons l'article par un exemple informel où il n'y a pas de théorème de compacité en considérant la théorie suivante :un jour, il ne pleuvra pas ; il pleut ; demain il pleut ; après-demain il pleut ; dans 3 jours il pleut ; dans 4 jours il pleut ;...La théorie n'est pas satisfaisable (toutes les phrases ne peuvent être vraies en même temps). Pourtant, toute partie finie est satisfaisable. En d'autres termes, la logique temporelle linéaire n'est pas compacte. En calcul propositionnel, une formule propositionnelle est dite satisfaisable si l'on peut assigner des valeurs de vérité (vrai ou faux) aux atomes constituant la formule de façon que celle-ci soit vrai. Par exemple, la formule "p et non q" est satisfaisable en mettant p à vrai et q à faux. Une telle assignation s'appelle une valuation. Par exemple, "p à vrai et q à faux" est une valuation. Ainsi, une formule est satisfaisable s'il existe une valuation qui la satisfait. Plus généralement une théorie propositionnelle est satisfaisable s'il existe une valuation qui satisfait chacune des formules de cette théorie. Le théorème de compacité s'énonce comme suit. La démonstration qui suit est donnée dans le cas où T est dénombrable (elle s'étend au cas général en utilisant le lemme de Zorn, plutôt que le lemme de König, ou l'axiome du choix dépendant). Soit T un ensemble infini dénombrable de formules propositionnelles et φ(0), φ(1)... une énumération des formules de T. Soit p(0), p(1)... une suite infinie dénombrable de variables propositionnelles avec lesquelles les formules de T sont construites.

Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Cours associés (3)
MATH-381: Mathematical logic
Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.
MATH-483: Gödel and recursivity
Gödel incompleteness theorems and mathematical foundations of computer science
MATH-318: Set theory
Set Theory as a foundational system for mathematics. ZF, ZFC and ZF with atoms. Relative consistency of the Axiom of Choice, the Continuum Hypothesis, the reals as a countable union of countable sets,
Publications associées (16)
Afficher plus
Concepts associés (19)
Ultrafilter on a set
In the mathematical field of set theory, an ultrafilter on a set is a maximal filter on the set In other words, it is a collection of subsets of that satisfies the definition of a filter on and that is maximal with respect to inclusion, in the sense that there does not exist a strictly larger collection of subsets of that is also a filter. (In the above, by definition a filter on a set does not contain the empty set.) Equivalently, an ultrafilter on the set can also be characterized as a filter on with the property that for every subset of either or its complement belongs to the ultrafilter.
Second-order logic
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence says that for every formula P, and every individual x, either Px is true or not(Px) is true (this is the law of excluded middle).
Ultrafiltre
vignette|Le diagramme de Hasse montre l'ensemble de tous les sous-ensembles de {1,2,3,4}, partiellement ordonnés par inclusion d'ensemble (⊆). L'ensemble supérieur ↑{1,4} est surligné en vert foncé, c'est un filtre. Cependant, ce n'est pas un ultrafiltre, car il peut toujours être étendu au filtre correctement plus grand ↑{1}, représenté en vert clair. Ce dernier ne peut pas être étendu à son tour à un filtre non trivialement plus grand, il s'agit donc d'un ultrafiltre.
Afficher plus

Copyright © 2025 EPFL, tous droits réservés

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.