Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Catégorie
Logique infinitaire
Résumé
Une logique infinitaire est une logique qui permet des formules infiniment longues ou des démonstrations infiniment longues. Certaines logiques infinitaires peuvent avoir des propriétés différentes de celles de la logique de premier ordre standard. En particulier, les logiques infinitaires peuvent ne pas être compactes ou complètes. Les notions de compacité et de complétude qui sont équivalentes en logique finitaire ne le sont pas forcément dans les logiques infinitaires. Par conséquent, pour les logiques infinitaires, des notions de forte compacité et complétude sont définies. Cet article aborde les logiques infinitaires présentées dans les systèmes à la Hilbert, car elles ont été largement étudiées et constituent les extensions les plus simples de la logique finitaire. Ce ne sont cependant pas les seules logiques infinitaires qui ont été formulées ou étudiées.
Comme nous présentons un langage avec des formules infiniment longues, il n'est pas possible d'écrire explicitement ces formules. Pour contourner ce problème, un certain nombre de commodités de notation, qui, à proprement parler, ne font pas partie du langage formel, sont utilisées. « » est utilisé pour souligner une expression infiniment longue. Dans le cas où cette notation n'est pas claire, la longueur de la séquence est notée plus tard. Lorsque cette notation devient ambiguë ou confuse, des suffixes tels que sont utilisés pour indiquer une disjonction infinie sur un ensemble de formules de cardinalité . La même notation peut être appliquée aux quantificateurs, par exemple . Cela est censé représenter une suite infinie de quantificateurs pour chaque où .
Les suffixes et les « » ne font pas partie de l'alphabet formel des langages infinitaires.
L'axiome du choix est supposé vrai, de façon à avoir des
Une logique infinitaire de premier-ordre Lα,β, α régulier, β = 0 ou ω ≤ β ≤ α, a le même ensemble de symboles qu'une logique finitaire et peut utiliser toutes les règles pour la formation de formules d'une logique finitaire ainsi que les suivantes :
Étant donné un ensemble de formules alors et sont des formules.
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.