|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
the consequence sign or turnstile-symbol “” expresses that is a consequence of :
“ yields .”
“With the can be proven.”
“, con-sequent-ly .”
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 . 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
often abbreviated as
“If and … are given then one of 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
If the framework regards propositions as types then this is the same as writing
Finally one can of course consider sequences of sequents
The precise nature of sequents has been formalized differently in different systems of formal logic. We discuss a few
(…) (Martin-Löf) (…)
(…) (Gentzen) (…)
(…) Simmons (…)
Under the categorical semantics of homotopy type theory sequents in the type theory pretty accurately corrsepond to morphisms in the (∞,1)-topos. We indicate how this works, first for type declarations, then for terms of dependent types?.
This equivalence sends an -family to its “name”, denoted
which is the morphism characterized by fitting into an ∞-pullback square of the form
If here we simply replace, notationally, the arrow “” by the turnstile “”, display a generic generalized element of and then write to highlight the dependence of the fibers of on in , then the symbols “” become the sequent “”. This sequent is the syntax of which the morphism is the categorical semantics.
Similarly, if is a section of over , hence a generalized element in the slice (∞,1)-topos , then by replacing the arrow-symbol by a turnstile-symbol we get “”. This is the sequent for the term of the dependent type .
In summary we have under the relation between category theory and type theory the notational correspondence:
morphisms to sequents.
|homotopy type theory|
The forms of hypothetical judgement have the form
which says that is a proposition under the assumptions that are all true, and, on the other hand, the form
which says that the proposition A is true under the assumptions that 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 in his sequence calculus, and for which the double arrow 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.
In section 2.3
what today is called a sequent is introduced under Sequenz (Ger: sequence), apparently derived from Konsequenz (Ger: consequence) and denoted by a single arrow “”.
In the lectures
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
In section D1.1 of
sequents are introduced in the context of a basic introduction to formal logic. There the the notation is used where is required to be a proposition and the context variables 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.