Sequent | EPFL Graph Search

Are you an EPFL student looking for a semester project?

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

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.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (19)

Related courses (2)

Related lectures (9)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a progr

Judgment (mathematical logic)

In mathematical logic, a judgment (or judgement) or assertion is a statement or enunciation in a metalanguage. For example, typical judgments in first-order logic would be that a string is a well-formed formula, or that a proposition is true. Similarly, a judgment may assert the occurrence of a free variable in an expression of the object language, or the provability of a proposition. In general, a judgment may be any inductively definable assertion in the metatheory.

Proof calculus

In mathematical logic, a proof calculus or a proof system is built to prove statements. A proof system includes the components: Language: The set L of formulas admitted by the system, for example, propositional logic or first-order logic. Rules of inference: List of rules that can be employed to prove theorems from axioms and theorems. Axioms: Formulas in L assumed to be valid. All theorems are derived from axioms. Usually a given proof calculus encompasses more than a single particular formal system, since many proof calculi are under-determined and can be used for radically different logics.

Structural rule

In proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgment or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic. Logics that deny one or more of the structural rules are classified as substructural logics. Three common structural rules are: Weakening, where the hypotheses or conclusion of a sequent may be extended with additional members.

LISA proof assistant: Formalisation and Verification CS-550: Formal verification

Covers the LISA proof assistant's codebase organization, kernel package, FOL formalization, and proof package.

Sequent Calculus: Basics and Applications CS-550: Formal verification

Covers the basics and applications of Sequent Calculus in Logic and Proof Theory, including Cut Elimination and practical proof analysis.

Propositions as Types: Logic and Programming Correspondence CS-452: Foundations of software

Explores the relationship between logic proofs and programming evidence through the Curry-Howard Correspondence.