\documentclass{article}
\oddsidemargin 0cm \evensidemargin 0cm
\topmargin 0.46cm \headheight 0cm \headsep 0cm
%\textheight 23cm \textwidth 16cm
\textheight 24.0cm \textwidth 16cm
\pagestyle{empty}
%
\usepackage{proof,latexsym}
\usepackage{rsfs}
\def\imp{\to}
\def\ra{\Rightarrow}
%\def\land{\mathbin\&}
\newtheorem{definition}{DEFINITION}[section]
\newtheorem{lemma}[definition]{LEMMA}
\newtheorem{theorem}[definition]{THEOREM}
\newtheorem{fact}[definition]{FACT}
\newtheorem{abbreviation}[definition]{ABBREVIATION}
\newtheorem{corollary}[definition]{COROLLARY}
\newtheorem{proposition}[definition]{PROPOSITION}
\newtheorem{example}[definition]{EXAMPLE}
\newtheorem{remark}[definition]{REMARK}
\newtheorem{conjecture}[definition]{CONJECTURE}
\def\T{\mathscr{T}}
%\setlength{\textwidth}{230pt}
%\renewcommand{\baselinestretch}{2}
%
\title{A Natural Deduction for Classical Logic, in which there exists
a proof with the Subformula Property}
\author{ Yuichi KOMORI \\
\texttt{komori@math.s.chiba-u.ac.jp} \\
	Department of Mathematics,
	Faculty of Science, Chiba University \\
	Inage-ku Chiba 263-8522 JAPAN}
\date{}
\begin{document}
\maketitle
%
In this note, we will pose a new system, named $\mu$--calculus.
$\lambda$--calculus can be simulated in $\mu$--calculus.
While the type assignment system $TA_\lambda$
gives a natural deduction for implicational intuitionistic logic,
the type assignment system $TA_\mu$ gives a natural deduction for
classical implicational logic.
Moreover for any classical implicational theorem $\alpha$ there exists
a proof of $\alpha$ in $TA_\mu$ enjoying the subformula property.

Ryo Kashima has posed a Natural deduction system for the classical
implicational logic. His system has three rules, the elimination of
the implication, the introduction of the implication and the case rule.
The author has noticed that the introduction of the implication is
derivable from the case rule and the weakening. So we have gotten
the system $TA_\mu$ from Kashima's system by replacing the introduction
of implication by the weakening.
%
\section{The type-free $\mu$-calculus and its type assignment}
\setcounter{definition}{0}
%
\begin{definition}[$\mu$-terms]\em \ 
An infinite sequence of term-variables is assmed to be given.
Then linguistic expression called $\mu$-terms are defined thus:
\begin{enumerate}
\item each term-variable is a $\mu$-terms, called an atom or atomic term;
\item if $M$ and $N$ are $\mu$-terms then $(MN)$ is a $\mu$-term called
	an application;
\item if $M$ is a $\mu$-term then $KM$ is a $\mu$-term called a weakening;
\item if $x$ is a term-variable and $M$ and $N$ are $\mu$-terms then
	$(\mu x. M*N)$ is a $\mu$-term called an abstract or a $\mu$-abstract.
\end{enumerate}
\end{definition}
%
\begin{definition}[$\beta$-reduction]\em \ 
Any $\mu$-term of form $KMN$, $(\mu x. M*N)R$, $\mu x. [xMN/z]P*Q$ (where
$z \in FV(P)$ and $x \notin FV(MP)$) or $\mu x. xM*N$ (where $x \notin
FV(M)$) is called a $\beta$-redex.
$\beta$-contracting an occurrence of a redex in
a term $U$ means replacing one occurence of
\begin{center}
\begin{tabular}{llll}
$KMN$ & by & $M$ , &  \\
$(\mu x. M*N)R$ & by & $\mu x. MR*NR$ & (we $\alpha$-convert
 $(\mu x. M*N)$ if necessary), \\
$\mu x. [xMN/z]P*Q$ & by & $\mu x. [xM/z]P*Q$ & (where $z \in FV(P)$ and
 $x \notin FV(MP)$), \\
