\documentclass[12pt]{article}
\textheight 552.4pt
\textwidth 5in
%
\usepackage{amsthm}
%\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{proof}
%\usepackage{latexsym}
% \usepackage{rsfs}
\def\imp{\to}
\def\ra{\rightarrow}
\newcommand{\ib}[1]{\textit{\textbf{#1}}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\def\Ra{\Rightarrow}
\swapnumbers
\theoremstyle{remark}
\newtheorem{example}{Example}[section]
\renewcommand{\theexample}{\thedefinition.\arabic{example}}
\newtheorem{remark}[example]{Remark}
\newtheorem{notation}[example]{Notation}
\newtheorem{note}[example]{Note}
\newtheorem{elemma}[example]{Lemma}
\newtheorem{exercise*}[example]{Exercise$^*$}
\newtheorem{informal}[example]{\textbf{Informal interpretation}}
\newtheorem{warning}[example]{Warning}
%
\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]
\newtheorem{discussion}[definition]{Discussion}
\newtheorem{HistoricalComment}[definition]{Historical Comment}
% \renewcommand{\thedefinition}{\thesection\arabic{definition}}
%
\theoremstyle{plain}
\newtheorem{theorem}[definition]{Theorem}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{corollary}[definition]{Corollary}
\newtheorem{proposition}[definition]{Proposition}
\newtheorem{fact}[definition]{Theorem}
%
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
%
\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{January 23, 2002}
\begin{document}
\thispagestyle{empty}
%
\noindent
Yuichi Komori

\bigskip

\begin{center}
{$\lambda\rho$-Calculus: A NATURAL DEDUCTION FOR CLASSICAL LOGIC}
\end{center}


%\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 intuitionistic implicational 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(cf. \cite{komori00}). Then we have discovered the $\lambda\rho$--calculus, introduced in the present paper.
%
% \section{The type-free $\lambda\rho$-calculus and its type assignment}
% \setcounter{definition}{0}
%
\section{The type free $\lambda\rho$-calculus}
\begin{definition}[$\lambda\rho$-terms]
An infinite sequence of \ib{$\lambda$-variables} is assumed to be given,
and an infinite sequence of \ib{$\rho$-variables} is assumed to be given.
Then linguistic expressions called \ib{$\lambda\rho$-terms} are defined thus:
\begin{enumerate}
\item each $\lambda$-variable is a $\lambda\rho$-terms, called an \ib{atom} or \ib{atomic term};
\item if $M$ and $N$ are $\lambda\rho$-terms then $(MN)$ is a $\lambda\rho$-term called
	an \ib{application};
\item if $M$ is a $\lambda\rho$-term and $a$ is a $\rho$-variable then
	$(aM)$ is a $\lambda\rho$-term called an \ib{absurd};
\item if $f$ is a $\lambda$-variable or a $\rho$-variable and $M$ is a $\lambda\rho$-term then
	$(\lambda f. M)$ is a $\lambda\rho$-term called an \ib{abstract}. \\
	(If $f$ is a $\lambda$-variable or a $\rho$-variable, then it is called a
	\ib{$\lambda$-abstract} or a \ib{$\rho$-abstract} respectively.)
\end{enumerate}
\end{definition}
%
\begin{notation} \emph{$\lambda$-variables} are denoted by ``$u$'', ``$v$'', ``$w$'', ``$x$'',
``$y$'', ``$z$'', with or without number-subscripts. \emph{$\rho$-variables} are denoted by
``$a$'', ``$b$'', ``$c$'', ``$d$'', with or without number-subscripts.  \emph{A term-variable}
means a $\lambda$-variable or a $\rho$-variable. \emph{Term variables} are denoted by
``$f$'', ``$g$'', ``$h$'', with or without number-subscripts. Distinct letters denotes
distinct variables unless otherwise stated.

\emph{A term $\lambda a.M$} is sometimes denoted by $\rho a.M$
if the variable $a$ is a $\rho$-variable.

\emph{Arbitrary $\lambda\rho$-terms} are denoted by ``$L$'', ``$M$'', ``$N$'', ``$P$'', ``$Q$'',
``$R$'',``$S$'',``$T$'', with or without number-subscripts. For ``\emph{$\lambda\rho$-term}''
we shall say just ``\emph{term}''.
\end{notation}
%
\begin{definition}[Free, bound] A non-binding variable occurence $\underline{f}$
in a term $M$ is said to be \ib{bound in} $M$ iff it is in the scope of an occurrence of
$\lambda f$ in $M$, otherwise it is \ib{free in} $M$.

A variable $f$  is said to be \ib{bound in} $M$ iff M contains an occurence of
$\lambda f$; and $f$ is said to be \ib{free in} $M$ iff $M$ contains a free occurence of $f$.
The set of all variables free in $M$ is called
\[ FV(M). \]
\end{definition}
%
\begin{definition}[$\rho\beta$-contraction]
A \ib{$\rho\beta$-redex} is any $\lambda\rho$-term of the form $aMN$, $(\lambda x. M)N$ or $(\lambda a. M)N$;
its \ib{contractum} is $aM$, $[N/x]M$ or $\lambda a. ([\lambda x. a(xN)/a]M)N$ respectively. The
\ib{re-write rules} are 
\begin{center}
\begin{tabular}{llll}
$aMN$ & $\rhd_{1\rho\beta}$ & $aM$ , &  \\
$(\lambda x. M)N$ & $\rhd_{1\rho\beta}$ & $[N/x]M$ , & \\
$(\lambda a. M)N$ & $\rhd_{1\rho\beta}$ & $\lambda a. ([\lambda x. a(xN)/a]M)N$ . & \\
\end{tabular}
\end{center}
If $P$ contains a $\rho\beta$-redex-occurrence $\underline{R}$ and $Q$ is the result of replacing this by its contractum,
we say $P$ \ib{$\rho\beta$-contracts to} $Q$ ($P\rhd_{1\rho\beta}Q$) and we call the triple $\langle P,\underline{R},Q\rangle$
a \ib{$\rho\beta$-contraction of} $P$.
\end{definition}
%
\setcounter{example}{0}
\begin{elemma}
$ P\rhd_{1\rho\beta}Q \hspace{3mm}\Longrightarrow\hspace{3mm} FV(P)\supseteq FV(Q)$. 
\end{elemma}
%
\begin{definition}[$\rho\beta$-reduction]
A \ib{$\rho\beta$-reduction} of a term $P$ is a finite or infinite sequence of $\rho\beta$-contractions with form
\[ \langle P_1,\underline{R}_1,Q_1\rangle, \langle P_2,\underline{R}_2,Q_2\rangle, \dots \]
where $P_1\equiv_\alpha P$ and $Q_i\equiv_\alpha P_{i+1}$ for $i=1,2,\ldots$. (The empty sequence is allowed.) We
say a finite reduction is \ib{from $P$ to $Q$} iff either it has $n\geq 1$ contractions and $Q_n\equiv_\alpha Q$
or it is empty and $P\equiv_\alpha Q$. A reduction from $P$ to $Q$ is said to \ib{terminate} or \ib{end} at
$Q$. If there is a reduction from $P$ to $Q$ we say $P$ \ib{$\rho\beta$-reduces to} $Q$, or
\[ P\rhd_{\rho\beta} Q. \]

Note that $\alpha$-conversions are allowed in a $\rho\beta$-reduction.
\end{definition}
%
\begin{fact}[(Church-Rosser Theorem for $\rho\beta$)]
\label{mainB}
If $M \rhd_{\rho\beta} P$ and $M \rhd_{\rho\beta} Q$ then there exists $T$
such that
\[ P \rhd_{\rho\beta} T, \ \ \ Q \rhd_{\rho\beta} T.\]
\end{fact}
%
\section{Assigning types to terms}
\begin{definition}[Types] An infinite sequence of \ib{type-variables} is assumed to be given,
distinct from the term-variables. \ib{Types} are linguistic expressions defined thus:
\begin{enumerate}
\item each type-variable is a type (called an \ib{atom});
\item if $\sigma$ and $\tau$ are types then $(\sigma\rightarrow\tau)$ is a type (called a
	\ib{composite type}).
\end{enumerate}
\end{definition}
%
\begin{notation} \ib{Type-variables} are denoted by ``$p$'', ``$q$'', ``$r$''
with or without number-subscripts, and distinct letters denote distinct variables unless
otherwise stated.

\ib{Arbitrary types} are denoted by lower-case Greek letters except ``$\lambda$'' and
``$\rho$''.

\ib{Parentheses} will often (but not always) be omitted from types, and the reader
should restore omitted ones in such a way that, for example,
\[ \rho\rightarrow\sigma\rightarrow\tau \equiv (\rho\rightarrow(\sigma\rightarrow\tau)) \]
This restoration rule is called \ib{association to the right}.
\end{notation}
%
\begin{definition} A \ib{type-assignment} is any expression
\[ M : \tau \]
where $M$ is a $\lambda\rho$-term or a $\rho$-variable and $\tau$ is a type; we call $M$ its
\ib{subject} and $\tau$ its \ib{predicate}.
\end{definition}

(``$M:\tau$'' should be read informally as ``\emph{assign to $M$ the type $\tau$}'' or ``\emph{$M$
has type
$\tau$}''
or ``\emph{$M$ denotes a member of whatever set $\tau$ denotes}''.)
%
\begin{definition} A \ib{type-context} $\Gamma$ is any finite, perhaps empty, set of
type-assignments
\[ \Gamma = \{f_1: \rho_1, \ \ldots, \ f_m:\rho_m\} \]
whose subjects are term-variables which is \ib{consistent} in the
sense that no term-variable is the subject of more than one assignment. For any such
$\Gamma$ define
\[ Subjects(\Gamma) = \{f_1,\ldots,f_m\}. \]
\end{definition}
%
\setcounter{example}{0}
\begin{notation} The result of removing from $\Gamma$ the assignment whose subject is $f$ (if
$\Gamma$ has one) is called
\[ \Gamma - f. \]
(If $f\notin Subjects(\Gamma)$ we define $\Gamma - f = \Gamma$.) The result of removing from
$\Gamma$ all
assignments $f_i:\rho_i$ with $f_i\notin FV(M)$ (where $M$ is a given term) is called
\[ \Gamma\upharpoonright M \]
or ``\emph{$\Gamma$ restricted to $M$}''. And $\Gamma$ is called an ``\ib{$M$-context}'' (for a given
$M$) iff
\[ Subjects(\Gamma) = FV(M). \]

$\Gamma_\lambda$ and $\Gamma_\rho$ denote the subsets of $\Gamma$ of all assignments whose
subjects are $\lambda$-variables and $\rho$-variables respectively.
\end{notation}
%
\begin{note} A type-context $\Gamma$ is a set, not a sequence. Hence it does not change
when its members are permuted or repeated.
\end{note}
%
%
\begin{definition} We say $\Gamma_1$ \ib{is consistent with} $\Gamma_2$ iff
$\Gamma_1\cup\Gamma_2$ is consistent; and $\Gamma_1,\ldots,\Gamma_n$
are \ib{mutually consistent} if their union is consistent.
\end{definition}
%
\begin{definition}[TA$_{\lambda\rho}$-formulae] For any type-context $\Gamma$ and
any type-assignment $M:\tau$, the pair $\langle\Gamma; M:\tau\rangle$ is called a 
\ib{TA$_{\lambda\rho}$-formula} and is written as
\[ \Gamma_\lambda \mapsto \Gamma_\rho,\ M:\tau \]
(or just $\mapsto M :\tau$ when $\Gamma$ is empty).
We shall call $M$ the \ib{subject} of this
formula and $\tau$
its \ib{predicate}.
\end{definition}
%
\setcounter{example}{0}
\begin{notation} The following abbreviations will often be used:
\[ f_1:\sigma_1,\ldots,f_n:\sigma_n \hspace{4mm}for\hspace{4mm}
\{f_1:\sigma_1,\ldots,f_n:\sigma_n\}, \]
\[ \Gamma, f_1:\sigma_1,\ldots,f_n:\sigma_n \hspace{4mm}for\hspace{4mm}
\Gamma\cup\{f_1:\sigma_1,\ldots,f_n:\sigma_n\}. \]
\end{notation}
%
%
\begin{definition}[The system TA$_{\lambda\rho}$] TA$_{\lambda\rho}$ has an infinite set of
axioms and four
deduction-rules (called ($\ra$E) or \emph{$\ra$-elimination}, ($\ra$I) or \emph{$\ra$-introduction},
(Absurd) and (Rati)), as follows.\\[3mm]
%
\ib{Axioms of TA$_{\lambda\rho}$}: for every term-variable $x$ and every type $\tau$,
TA$_{\lambda\rho}$ has an axiom
\[ x:\tau \mapsto x:\tau. \]
\ib{Deduction-rules of TA$_{\lambda\rho}$}:
\[ \vcenter{\infer[(\ra E)]
{\langle\Gamma_1\cup\Gamma_2; (PQ):\tau\rangle}{
	\langle\Gamma_1; P:(\sigma\ra\tau)\rangle & \langle\Gamma_2; Q:\sigma\rangle}}
	\hspace{5mm}[if\ \Gamma_1\cup\Gamma_2\ is\ consistent], \]
\[\vcenter{\infer[(\ra I)]
{\langle\Gamma-x; (\lambda x.P):(\sigma\ra\tau)\rangle}
{\langle\Gamma; P:\tau\rangle}}
\hspace{5mm}[if\ \Gamma\ is\ consistent\ with\ x:\sigma],\]
\[\vcenter{\infer[(Absurd)]
{\langle\Gamma, a:\tau; (aP):\sigma\rangle}
{\langle\Gamma; P:\tau\rangle}}
\hspace{5mm}[if\ \Gamma\ is\ consistent\ with\ a:\tau],\]
\[\vcenter{\infer[(Rati)]
{\langle\Gamma-a; (\lambda a.P):\tau\rangle}
{\langle\Gamma; P:\tau\rangle}}
\hspace{5mm}[if\ \Gamma\ is\ consistent\ with\ a:\tau].\]
\end{definition}
%
\setcounter{example}{0}
\begin{example}[$((\alpha \to \beta) \to \alpha) \to \alpha$]
\[\infer[(\to I)]{\mapsto\lambda y. \rho a. y(\lambda x.ax):((\alpha \to \beta) \to \alpha)
\to \alpha}
{\infer[(Rati)]{y:(\alpha\ra\beta)\ra\alpha\mapsto\rho a. y(\lambda x.ax):\alpha}
{\infer[(\to E)]{y:(\alpha\ra\beta)\ra\alpha\mapsto a:\alpha, y(\lambda x.ax):\alpha}
{y:(\alpha\ra\beta)\ra\alpha\mapsto y:(\alpha \to \beta) \to \alpha &
\infer[(\to I)]{\mapsto a:\alpha,\lambda x.ax:\alpha \to \beta}
{\infer[(Absurd)]{x:\alpha\mapsto a:\alpha, ax:\beta}
{x:\alpha\mapsto x:\alpha}}}}} \]
%

The above TA$_{\lambda\rho}$-deduction is often written as below;
\[\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}}}}}, \]
%
or in more compact style;
\[\infer[\lambda y]{((\alpha \to \beta) \to \alpha) \to \alpha}
{\infer[\rho a]{\hspace{2mm}\alpha\hspace{2mm}}{\infer[(\to E)]{\alpha}
{y:(\alpha \to \beta) \to \alpha &
\infer[\lambda x]{\alpha \to \beta}{\infer[a]{\beta}
{x:\alpha}}}}}. \]
\end{example}
%
\begin{definition} Let $\Gamma$ be a type-context. If there is a
TA$_{\lambda\rho}$-deduction of a formula
$\langle\Gamma'; M:\tau\rangle$ for some $\Gamma' \subseteq \Gamma$ we shall say
\[ \Gamma_\lambda\vdash_{\lambda\rho} \Gamma_\rho, M:\tau. \]

