nLab sequent

Sequent

Context

Deduction and Induction

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Sequent

Idea

In formal logic a sequent (Gentzen 35, Martin-Löf 83) or hypothetical judgement (Pfenning, Davies 00) is an expression in the metalanguage which is a string of symbols of the form

AntecedentSuccedent Antecedent \vdash Succedent

where

  1. AntecedentAntecedent are symbols indicating judgements called the antecedents or context,

  2. SuccedentSuccedent are symbols indicating judgements called the succedents or (if it is just a single judgement) the consequent

  3. the consequence sign or turnstile-symbol “\vdash” expresses that SuccedentSuccedent is a consequence of AntecedentAntecedent:

    AntecedentAntecedent yields SuccedentSuccedent.”

    or

    “With AntecedentAntecedent the SuccedentSuccedent can be proven.”

    or

    AntecedentAntecedent, con-sequent-ly SuccedentSuccedent.”

    Or similar.

Historically the “consequence” here was early on transmuted to “sequenz” (Gentzen) and then later to “sequent”. See the section History below.

In systems of formal logic such as natural deduction/type theory such sequents express rules for explicit symbol manipulation admitted in the system rather than formal implications within the system. The latter instead are expressed by terms of function type t:ϕψt : \phi \to \psi. But the term introduction rule for terms of function types say that given one, one is allowed to get the other.

Typically one allows a list of expressions on both sides of the turnstile-symbols as in

Antec 1,,Antec kSucc 1,,Succ l Antec_1, \cdots, Antec_k \vdash Succ_1, \cdot, Succ_l

often abbreviated as

AntecSucc \vec Antec \vdash \vec Succ

in which case on the left a conjunction of the antecedents and on the right a disjunction of succedents is understood, as in

“If Antec 1Antec_1 and Antec 2Antec_2… are given then one of Succ 1,,Succ lSucc_1, \cdots, Succ_l is a consequence”.

An intuitionistic sequent has at most one succedent, which is then called the consequent. Often “intuitionistic sequent” is used to mean one with exactly one succedent, although technically it would make more sense to call those minimal sequents.

Another variant is that in some frameworks the antecedent and succedent displayed are required to be propositions and the free variables of the context are instead displayed beneath the turnstile as in

ϕ(x)true xψ(x)true. \vec \phi(x)\, true \vdash_{\vec x} \vec \psi(x) \, true \,.

If the framework regards propositions as types then this is the same as writing

x.ϕ(x)ψ(x). \vec x. \vec \phi(x) \vdash \vec \psi(x) \,.

Finally one can of course consider sequences of sequents

(Γ 1Δ 1),,(Γ nΔ n) (\Gamma_1 \vdash \Delta_1), \cdots, (\Gamma_n \vdash \Delta_n)

and if these are read disjunctively it is like a higher-order sequent without antecedent and called a hypersequent.

Rules for formal manipulation of sequents are called sequent calculi or deduction calculi. See there for more details.

Definition

The precise nature of sequents has been formalized differently in different systems of formal logic. We discuss a few

Intuitionistic sequents

(…) (Martin-Löf) (…)

Gentzen’s sequents

(…) (Gentzen) (…)

Sequents in focalized calculi

(…) Simmons (…)

Semantics

We discuss aspects of the categorical semantics of sequents, hence their interpretation when the ambient formal logic is regarded as the internal language of a category.

In homotopy type theory

Under the categorical semantics of homotopy type theory sequents in the type theory pretty accurately correspond to morphisms in the (∞,1)-topos. We indicate how this works, first for type declarations, then for terms of dependent types.

Let H\mathbf{H} be an (∞,1)-topos. Write TypeHType \in \mathbf{H} for the internal universe of small objects of H\mathbf{H}, called the object classifier.

This is defined as the representing object for the core of the small codomain fibration, exhibited by an equivalence of ∞-groupoids

name:Core(H /X) smallH(X,Type). name : Core(\mathbf{H}_{/X})^{small} \stackrel{\simeq}{\to} \mathbf{H}(X,Type) \,.

This equivalence sends an XX-family (EX)H /X(E \to X) \in \mathbf{H}_{/X} to its “name”, denoted

XEType, X \stackrel{\vdash E}{\to} Type \,,

which is the morphism characterized by fitting into an ∞-pullback square of the form

E Type^ X E Type, \array{ E &\to& \widehat{Type} \\ \downarrow &\swArrow& \downarrow \\ X &\underset{\vdash E}{\to}& Type } \,,

If here we simply replace, notationally, the arrow “\to” by the turnstile “\vdash”, display a generic generalized element xx of XX and then write E(x)E(x) to highlight the dependence of the fibers of EE on xx in XX, then the symbols “XETypeX \stackrel{\vdash E}{\to} Type” become the sequent “x:XE(x):Typex : X \vdash E(x) : Type”. This sequent is the syntax of which the morphism is the categorical semantics.

Similarly, if Xt XEX \stackrel{t}{\to}_X E is a section of EE over XX, hence a generalized element in the slice (∞,1)-topos H /X\mathbf{H}_{/X}, then by replacing the arrow-symbol by a turnstile-symbol we get “x:Xt(x):E(x)x : X \vdash t(x) : E(x)”. This is the sequent for the term tt of the dependent type EE.

In summary we have under the relation between category theory and type theory the notational correspondence:

morphisms to sequents.

\,typesterms
∞-topos theoryXEType\;\;\;\;X \stackrel{\vdash \;\;\;\;E}{\to} \;\;\TypeXt XE\;\;\;\;X \stackrel{\vdash \;\;\;t}{\to} {}_X \;\;E
homotopy type theoryx:XE(x):Typex : X \vdash E(x) : Typex:Xt(x):E(x)x : X \vdash t(x) : E(x)