$\mu x. xM*N$ & by & $[M/x]N$ & (where $x \notin FV(M)$).
\end{tabular}
\end{center}
If this changes $U$ to $V$, we say U $\beta$-contracts to $V$, or
\[ U \rhd_{1\beta} V . \]
We say $U$ $\beta$-reduces to $V$, or
\[ U \rhd_{\beta} V , \]
iff $V$ is obtained from $U$ by a finite (perhaps empty) series of
$\beta$-contractions and changes of bound variables.
% When there is no danger of confusion, '$\mu\beta$' may be omitted.
\end{definition}
\begin{conjecture}[or FACT (Church-Rosser Theorem for $\beta$)]
\label{mainB}
If $M \rhd_{\beta} P$ and $N \rhd_{\beta} Q$ then there exist $T$
such that
\[ P \rhd_{\beta} T, \ \ \ Q \rhd_{\beta} T.\]
\end{conjecture}

We can consider different types of reductions that have logical reasons,
for example, 
\[ R(\mu x. M*N) \rhd_1 \mu x. RM*RN. \]
But the reduction obtained from $\beta$-reduction adding the above
reduction does not enjoy the Church-Rosser property.
\begin{abbreviation}\label{lambda}
$(\lambda x. M) \equiv (\mu x. x * KM)$.
\end{abbreviation}
\begin{fact}[$\mu$-calculus simulates $\lambda$-calculus]
\[ (\lambda x. M)N \rhd_{\beta} [M/x]N. \]
\end{fact}
%
\begin{definition}[$\eta$-reduction]\em \ 
Any $\mu$-term of form $\mu x. x*K(Nx)$ or $\mu x. M*N$ (where
$x \notin FV(N)$) is called a $\eta$-redex.
$\eta$-Contracting an occurrence of a $\eta$-redex in
a term $U$ means replacing one occurence of
\begin{center}
\begin{tabular}{llll}
$\mu x. x*K(Nx)$ & by & $\mu x. x*N$ , & \\
$\mu x. M*N$ & by & $N$ & (where $x \notin FV(N)$)\ \ . \\
\end{tabular}
\end{center}
If this changes $U$ to $V$, we say U $\eta$-contracts to $V$, or
\[ U \rhd_{1\eta} V . \]
We say $U$ $\eta$-reduces to $V$, or
\[ U \rhd_{\eta} V , \]
iff $V$ is obtained from $U$ by a finite (perhaps empty) series of
$\eta$-contractions and changes of bound variables.
% When there is no danger of confusion, '$\mu\eta$' may be omitted.
\end{definition}
\begin{conjecture}[or FACT (Church-Rosser Theorem for $\beta\eta$)]
\label{mainC}
If $M \rhd_{\beta\eta} P$ and $N \rhd_{\beta\eta} Q$ then there exist $T$
such that
\[ P \rhd_{\beta\eta} T, \ \ \ Q \rhd_{\beta\eta} T.\]
\end{conjecture}

Types are defined as usual.

\begin{definition}[The type-assignment system $TA_\mu$]\em \ 
$TA_\mu$ is a Natural Deduction system. Its formulas are arbitrary
expressions $M:\alpha$, where $M$ is a $\mu$-term and $\alpha$ is a type.
\[
\infer[(\to E)]{MN:\beta}{\deduce{M:\alpha\to\beta}{\Pi_1} &
	\deduce{N:\alpha}{\Pi_2}},
\qquad
\infer[(Weakening)]{KM:\alpha \to \beta}{\deduce{M:\beta}{\Pi}},
\]

\[
\infer[k (Case)]{\mu x. M * N:\gamma}{\deduce{M:\gamma}{
	\deduce{\Pi_1}{\deduce{x:\alpha\to\beta}{k}}} &
	\deduce{N:\gamma}{\deduce{\Pi_2}{\deduce{x:\alpha}{k}}}}.
\]
\end{definition}
%
\begin{fact}[$TA_\mu$ is a proof of classical implicational logic]
$\alpha$ is a classical implicational theorem  \ \ if and only if \ \ 
there exists a closed $\mu$-term $M$ such that \ \ \ $\vdash_\mu M:\alpha$.
\end{fact}
%
\section{The type-free $\lambda A$-calculus and its type assignment}
%
We will next introduce an auxiliary type type-assignment system
$TA_{\lambda A}$ to prove the subformula property of the system $TA_\mu$.

