# Theory MultiSequents

section "Multisuccedent Sequents"
theory MultiSequents
imports "HOL-Library.Multiset"
begin
text‹
\section{Introduction}
In this paper, we give an overview of some results about invertibility in sequent calculi. The framework is outlined in \S\ref{isadefs}. The results are mainly concerned with multisuccedent calculi that have a single principal formula. We will use, as our running example throughout, the calculus \textbf{G3cp}. In \S\ref{isasingle}, we look at the formalisation of single-succedent calculi; in \S\ref{isafirstorder}, the formalisation in \textit{Nominal Isabelle} for first-order calculi is shown; in \S\ref{isamodal} the results for modal logic are examined. We return to multisuccedent calculi in \S\ref{isaSRC} to look at manipulating rule sets.
\section{Formalising the Framework \label{isadefs}}
\subsection{Formulae and Sequents \label{isaformulae}}
A \textit{formula} is either a propositional variable, the constant $\bot$, or a connective applied to a list of formulae. We thus have a type variable indexing formulae, where the type variable will be a set of connectives. In the usual way, we index propositional variables by use of natural numbers. So, formulae are given by the datatype:
›