\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{sequent}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{deduction_and_induction}{}\paragraph*{{Deduction and Induction}}\label{deduction_and_induction}

[[!include deduction and induction - contents]]

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{sequent}{}\section*{{Sequent}}\label{sequent}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{intuitionistic_sequents}{Intuitionistic sequents}\dotfill \pageref*{intuitionistic_sequents} \linebreak
\noindent\hyperlink{gentzens_sequents}{Gentzen's sequents}\dotfill \pageref*{gentzens_sequents} \linebreak
\noindent\hyperlink{sequents_in_focalized_calculi}{Sequents in focalized calculi}\dotfill \pageref*{sequents_in_focalized_calculi} \linebreak
\noindent\hyperlink{semantics}{Semantics}\dotfill \pageref*{semantics} \linebreak
\noindent\hyperlink{in_homotopy_type_theory}{In homotopy type theory}\dotfill \pageref*{in_homotopy_type_theory} \linebreak
\noindent\hyperlink{History}{History}\dotfill \pageref*{History} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

In formal [[logic]] a \emph{sequent} (\hyperlink{Gentzen}{Gentzen 35}, \hyperlink{Martin-L&#246;f}{Martin-L\"o{}f 83}) or \emph{hypothetical judgement} (\href{Pfenning-Davies}{Pfenning, Davies 00}) is an expression in the [[metalanguage]] which is a string of symbols of the form

\begin{displaymath}
Antecedent \vdash Succedent
\end{displaymath}
where

\begin{enumerate}%
\item $Antecedent$ are symbols indicating [[judgements]] called the \emph{[[antecedents]]} or \emph{[[context]]},


\item $Succedent$ are symbols indicating [[judgements]] called the \emph{[[succedents]]} or (if it is just a single judgement) the \emph{[[consequent]]}


\item the \textbf{consequence sign} or \textbf{turnstile}-symbol ``$\vdash$'' expresses that $Succedent$ is a \emph{consequence} of $Antecedent$:

`` $Antecedent$ yields $Succedent$.''

or

``With $Antecedent$ the $Succedent$ can be [[proof|proven]].''

or

``$Antecedent$, con-sequent-ly $Succedent$.''

Or similar.



\end{enumerate}
Historically the ``consequence'' here was early on transmuted to ``sequenz'' (\hyperlink{Gentzen}{Gentzen}) and then later to ``sequent''. See the section \emph{\hyperlink{History}{History}} below.

In systems of [[formal logic]] such as [[natural deduction]]/[[type theory]] such sequents express rules for explicit \emph{symbol manipulation} admitted in the system rather than formal [[implications]] \emph{within} the system. The latter instead are expressed by [[terms]] of [[function type]] $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

\begin{displaymath}
Antec_1, \cdots, Antec_k \vdash Succ_1, \cdot, Succ_l
\end{displaymath}
often abbreviated as

\begin{displaymath}
\vec Antec \vdash \vec Succ
\end{displaymath}
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_1$ and $Antec_2$\ldots{} are given then one of $Succ_1, \cdots, Succ_l$ is a consequence''.

An \textbf{[[intuitionistic logic|intuitionistic]] sequent} has at most one succedent, which is then called the \textbf{[[consequent]]}. Often ``intuitionistic sequent'' is used to mean one with \emph{exactly} one succedent, although technically it would make more sense to call those [[minimal logic|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

\begin{displaymath}
\vec \phi(x)\, true \vdash_{\vec x} \vec \psi(x) \, true
  \,.
\end{displaymath}
If the framework regards [[propositions as types]] then this is the same as writing

\begin{displaymath}
\vec x. \vec \phi(x) \vdash \vec \psi(x)
  \,.
\end{displaymath}
Finally one can of course consider sequences of sequents

\begin{displaymath}
(\Gamma_1 \vdash \Delta_1), \cdots, (\Gamma_n \vdash \Delta_n)
\end{displaymath}
and if these are read [[disjunction|disjunctively]] it is like a higher-order sequent without [[antecedent]] and called a \textbf{hypersequent}.

Rules for formal manipulation of sequents are called \emph{[[sequent calculi]]} or \emph{[[deduction calculi]]}. See there for more details.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

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

\hypertarget{intuitionistic_sequents}{}\subsubsection*{{Intuitionistic sequents}}\label{intuitionistic_sequents}

(\ldots{}) (\hyperlink{Martin-L&#246;f}{Martin-L\"o{}f}) (\ldots{})

\hypertarget{gentzens_sequents}{}\subsubsection*{{Gentzen's sequents}}\label{gentzens_sequents}

(\ldots{}) (\hyperlink{Gentzen}{Gentzen}) (\ldots{})

\hypertarget{sequents_in_focalized_calculi}{}\subsubsection*{{Sequents in focalized calculi}}\label{sequents_in_focalized_calculi}

(\ldots{}) \hyperlink{Simmons}{Simmons} (\ldots{})

\hypertarget{semantics}{}\subsection*{{Semantics}}\label{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]].

\hypertarget{in_homotopy_type_theory}{}\subsubsection*{{In homotopy type theory}}\label{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 $\mathbf{H}$ be an [[(∞,1)-topos]]. Write $Type \in \mathbf{H}$ for the [[universe in a topos|internal universe]] of [[small objects]] of $\mathbf{H}$, called the \emph{[[object classifier]]}.

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

\begin{displaymath}
name
  :
  Core(\mathbf{H}_{/X})^{small} \stackrel{\simeq}{\to} \mathbf{H}(X,Type)
  \,.
\end{displaymath}
This equivalence sends an $X$-family $(E \to X) \in \mathbf{H}_{/X}$ to its ``name'', denoted

\begin{displaymath}
X \stackrel{\vdash E}{\to} Type
  \,,
\end{displaymath}
which is the morphism characterized by fitting into an [[(∞,1)-pullback|∞-pullback]] square of the form

\begin{displaymath}
\itexarray{
     E &\to& \widehat{Type}
     \\
     \downarrow &\swArrow& \downarrow
     \\
     X &\underset{\vdash E}{\to}& Type
  }
  \,,
\end{displaymath}
If here we simply replace, notationally, the arrow ``$\to$'' by the turnstile ``$\vdash$'', display a generic [[generalized element]] $x$ of $X$ and then write $E(x)$ to highlight the dependence of the [[fibers]] of $E$ on $x$ in $X$, then the symbols ``$X \stackrel{\vdash E}{\to} Type$'' become the sequent ``$x : X \vdash E(x) : Type$''. This sequent is the [[syntax]] of which the morphism is the [[categorical semantics]].

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

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

\textbf{morphisms to sequents.}

\begin{tabular}{l|l|l}
$\,$&[[types]]&[[terms]]\\
\hline 
[[(∞,1)-topos theory&∞-topos theory]]&$\;\;\;\;X \stackrel{\vdash \;\;\;\;E}{\to} \;\;\Type$\\
[[homotopy type theory]]&$x : X \vdash E(x) : Type$&$x : X \vdash t(x) : E(x)$\\
\end{tabular}

\hypertarget{History}{}\subsection*{{History}}\label{History}

The notion of sequent was introduced in section 2.3 of (\hyperlink{Gentzen}{Gentzen 1935}) (called \emph{Sequenz} there). In (\hyperlink{Martin-L&#246;f}{Martin-L\"o{}f 1984, pages 29-30}) it says

\begin{quote}%
The forms of hypothetical judgement $[$ have $]$ the form

$A_1 true, \cdots, A_n true \vdash A prop$

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

$A_1 true, \cdots, A_n true \vdash A true$

which says that the proposition A is true under the assumptions that $A_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 \textbf{judgements that precede the consequence sign} the antecedents and the \textbf{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.


\end{quote}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[sequent calculus]]


\item [[cut rule]]



\end{itemize}
[[!include logic symbols -- table]]

\hypertarget{references}{}\subsection*{{References}}\label{references}

In section 2.3

\begin{itemize}%
\item [[Gerhard Gentzen]] \emph{Untersuchungen \"u{}ber das logische Schlie\ss{}en I} \emph{Mathematische Zeitschrift} 39(1), Springer-Verlag 1935. $<$http://dx.doi.org/10.1007/BF01201353{\tt \symbol{62}}.

\end{itemize}
what today is called a \emph{sequent} is introduced under \emph{Sequenz} (Ger: \emph{sequence}), apparently derived from \emph{Konsequenz} (Ger: \emph{consequence}) and denoted by a single arrow ``$\to$''.

In the lectures

\begin{itemize}%
\item [[Per Martin-Löf]], \emph{On the meaning of logical constants and the justifications of the logical laws}, leture series in Siena (1983) (\href{http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf}{web})

\end{itemize}
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 \emph{hypothetical judgements} in section 3 of

\begin{itemize}%
\item [[Frank Pfenning]], Rowan Davies, \emph{A judgemental reconstruction of modal logic} (2000) (\href{http://www.cs.cmu.edu/~fp/papers/mscs00.pdf}{pdf})

\end{itemize}
In section D1.1 of

\begin{itemize}%
\item [[Peter Johnstone]], \emph{[[Sketches of an Elephant]]}

\end{itemize}
sequents are introduced in the context of a basic introduction to [[formal logic]]. There the the notation $\phi \vdash_{\vec c} \psi$ is used where $\phi$ is required to be a [[proposition]] and the [[context]] [[variables]] $\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

\begin{itemize}%
\item Robert J. Simmons, \emph{Structural focalization} (\href{http://arxiv.org/abs/1109.6273}{arXiv:1109.6273})

\end{itemize}
[[!redirects sequents]]

[[!redirects turnstile]]

[[!redirects hypothetical judgement]] [[!redirects hypothetical judgements]]



\end{document}