\begin{definition}[$\lambda A$-terms]\em \ 
An infinite sequence of term-variables is assmed to be given.
Then linguistic expression called $\lambda A$-terms are defined thus:
\begin{enumerate}
\item each term-variable is a $\lambda A$-terms, called an atom or atomic term;
\item if $M$ and $N$ are $\lambda A$-terms then $(MN)$ is a $\lambda A$-term
called an application;
\item if $M$ is a $\lambda A$-term then $AM$ is a $\lambda A$-term called
a r-weakening;
\item if $x$ is a term-variable and $M$ is a $\lambda A$-terms then
	$(\lambda x. M)$ is a $\lambda A$-term called an abstract or
	a $\lambda$-abstract.
\end{enumerate}
\end{definition}
%
\begin{definition}[$A\beta$-reduction]\em \ 
Any $\lambda A$-term of form $AMN$ and $(\lambda x. M)N$
is called a redex.
Contracting an occurrence of a redex in
a term $U$ means replacing one occurence of
\begin{center}
\begin{tabular}{lll}
$AMN$ & by & $AM$, \\
$(\lambda x. M)N$ & by & $[N/x]M$.
\end{tabular}
\end{center}
If this changes $U$ to $V$, we say U $A\beta$-contracts to $V$, or
\[ U \rhd_{1A\beta} V . \]
We say $U$ $A\beta$-reduces to $V$, or
\[ U \rhd_{A\beta} V , \]
iff $V$ is obtained from $U$ by a finite (perhaps empty) series of
$A\beta$-contractions and changes of bound variables.
\end{definition}
%
\begin{fact}[Church-Rosser Theorem for $A\beta$] \label{mainB}
If $M \rhd_{A\beta} P$ and $N \rhd_{A\beta} Q$ then there exist $T$
such that
\[ P \rhd_{A\beta} T, \ \ \ Q \rhd_{A\beta} T.\]
\end{fact}

A $\bot$-type is a type constructed from variables and a type constant
'$\bot$'.

\begin{definition}[The type-assignment system $TA_{\lambda A}$]\em \ 
$TA_{\lambda A}$ is a Natural Deduction system. Its formulas are arbitrary
expressions $M:\alpha$, where $M$ is a $\lambda A$-term and $\alpha$ is
a $\bot$-type.
\[
\infer[(\to E)]{MN:\beta}{\deduce{M:\alpha\to\beta}{\Pi_1} &
	\deduce{N:\alpha}{\Pi_2}},
\qquad
\infer[k (\to I)]{\lambda x. M:\alpha \to \beta}{\deduce{M:\beta}{
	\deduce{\Pi}{\deduce{x:\alpha}{k}}} &
	},
\]

\[
\infer[(R-Weakening)]{AM:\alpha}{\deduce{M:\bot}{\Pi}}.
\]
\end{definition}
%
\begin{fact}[$TA_{\lambda A}$ is a proof of intutionistic logic]
$\alpha$ is a theorem of intutionistic $\{\to,\bot\}$-fragment logic
 \ \ if and only if \ \ 
there exists a closed $\lambda A$-term $M$ such that \ \ \ 
$\vdash_{\lambda A} M:\alpha$.
\end{fact}
%
\begin{fact}[Normalization Theorem for $TA_{\lambda A}$]
Every $TA_{\lambda A}$-typable term has a $A\beta$-normal form.
\end{fact}
\begin{fact}[Subformula Property for $TA_{\lambda A}$]
Let $\lambda A$-term $M$ be a $A\beta$-normal form and 
$\Delta$ a $TA_{\lambda A}$-deduction of $M:\alpha$. Then
every type in $\Delta$ has an occurence in $\alpha$ or in a predicate
of undischarged assumptions.
\end{fact}
%
\section{Transelation of $\lambda A$-terms to $\mu$-terms}
%
In this section we will define a translation $\T$ of
$\lambda A$-terms to $\mu$-terms.
At first, we define a simple translation $\T^*$ of $\lambda A$-terms
without occurences of $A$ to $\mu$-terms.

