\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{$\lambda\rho$-Calculus: A Natural Deduction for Classical Logic}
\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 $\lambda\rho$--calculus.
While the type assignment system $TA_\lambda$
gives a natural deduction for implicational intuitionistic logic,
the type assignment system $TA_{\lambda\rho}$ gives a natural deduction for
classical implicational logic.
Moreover for any classical implicational theorem $\alpha$ there exists
a proof of $\alpha$ in $TA_{\lambda\rho}$ 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 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. Then we have discovered the
$\lambda\rho$--calculus.
%
% \section{The type-free $\lambda\rho$-calculus and its type assignment}
% \setcounter{definition}{0}
%
\begin{definition}[$\lambda\rho$-terms]\em \ 
An infinite sequence of $\lambda$-variables is assumed to be given,
and an infinite sequence of $\rho$-variables is assumed to be given.
Then linguistic expressions called $\lambda\rho$-terms are defined thus:
\begin{enumerate}
\item each $\lambda$-variable is a $\lambda\rho$-terms, called an atom or atomic term;
\item if $M$ and $N$ are $\lambda\rho$-terms then $(MN)$ is a $\lambda\rho$-term called
	an application;
\item if $M$ is a $\lambda\rho$-term and $a$ is a $\rho$-variable then
	$aM$ is a $\lambda\rho$-term called an absurd;
\item if $x$ is a $\lambda$-variable and $M$ is a $\lambda\rho$-term then
	$(\lambda x. M)$ is a $\lambda\rho$-term called an abstract or a $\lambda$-abstract;
\item if $a$ is a $\rho$-variable and $M$ is a $\lambda\rho$-term then
	$(\rho a. M)$ is a $\lambda\rho$-term called a rationalization.
\end{enumerate}
\end{definition}
%
\begin{definition}[$\rho\beta$-reduction]\em \ 
Any $\lambda\rho$-term of form $aMN$, $(\lambda x. M)N$, $(\rho a. M)N$
is called a $\rho\beta$-redex.
$\rho\beta$-contracting an occurrence of a redex in
a term $U$ means replacing one occurence of
\begin{center}
\begin{tabular}{llll}
$aMN$ & by & $aM$ , &  \\
$(\lambda x. M)N$ & by & $[N/x]M$ , & \\
$(\rho a. M)N$ & by & $\rho a. ([\lambda x. a(xN)/a]M)N$ . & \\
\end{tabular}
\end{center}
If this changes $U$ to $V$, we say U $\rho\beta$-contracts to $V$, or
\[ U \rhd_{1\rho\beta} V . \]
We say $U$ $\rho\beta$-reduces to $V$, or
\[ U \rhd_{\rho\beta} V , \]
iff $V$ is obtained from $U$ by a finite (perhaps empty) series of
$\rho\beta$-contractions and changes of bound variables.
% When there is no danger of confusion, '$\mu\beta$' may be omitted.
\end{definition}
\begin{fact}[(Church-Rosser Theorem for $\rho\beta$)]
\label{mainB}
If $M \rhd_{\rho\beta} P$ and $N \rhd_{\rho\beta} Q$ then there exist $T$
such that
\[ P \rhd_{\rho\beta} T, \ \ \ Q \rhd_{\rho\beta} T.\]
\end{fact}

%
Types are defined as usual.

\begin{definition}[The type-assignment system $TA_{\lambda\rho}$]\em \ 
$TA_\lambda\rho$ is a Natural Deduction system. Its formulas are arbitrary
expressions $M:\alpha$, where $M$ is a $\lambda\rho$-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[(\to I)]{\lambda x. M : \alpha \to \beta}{\deduce{M:\beta}{
	\deduce{\Pi}{x:\alpha} }},
\]

\[
\infer[(Absurd)]{aM:\beta}{\deduce{M:\alpha}{\Pi}},
\qquad
\infer[(Rati)]{\rho a. M : \alpha}{\deduce{M:\alpha}{
	\Pi }}.
\]
\end{definition}
%
\begin{example}[$((\alpha \to \beta) \to \alpha) \to \alpha$]
\[\infer[(\to I)]{\lambda y. \rho a. y(\lambda x.ax):((\alpha \to \beta) \to \alpha) \to \alpha}
{\infer[(Rati)]{\rho a. y(\lambda x.ax):\alpha}{\infer[(\to E)]{y(\lambda x.ax):\alpha}{
y:(\alpha \to \beta) \to \alpha &
\infer[(\to I)]{\lambda x.ax:\alpha \to \beta}{\infer[(Absurd)]{ax:\beta}
{x:\alpha}}}}} \]
\end{example}
\begin{fact}[$TA_{\lambda\rho}$ is a proof of classical implicational logic]
$\alpha$ is a classical implicational theorem  \ \ if and only if \ \ 
there exists a closed $\lambda\rho$-term $M$ such that \ \ \ $\vdash_{\lambda\rho} M:\alpha$.
\end{fact}
%
\begin{fact}[Normalization Theorem for $TA_{\lambda\rho}$]
Every $TA_\lambda\rho$-typable term has a $\rho\beta$-normal form.
\end{fact}
\begin{fact}[Subformula Property for $TA_{\lambda\rho}$]
Let $\lambda\rho$-term $M$ be a $\rho\beta$-normal form and 
$\Delta$ a $TA_{\lambda\rho}$-deduction of $M:\alpha$. Then
every type in $\Delta$ has an occurence in $\alpha$ or in a predicate
of undischarged assumptions.
\end{fact}
%
\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}
