\documentstyle[url]{llncs}

\everymath{\rm}
\everydisplay{\rm}
\input{lgwinclude}

% Save current \parindent (used by e.g. pyk display ... end display)
\newlength{\docparindent}
\setlength{\docparindent}{\parindent}

\newcommand{\liberalUrlBreak}[1]{{%
\mathcode`\/="262F%
\mathcode`\0="2630%
\mathcode`\1="2631%
\mathcode`\2="2632%
\mathcode`\3="2633%
\mathcode`\4="2634%
\mathcode`\5="2635%
\mathcode`\6="2636%
\mathcode`\7="2637%
\mathcode`\8="2638%
\mathcode`\9="2639%
\mathcode`\:="263A%
\mathcode`\A="2641%
\mathcode`\B="2642%
\mathcode`\C="2643%
\mathcode`\D="2644%
\mathcode`\E="2645%
\mathcode`\F="2646%
%\thinmuskip=0mu%
\medmuskip=0mu plus 2mu minus 0mu%
%\thickmuskip=0mu%
%\def\thinspace{\kern 0em}%
$#1$}}

\let\oldmathbf=\mathbf
\renewcommand{\mathbf}[1]{{\oldmathbf #1}}
\let\oldmathit=\mathit
\renewcommand{\mathit}[1]{{\oldmathit #1}}
\let\oldmathsf=\mathsf
\renewcommand{\mathsf}[1]{{\oldmathsf #1}}

\begin {document}
\title {The Logiweb sequent calculus}
\author {Klaus Grue\inst{1}}
\institute {Department of Computer Science, University of Copenhagen (DIKU)}
\date {\today}
\maketitle


\raggedright



\begin{abstract}
The `Logiweb sequent calculus' is suited for terse, human readable formulation of axioms, inference rules, theories, lemmas, and proofs. It supports different styles of theories like equational theories and FOL based theories. It permits to express arbitrary side conditions in the `Logiweb programming language'. As an example of use, the calculus allows to express the deduction rule as an inference rule which makes it easy to get started using a theory. The calculus has operations for `dereferencing' and `referencing' which allow to convert e.g.\ the name of a lemma into the contents of the lemma and vice versa. The calculus interacts smoothly with fully automatic tactics as well as proofs in which part of the work is done by a human author and part is done by proof tactics.
\end{abstract}



\section{Introduction}\label{sec:Introduction}

Logiweb \cite{grue04,grue05,base} is a system for electronic publication of logic. It allows authors different places in the world to define theories, state and prove lemmas, and to publish {\em Logiweb pages} that contain the results. The present paper is an example of a Logiweb page, and the present paper is correct in the sense that it has been verified by Logiweb.

Core Logiweb allows users to program proof systems in the {\em Logiweb programming language} and to publish the proof system. Users who use the same proof system and the same axiomatic theory may benefit from the results of each other in that a proof written by one author may make references across the internet to lemmas proved by another author. Cross theory cooperation (e.g.\ use of ZFC results in NBG) could be more cumbersome and cross proof system cooperation even more so, depending on the theories and systems involved.

The present paper introduces {\em Logiweb sequent calculus} which allows users to express arbitrary axiomatic theories on the same footing. That  calculus supports arbitrary styles of logic (e.g.\ FOL or equational) equally well. The calculus is machine friendly in that proofs are easy to generate, verify, store, and transmit and it is general so that users of Logiweb are not tempted to make a proof system each. User friendliness in the sense that theories, lemmas, and proofs should be easy to read and write is taken care of by Logiwebs rendering and Turing complete macro expansion facilities combined with the support for proof tactics in the implementation of the calculus in \cite{base}.

The present paper gives an overview. Details are in a web appendix \cite{appendix}.



\section{Logiweb sequent calculus}

Let $\underline{
\mathsf {v}}$ and $\underline{
\mathsf {t}}$ denote the syntax classes of metavariables and object terms, respectively. The format $\underline{
\mathsf {s}}$ of Logiweb statements is $\underline{
\mathsf {s}}::=\underline{
\mathsf {v}}
\mathrel{|} \underline{
\mathsf {t}}
\mathrel{|} \underline{
\mathsf {s}}
\vdash \underline{
\mathsf {s}}
\mathrel{|} \underline{
\mathsf {t}}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {s}}
\mathrel{|} 
\forall \underline{
\mathsf {v}}
\colon \underline{
\mathsf {s}}
\mathrel{|} 
{\makebox [0mm][l]{$\bot $}\,{\bot }}
\mathrel{|} \underline{
\mathsf {s}}
\mathrel {\oplus} \underline{
\mathsf {s}}$. As an example of use, consider the following:

\[ 
\begin {array}{
l
c
l
l
}Let
&
A
&denote
&
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}.
\\{}Let
&
R
&denote
&
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}.
\\{}Let
&
C
&denote
&
0
= 
1
\vdash 
{\makebox [0mm][l]{$\bot $}\,{\bot }}.
\\{}Let
&
T
&denote
&
R
\mathrel {\oplus} 
C
\mathrel {\oplus} 
A.
\\{}Let
&
L
&denote
&
T
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}.
\end {array} \]

\noindent The construct $
\forall \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}$ states that $\underline{
\mathsf {a}}$ is provable for all object terms $\underline{
\mathsf{x}}$. Hence, $
A$ above is an axiom scheme which says that $\underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}$ for all object terms $\underline{
\mathsf {a}}$.

The construct $\underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}$ states that if $\underline{
\mathsf {a}}$ is provable then $\underline{
\mathsf {b}}$ is provable. $\underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}$ is right associative and has higher priority than $
\forall \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}$, so $
R$ above means $
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}$. Hence, $
R$ is the inference rule which states that $\underline{
\mathsf {a}}
= \underline{
\mathsf {b}}$ and $\underline{
\mathsf {a}}
= \underline{
\mathsf {c}}$ infer $\underline{
\mathsf {b}}
= \underline{
\mathsf {c}}$. The macro that expands $
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {d}}$ into $
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {d}}$ is defined in \cite{appendix}.

The construct $
{\makebox [0mm][l]{$\bot $}\,{\bot }}$ denotes absurdity, i.e. meta-falsehood (we reserve $
\mathsf {F}$ and $
\bot $ to denote falsehood and infinite looping, respectively, at the object level). Hence, $
C$ above states that $
0
= 
1$ is an absurdity.

The construct $\underline{
\mathsf {a}}
\mathrel {\oplus} \underline{
\mathsf {b}}$ states that both $\underline{
\mathsf {a}}$ and $\underline{
\mathsf {b}}$ are provable. Hence, $
T$ above is the axiomatic theory which comprises the axiom scheme $
A$, the inference rule $
R$, and the statement that $
0
= 
1$ is an absurdity.

The lemma $
L$ above says that $\underline{
\mathsf {a}}
= \underline{
\mathsf {a}}$ is provable in the theory $
T$.

The construct $\underline{
\mathsf {a}}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {b}}$ states that if computation of $\underline{
\mathsf {a}}$ yields $
\mathsf {T}$ then $\underline{
\mathsf {b}}$ is provable. $\underline{
\mathsf {a}}$ must be expressed in the Logiweb programming language (c.f.\ \cite{base}). $
\mathsf {T}$ denotes truth in the Logiweb programming language. If $\underline{
\mathsf {a}}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {b}}$ then we shall say that $\underline{
\mathsf {a}}$ {\em endorses} $\underline{
\mathsf {b}}$. The endorsement operator allows to express side conditions as we shall see later.

A {\em Logiweb sequent} is a triple $
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}$ where $
\mathsf {c}$ is a Logiweb statement and $
\mathsf {p}$ and $
\mathsf {s}$ are finite sets of Logiweb statements. The sequent $
\{
\mathsf {p}
_{
1
}
,\linebreak [0] \ldots
,\linebreak [0] 
\mathsf {p}
_{
\mathsf {m}
}
\}
\mathrel { : \, : }
\{
\mathsf {s}
_{
1
}
,\linebreak [0] \ldots
,\linebreak [0] 
\mathsf {s}
_{
\mathsf {n}
}
\}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}$ represents $
\mathsf {p}
_{
1
}
\vdash \ldots
\vdash 
\mathsf {p}
_{
\mathsf {m}
}
\vdash 
\mathsf {s}
_{
1
}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \ldots
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf {s}
_{
\mathsf {n}
}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf {c}$. The operations of Logiweb sequent calculus are:

\[
\begin {array}{
r
l
l
l
r
l
l
}
\mathsf {a}
{} ^ { I }
&
 \rightarrow 
&
\emptyset 
,\linebreak [0] 
\emptyset 
,\linebreak [0] 
\mathsf {a}
\vdash 
\mathsf {a}
\mathrel { : \, : }
\mathsf {T}
&

&
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\forall 
\mathsf{x}
\colon 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
\mathop {\char64} 
\mathsf {a}
&
 \rightarrow 
&
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\langle 
\mathsf {c}
\,{|}
\mathsf{x}
{:=}\,
\mathsf {a}
\rangle 
\mathrel { : \, : }
\mathsf {T}\footnotemark
\\{}
\mathsf {a}
\vdash 
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
&
 \rightarrow 
&
\mathsf {p}
\backslash \{ 
\mathsf {a}
\}
,\linebreak [0] 
\mathsf {s}
,\linebreak [0] 
\mathsf {a}
\vdash 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
&

&
\mathsf {p}
,\linebreak [0] 
\mathsf {s}
,\linebreak [0] 
\mathsf {a}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf {b}
\mathrel { : \, : }
\mathsf {T}
{} ^ { V } 
&
 \rightarrow 
&
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {b}
\mathrel { : \, : }
\mathsf {T}\footnotemark
\\{}
\mathsf {a}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
&
 \rightarrow 
&
\mathsf {p}
,\linebreak [0] 
\mathsf {s}
\backslash \{ 
\mathsf {a}
\}
,\linebreak [0] 
\mathsf {a}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
&

&
\mathsf {p}
,\linebreak [0] 
\mathsf {s}
,\linebreak [0] 
\mathsf {a}
\vdash 
\mathsf {b}
\vdash 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
{} ^ { + } 
&
 \rightarrow 
&
\mathsf {p}
,\linebreak [0] 
\mathsf {s}
,\linebreak [0] 
\mathsf {a}
\mathrel {\oplus} 
\mathsf {b}
\vdash 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
\\{}
\forall 
\mathsf{x}
\colon 
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
&
 \rightarrow 
&
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\forall 
\mathsf{x}
\colon 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}\footnotemark
&

&
\mathsf {p}
,\linebreak [0] 
\mathsf {s}
,\linebreak [0] 
\mathsf {a}
\mathrel {\oplus} 
\mathsf {b}
\vdash 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
{} ^ { - } 
&
 \rightarrow 
&
\mathsf {p}
,\linebreak [0] 
\mathsf {s}
,\linebreak [0] 
\mathsf {a}
\vdash 
\mathsf {b}
\vdash 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
\\{}
\mathsf {p}
,\linebreak [0] 
\mathsf {s}
,\linebreak [0] 
\mathsf {a}
\vdash 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
{} ^ { \rhd }
&
 \rightarrow 
&
\mathsf {p}
\cup \{ 
\mathsf {a}
\}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
&

&
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
\mathrel {i.e.} 
\mathsf {n}
&
 \rightarrow 
&
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {n}
\mathrel { : \, : }
\mathsf {T}\footnotemark
\\{}
\mathsf {p}
,\linebreak [0] 
\mathsf {s}
,\linebreak [0] 
\mathsf {a}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
{} ^ { \rhd }
&
 \rightarrow 
&
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\cup \{ 
\mathsf {a}
\}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}
&

&
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {n}
\mathrel { : \, : }
\mathsf {T}
{} ^ { \ast } 
&
 \rightarrow 
&
\mathsf {p}
\mathrel { : \, : }
\mathsf {s}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}\addtocounter{footnote}{-1}\footnotemark
\\{}

&

&

&\makebox[0mm][r]{$
\mathsf {p}
_{
1
}
\mathrel { : \, : }
\mathsf {s}
_{
1
}
\mathrel { : \, : }
\mathsf {c}
_{
1
}
\mathrel { : \, : }
\mathsf {T}
; 
\mathsf {p}
_{
2
}
\mathrel { : \, : }
\mathsf {s}
_{
2
}
\mathrel { : \, : }
\mathsf {c}
_{
2
}
\mathrel { : \, : }
\mathsf {T}$}
 \rightarrow \makebox[0mm][l]{$
\mathsf {p}
_{
1
}
\cup 
\mathsf {p}
_{
2
}
\backslash \{ 
\mathsf {c}
_{
1
}
\}
\mathrel { : \, : }
\mathsf {s}
_{
1
}
\cup 
\mathsf {s}
_{
2
}
\mathrel { : \, : }
\mathsf {c}
_{
2
}
\mathrel { : \, : }
\mathsf {T}$}
\end {array}\]%
%
\footnotetext[1]{if $
\mathsf {a}$ is free for $
\mathsf{x}$ in $
\mathsf {c}$}%
%
\footnotetext[2]{if computation of $
\mathsf {a}$ yields $
\mathsf {T}$ in the Logiweb programming language}%
%
\footnotetext[3]{if $
\mathsf{x}$ is not free in any member of $
\mathsf {p}$ or $
\mathsf {s}$}%
%
\footnotetext[4]{if $
\mathsf {n}$ is defined to denote $
\mathsf {c}$}

\noindent Evaluation of a sequent operation gives a sequent or an exception. Exceptional cases are omitted above. Now let $
A'$ denote $
T
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}$. We have

\[ 
\begin {array}{
l
l
l
}
T
\vdash 
T
{} ^ { I }
{} ^ { \rhd }
{} ^ { \ast } 
; 
R
\mathrel {\oplus} 
C
\vdash 
L
{} ^ { I }
{} ^ { + } 
{} ^ { \ast } 
\mathrel {i.e.} 
A'
&
 \rightarrow 
\\{}
T
\vdash 
\emptyset 
,\linebreak [0] 
\emptyset 
,\linebreak [0] 
T
\vdash 
T
\mathrel { : \, : }
\mathsf {T}
{} ^ { \rhd }
{} ^ { \ast } 
; 
R
\mathrel {\oplus} 
C
\vdash 
\emptyset 
,\linebreak [0] 
\emptyset 
,\linebreak [0] 
A
\vdash 
A
\mathrel { : \, : }
\mathsf {T}
{} ^ { + } 
{} ^ { \ast } 
\mathrel {i.e.} 
A'
&
 \rightarrow 
\\{}
T
\vdash 
\{
T
\}
\mathrel { : \, : }
\emptyset 
\mathrel { : \, : }
T
\mathrel { : \, : }
\mathsf {T}
{} ^ { \ast } 
; 
\emptyset 
,\linebreak [0] 
\emptyset 
,\linebreak [0] 
R
\mathrel {\oplus} 
C
\vdash 
A
\vdash 
A
\mathrel { : \, : }
\mathsf {T}
{} ^ { + } 
{} ^ { \ast } 
\mathrel {i.e.} 
A'
&
 \rightarrow 
\\{}
T
\vdash 
\{
T
\}
,\linebreak [0] 
\emptyset 
,\linebreak [0] 
R
\mathrel {\oplus} 
C
\mathrel {\oplus} 
A
\mathrel { : \, : }
\mathsf {T}
; 
\emptyset 
,\linebreak [0] 
\emptyset 
,\linebreak [0] 
R
\mathrel {\oplus} 
C
\mathrel {\oplus} 
A
\vdash 
A
\mathrel { : \, : }
\mathsf {T}
{} ^ { \ast } 
\mathrel {i.e.} 
A'
&
 \rightarrow 
\\{}
T
\vdash 
\{
T
\}
,\linebreak [0] 
\emptyset 
,\linebreak [0] 
R
\mathrel {\oplus} 
C
\mathrel {\oplus} 
A
\mathrel { : \, : }
\mathsf {T}
; 
\{
R
\mathrel {\oplus} 
C
\mathrel {\oplus} 
A
\}
\mathrel { : \, : }
\emptyset 
\mathrel { : \, : }
A
\mathrel { : \, : }
\mathsf {T}
{} ^ { \ast } 
\mathrel {i.e.} 
A'
&
 \rightarrow 
\\{}
T
\vdash 
\{
T
\}
\mathrel { : \, : }
\emptyset 
\mathrel { : \, : }
L
\mathrel { : \, : }
\mathsf {T}
{} ^ { \ast } 
\mathrel {i.e.} 
A'
 \rightarrow 
T
\vdash 
\{
T
\}
\mathrel { : \, : }
\emptyset 
\mathrel { : \, : }
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
\mathrel { : \, : }
\mathsf {T}
\mathrel {i.e.} 
A'
&
 \rightarrow 
\\{}
\emptyset 
,\linebreak [0] 
\emptyset 
,\linebreak [0] 
T
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
\mathrel { : \, : }
\mathsf {T}
\mathrel {i.e.} 
A'
 \rightarrow 
\emptyset 
\mathrel { : \, : }
\emptyset 
\mathrel { : \, : }
A'
\mathrel { : \, : }
\mathsf {T}
\end {array} \]

\noindent which proves $
A'$.

The syntax of {\em Logiweb sequent terms} reads $\underline{
\mathsf {q}}::=\underline{
\mathsf {s}}
{} ^ { I }
\mathrel{|} \underline{
\mathsf {s}}
\vdash \underline{
\mathsf {q}}
\mathrel{|} \underline{
\mathsf {s}}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {q}}
\mathrel{|} 
\forall \underline{
\mathsf {v}}
\colon \underline{
\mathsf {q}}
\mathrel{|} \underline{
\mathsf {q}}
{} ^ { \rhd }
\mathrel{|} \underline{
\mathsf {q}}
\mathop {\char64} \underline{
\mathsf {s}}
\mathrel{|} \underline{
\mathsf {q}}
{} ^ { V } 
\mathrel{|} \underline{
\mathsf {q}}
{} ^ { + } 
\mathrel{|} \underline{
\mathsf {q}}
{} ^ { - } 
\mathrel{|} \underline{
\mathsf {q}}
\mathrel {i.e.} \underline{
\mathsf {s}}
\mathrel{|} \underline{
\mathsf {q}}
{} ^ { \ast } 
\mathrel{|} \underline{
\mathsf {q}}
; \underline{
\mathsf {q}}$. A sequent term $
\mathsf {q}$ is said to {\em prove} the statement $
\mathsf {c}$ if $
\mathsf {q}$ evaluates to $
\emptyset 
\mathrel { : \, : }
\emptyset 
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}$ (\cite{base} allows $
\mathsf {q}$ to evaluate to $
\mathsf {p}
\mathrel { : \, : }
\emptyset 
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {T}$ provided all elements of $
\mathsf {p}$ are names of previously proved lemmas).



\section{Object theories}\label{section:ObjectTheories}

Logiweb sequent calculus is like assembly language: general and machine friendly, but it needs syntactic sugar. The user friendliness of the combined system of Logiweb, Logiweb sequent calculus, and syntactic sugar has been tested during a course in logic in which ten students wrote Logiweb pages that proved $\overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}$ from the raw axioms of Mendelsons system $
S$ (Peano arithmetic) \cite{mendelson}. It was found that the students could prove commutativity, get the proof verified, and write a report on that in less than three weeks, starting with little experience in Logiweb, mechanical proof checking, and logic in general. For links to the reports, consult \url{http://yoa.dk/}.

While proving $\overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}$ from the raw axioms may be a good student exercise, it was found that the deduction theorem and parallel instantiation of object variables was badly needed. Versions of theorems that used inference $
\vdash $ and meta variables were easier to use than theorems using implication $
\Rightarrow $ and object variables, but the axiom of induction forced implication and object variables upon the students. Instantiation of object variables is cumbersome because axiom A4 in \cite{mendelson} only allows to instantiate one variable at a time whereas the students needed parallel instantiation, e.g.\ when swapping two object variables. And hypothetical reasoning either required manual unfolding of the deduction theorem or programming of a proof tactic that could cost a lot of CPU-time for large developments.

An {\em inference rule of deduction} would eliminate these problems. If, however, $
\forall_{obj} \overline{
\mathsf{x}}
\colon 
\forall_{obj} \overline{
\mathsf{y}}
\colon \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{y}}
= \overline{
\mathsf{x}}$ is an object statement and $
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}$ is a meta statement, then the deduction rule is a meta meta statement. We do not want to introduce a meta meta level above the Logiweb sequent calculus just to express deduction so we shall express deduction using the side condition machinery of the sequent calculus.



\subsection{Peano arithmetic}

A modified version of Mendelsons system $
S$ (Peano arithmetic) \cite{mendelson} may be formulated thus:

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}

\item \makebox[0.45\textwidth][l]{$
[
S
\stackrel{
stmt
}{\rightarrow}
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
{}'
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
{}'
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
{\neg }\underline{
\mathsf {a}}
\vdash \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
\langle 
\lceil \underline{
\mathsf {b}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {a}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil 
0
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {c}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {a}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf{x}}
{}'
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
0
= \underline{
\mathsf {a}}
{}'
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\vdash 
\forall_{obj} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\cdot 
0
= 
0
]$}$
[
MP
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
]
[
MP
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{$
[
Gen
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\vdash 
\forall_{obj} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}
]
[
Gen
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}$
[
Ded
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
]
[
Ded
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{$
[
Neg
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
{\neg }\underline{
\mathsf {a}}
\vdash \underline{
\mathsf {a}}
]
[
Neg
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}$
[
S2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
{}'
]
[
S2
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{$
[
S3
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
0
= \underline{
\mathsf {a}}
{}'
]
[
S3
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}$
[
S4
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
{}'
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]
[
S4
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{$
[
S5
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
]
[
S5
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}$
[
S6
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
]
[
S6
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{$
[
S7
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\cdot 
0
= 
0
]
[
S7
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}$
[
S8
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
]
[
S8
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
S1
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
]
[
S1
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
S9
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
\langle 
\lceil \underline{
\mathsf {b}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {a}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil 
0
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {c}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {a}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf{x}}
{}'
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
]
[
S9
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$\footnote{$
\langle 
\lceil \underline{
\mathsf {a}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {b}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {c}}
\rceil 
\rangle $ says `the object term $\underline{
\mathsf {b}}$ where the object variable $\underline{
\mathsf{x}}$ is replaced by the object term $\underline{
\mathsf {c}}$ is alpha equivalent to the object term $\underline{
\mathsf {a}}$, c.f.\ \cite{appendix}}

\end{list}

\noindent As defined in \cite{base}, $
[
S5
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
]
[
S5
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$ macro expands into a lemma and a proof where the lemma says $
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}$ and the proof is a proof of that lemma. $
[
S
\stackrel{
stmt
}{\rightarrow}
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
{}'
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
{}'
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
{\neg }\underline{
\mathsf {a}}
\vdash \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
\langle 
\lceil \underline{
\mathsf {b}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {a}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil 
0
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {c}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {a}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf{x}}
{}'
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
0
= \underline{
\mathsf {a}}
{}'
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\vdash 
\forall_{obj} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\cdot 
0
= 
0
]$ macro expands into a definition which defines $
S$ as the conjunction of $
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}$ and all the other rules attributed to $
S$. The $
[{\cal X}
\stackrel{
stmt
}{\rightarrow}
\mathsf{x}
]$ macro is somewhat complex since it has to scan the entire page to find all rules related to the theory being defined. The benefit of collecting rules from the entire page is that it gives authors the freedom to introduce axioms one by one.

The deduction rule $
Ded$ is such that e.g.\ $
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}$ allows to conclude $\underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}$ and $\overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}$ allows to conclude $\underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}$ so $
Ded$ implements both deduction and parallel instantiation. All complexity is hidden in the side condition which is defined in \cite{appendix}.

Having the deduction rule, axioms A1, A2, A4, and A5 in \cite{mendelson} become superfluous. For proofs of those axioms based on deduction, see \cite{appendix}.

As an example of a development, \cite{appendix} proves the following lemmas from \cite{mendelson} in system $
S$:

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}

\item $
[
Prop\ 3.2a
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.2b
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.2c
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.2d
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.2e
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.2f
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.2g
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
]$

\item $
[
Prop\ 3.2h
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
]$

\end{list}

\noindent In the present paper we merely show the proof of an auxiliary lemma which proves the induction step of $
Prop\ 3.2f$:

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item $
[
Prop\ 3.2f_2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
]$



\item $
[
Prop\ 3.2f_2
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\vdash 
S2
\rhd \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
; 
S6
\gg 
0
+ \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
\rhd 
0
+ \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
\gg \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
\gg \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\end{list}

\noindent As defined in \cite{base}, $
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {b}}$ macro expands into $
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {b}}$. $
S2
\rhd L04
\gg \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
; \underline{
\mathsf {b}}$ macro expands into a local macro definition and a call to a proof tactic. The local macro definition defines $L05$ as shorthand for $\underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'$ and the proof tactic expands the line into $
S2
{} ^ { I }
{} ^ { \rhd }
{} ^ { \ast } 
{} ^ { \rhd }
\mathop {\char64} \underline{
\mathsf {a}}
\mathop {\char64} 
0
+ \underline{
\mathsf {a}}
; \underline{
\mathsf {b}}$ using unification. For more details see \cite{appendix}.



\section{Conclusion and further work}

Logiweb sequent calculus with examples from traditional Peano arithmetic has been presented. For further examples, click `Map Theory' at http://yoa.dk/. Map theory is an equational theory. In that theory, all definitions present on a lemmas home page become axioms according to an `axiom of definition' which is expressible by a side condition in the Logiweb sequent calculus.

The traditional deduction theorem requires that no application of Gen is made to variables free in the premise. The side condition of the deduction rule above is quite different. Proving the consistency of the deduction rule is work of the future but is expected to be straightforward since, in the standard model, a statement holds for all natural numbers if and only if it holds for all terms.



%------------------------------------------------------------------------------
\bibliographystyle{alpha}
\bibliography{./page}
%------------------------------------------------------------------------------
\everymath{}
\everydisplay{}

\end{document}
