Ê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.
Concept
Sequent
Résumé
In mathematical logic, a sequent is a very general kind of conditional assertion.
A sequent may have any number m of condition formulas Ai (called "antecedents") and any number n of asserted formulas Bj (called "succedents" or "consequents"). A sequent is understood to mean that if all of the antecedent conditions are true, then at least one of the consequent formulas is true. This style of conditional assertion is almost always associated with the conceptual framework of sequent calculus.
Sequents are best understood in the context of the following three kinds of logical judgments:
Unconditional assertion. No antecedent formulas.
Example: ⊢ B
Meaning: B is true.
Conditional assertion. Any number of antecedent formulas.
Simple conditional assertion. Single consequent formula.
Example: A1, A2, A3 ⊢ B
Meaning: IF A1 AND A2 AND A3 are true, THEN B is true.
Sequent. Any number of consequent formulas.
Example: A1, A2, A3 ⊢ B1, B2, B3, B4
Meaning: IF A1 AND A2 AND A3 are true, THEN B1 OR B2 OR B3 OR B4 is true.
Thus sequents are a generalization of simple conditional assertions, which are a generalization of unconditional assertions.
The word "OR" here is the inclusive OR. The motivation for disjunctive semantics on the right side of a sequent comes from three main benefits.
The symmetry of the classical inference rules for sequents with such semantics.
The ease and simplicity of converting such classical rules to intuitionistic rules.
The ability to prove completeness for predicate calculus when it is expressed in this way.
All three of these benefits were identified in the founding paper by .
Not all authors have adhered to Gentzen's original meaning for the word "sequent". For example, used the word "sequent" strictly for simple conditional assertions with one and only one consequent formula. The same single-consequent definition for a sequent is given by .
In a general sequent of the form
both Γ and Σ are sequences of logical formulas, not sets. Therefore both the number and order of occurrences of formulas are significant.
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.