History

The notion of sequent was introduced in section 2.3 of (Gentzen 1935) (called Sequenz there). In (Martin-Löf 1984, pages 29-30) it says

The forms of hypothetical judgement [[ have ]] the form

A 1true,,A ntrueApropA_1 true, \cdots, A_n true \vdash A prop

which says that AA is a proposition under the assumptions that A 1,,A nA_1, \cdots, A_n are all true, and, on the other hand, the form

A 1true,,A ntrueAtrueA_1 true, \cdots, A_n true \vdash A true

which says that the proposition A is true under the assumptions that A 1,,A nA_1, \cdots, A_n are all true. Here I am using the vertical bar for the relation of logical consequence, that is, for what Gentzen expressed by means of the arrow \to in his sequence calculus, and for which the double arrow \Rightarrow is also a common notation. It is the relation of logical consequence, which must be carefully distinguished from implication. What stands to the left of the consequence sign, we call the hypotheses, in which case what follows the consequence sign is called the thesis, or we call the judgements that precede the consequence sign the antecedents and the judgement that follows after the consequence sign the consequent. This is the terminology which Gentzen took over from the scholastics, except that, for some reason, he changed consequent into succedent and consequence into sequence, Ger. Sequenz, usually improperly rendered by sequent in English.

\phantom{-}symbol\phantom{-}\phantom{-}in logic\phantom{-}
A\phantom{A}\inA\phantom{A}element relation
A\phantom{A}:\,:A\phantom{A}typing relation
A\phantom{A}==A\phantom{A}equality
A\phantom{A}\vdashA\phantom{A}A\phantom{A}entailment / sequentA\phantom{A}
A\phantom{A}\topA\phantom{A}A\phantom{A}true / topA\phantom{A}
A\phantom{A}\botA\phantom{A}A\phantom{A}false / bottomA\phantom{A}
A\phantom{A}\RightarrowA\phantom{A}implication
A\phantom{A}\LeftrightarrowA\phantom{A}logical equivalence
A\phantom{A}¬\notA\phantom{A}negation
A\phantom{A}\neqA\phantom{A}negation of equality / apartnessA\phantom{A}
A\phantom{A}\notinA\phantom{A}negation of element relation A\phantom{A}
A\phantom{A}¬¬\not \notA\phantom{A}negation of negationA\phantom{A}
A\phantom{A}\existsA\phantom{A}existential quantificationA\phantom{A}
A\phantom{A}\forallA\phantom{A}universal quantificationA\phantom{A}
A\phantom{A}\wedgeA\phantom{A}logical conjunction
A\phantom{A}\veeA\phantom{A}logical disjunction
symbolin type theory (propositions as types)
A\phantom{A}\toA\phantom{A}function type (implication)
A\phantom{A}×\timesA\phantom{A}product type (conjunction)
A\phantom{A}++A\phantom{A}sum type (disjunction)
A\phantom{A}00A\phantom{A}empty type (false)
A\phantom{A}11A\phantom{A}unit type (true)
A\phantom{A}==A\phantom{A}identity type (equality)
A\phantom{A}\simeqA\phantom{A}equivalence of types (logical equivalence)
A\phantom{A}\sumA\phantom{A}dependent sum type (existential quantifier)
A\phantom{A}\prodA\phantom{A}dependent product type (universal quantifier)
symbolin linear logic
A\phantom{A}\multimapA\phantom{A}A\phantom{A}linear implicationA\phantom{A}
A\phantom{A}\otimesA\phantom{A}A\phantom{A}multiplicative conjunctionA\phantom{A}
A\phantom{A}\oplusA\phantom{A}A\phantom{A}additive disjunctionA\phantom{A}
A\phantom{A}&\&A\phantom{A}A\phantom{A}additive conjunctionA\phantom{A}
A\phantom{A}\invampA\phantom{A}A\phantom{A}multiplicative disjunctionA\phantom{A}
A\phantom{A}!\;!A\phantom{A}A\phantom{A}exponential conjunctionA\phantom{A}

References

In section 2.3

  • Gerhard GentzenUntersuchungen über das logische Schließen I Mathematische Zeitschrift 39(1), Springer-Verlag 1935. <http://dx.doi.org/10.1007/BF01201353>.

what today is called a sequent is introduced under Sequenz (Ger: sequence), apparently derived from Konsequenz (Ger: consequence) and denoted by a single arrow “\to”.

In the lectures

  • Per Martin-Löf, On the meaning of logical constants and the justifications of the logical laws, leture series in Siena (1983) (web)

where the author provides a modern foundation for logic based on a clear separation of the notions of judgment and proposition (see at Martin-Löf dependent type theory) the author says (pages 29-30) that “the forms of hypothetical judgements that I shall need” are Gentzen‘s sequents without the symmetry between antecedent and succedent that Gentzen used.

Referring explicitly to these lectures, these are are then just called hypothetical judgements in section 3 of

  • Frank Pfenning, Rowan Davies, A judgemental reconstruction of modal logic (2000) (pdf)

In section D1.1 of

sequents are introduced in the context of a basic introduction to formal logic. There the the notation ϕ cψ\phi \vdash_{\vec c} \psi is used where ϕ\phi is required to be a proposition and the context variables x\vec x are typeset below the turnstile. From the categorical semantics in section D1.2 it is clear that in the sense of dependent type theory these variables are to stand to the left of the turnstile.

See also

Last revised on December 19, 2022 at 19:42:19. See the history of this page for a list of all contributions to it.