\begin{definition}[Translation $\T^*$]\em \ 
We define recursively the translation $\T^*$ of $\lambda A$-terms, in which
no $A$ occurs, to $\mu$-terms, as follows:
\begin{enumerate}
\item $\T^*(x) \equiv x$,
\item $\T^*(MN) \equiv (\T^*(M)\T^*(N))$,
\item $\T^*(\lambda x. M) \equiv (\mu x. x*K\T^*(M))$.
\end{enumerate}
\end{definition}
\begin{definition}[Translation $\T$]\em \ 
We define recursively the translation $\T$ of $\lambda A$-terms of the
form $AM$ to $\mu$-terms, as follows:
\begin{enumerate}
\item $\T(AM) \equiv \T^*(M)$ \ \  if no $A$ occurs in $N$,
\item $\T(AM) \equiv \T(AN)$ \ \  if $M$ is of the form $(\cdots AN \cdots)$
where this $A$ is the leftmost occurence and no free variable in $N$
is bounded in $M$,
\item $\T(AM) \equiv \mu x. \T(AN)*\T(AR)$ \ \ if $M$ is of the form
$(\cdots (\lambda x. \cdots AQ \cdots) \cdots)$
where this $A$ is the leftmost occurence and this '$\lambda x$' is the
leftmost occurence which bounds a free variable in $Q$ and
$N$ is obtained from $M$ by replacing $(\lambda x. \cdots AQ \cdots)$
by $x$ (we $\alpha$-convert $M$ if necessary) and
$R \equiv (\cdots (\lambda z. \cdots AQ \cdots) \cdots)$ and
the variable $z$ is new.
\end{enumerate}
\end{definition}
%
\section{Proof of Subformula Property}
%
\begin{lemma}
Let $M$ be a $A\beta$-normal term without occurences $A$, \ \ 
$\Gamma \vdash_{\lambda A} M:\alpha$ \ \ and g be a new type variable. Then
\begin{enumerate}
\item $[g/\bot]\Gamma \vdash_\mu \T^*(M):[g/\bot]\alpha$,
\item every type in $TA_\mu$-deduction of $\T^*(M):[g/\bot]\alpha$
	has an occurence in $[g/\bot]\alpha$ or in a type in $[g/\bot]\Gamma$.
\end{enumerate}
\end{lemma}
%
\begin{lemma}
Let $AM$ be a $A\beta$-normal term, \ \ 
$\Gamma \vdash_{\lambda A} M:\bot$ \ \ and g be a new type variable. Then
\begin{enumerate}
\item $[g/\bot]\Gamma \vdash_\mu \T(AM):g$,
\item every type in $TA_\mu$-deduction of $\T(AM):g$ \ \ 
	is $g$ or has an occurence in a type in $[g/\bot]\Gamma$.
\end{enumerate}
\end{lemma}
%
\begin{lemma}
Let $\alpha$ be a implicational formula and $g$ be the rightmost
variable in $\alpha$. Then\\
$\alpha$ is a classical teorem \ \ if and only if \ \ 
$[\bot/g]\alpha$ is an intuitionistic theorem.
\end{lemma}
%
\begin{theorem}[Subformula Property of $TA_\mu$]
If a type $\alpha$ is a classical implicational theorem, then
there exists a closed $\mu$-term $M$ such that
\begin{enumerate}
\item $\vdash_\mu M:\alpha$,
\item for any $TA_\mu$-deduction $\Delta$ of $M:\alpha$, every type
	in $\Delta$ has an occurence in $\alpha$.
\end{enumerate}
\end{theorem}
%
{\bf Acknowledgement.} The author would like to thank Ryo Kashima
for informing him of Kashima's Natural deduction system.
\nocite{Hindley}
\nocite{Hindley2}
%\bibliography{logic}
%\bibliographystyle{jplain}
\begin{thebibliography}{1}

\bibitem{Hindley2}
J.~Roger Hindley.
\newblock {\em Basic Simple Type Theory}, Vol.~42 of {\em Cambridge Tracts in
  Theoretical Computer Science}.
\newblock Cambridge University Press, 1997.

\bibitem{Hindley}
J.~Roger Hindley and Jonathan~P. Seldin.
\newblock {\em Introduction to combinators and $\lambda$--calculus}, Vol.~1 of
  {\em London Mathematical Society Student Texts}.
\newblock Cambridge University Press, 1986.

\end{thebibliography}
\end{document}