In the special case $\Gamma = \emptyset$ we shall say \ib{$M$ has type $\tau$ in
TA$_{\lambda\rho}$}, or \ib{$\tau$ is a type of $M$
in TA$_{\lambda\rho}$}, or
\[ \vdash_{\lambda\rho} M:\tau. \]

The phrase ``in TA$_{\lambda\rho}$'' may be omitted when no confusion is likely.
\end{definition}
%
\begin{fact}[A $\lambda\rho$-term 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 $\langle\Gamma; M:\alpha\rangle$. Then
every type in $\Delta$ has an occurence in $\alpha$ or in a type in $\Gamma$.
\end{fact}
%
\begin{fact}[Subject-reduction Theorem]
If \ $\Gamma\vdash_{\lambda\rho}\Theta,\ P:\tau$ \ and \ $P\rhd_{\rho\beta}Q$ then
\[ \Gamma \vdash_{\lambda\rho}\Theta,\ Q:\tau. \]
\end{fact}
%
\nocite{Hindley}
\nocite{Hindley2}
%\bibliographystyle{plain}
%\bibliography{logic}
\begin{thebibliography}{1}
\bibitem{Hindley2}
J.~Roger Hindley.
\newblock {\em Basic Simple Type Theory}, volume~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}, volume~1
  of {\em London Mathematical Society Student Texts}.
\newblock Cambridge University Press, 1986.
\bibitem{komori00}
Yuichi Komori.
\newblock A natural deduction for classical logic, in which there exists a
  proof with the subformula property.
\newblock In {\em Proc. 33rd MLG meeting}, pages 3--6, Echigo Yuzawa, 2000.
\newblock http://www.math.s.chiba-u.ac.jp/\~{}komori/gakkai01-10/subform.dvi(tex).
\end{thebibliography}

\bigskip
\noindent
Department of Mathematics,\\
Faculty of Science, Chiba University \\
Inage-ku Chiba 263-8522 JAPAN \\
email: {\tt komori@math.s.chiba-u.ac.jp} \\
\end{document}

