\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{natural deduction}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{deduction_and_induction}{}\paragraph*{{Deduction and Induction}}\label{deduction_and_induction}

[[!include deduction and induction - contents]]

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{summary}{Summary}\dotfill \pageref*{summary} \linebreak
\noindent\hyperlink{IntroductionAndElimination}{Introduction and elimination}\dotfill \pageref*{IntroductionAndElimination} \linebreak
\noindent\hyperlink{formation_and_computation}{Formation and computation}\dotfill \pageref*{formation_and_computation} \linebreak
\noindent\hyperlink{hypothetical_reasoning}{Hypothetical reasoning}\dotfill \pageref*{hypothetical_reasoning} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{relation_to_category_theory}{Relation to category theory}\dotfill \pageref*{relation_to_category_theory} \linebreak
\noindent\hyperlink{decidability}{Decidability}\dotfill \pageref*{decidability} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

Formalization of mathematical reasoning can be presented in different forms. The framework of \textbf{natural deduction} describes a particular class of [[deductive systems]] which is supposed to be close to ``natural'' \emph{[[deductive reasoning]]} insofar it is based on the idea of \emph{reasoning from assumptions} in contrast to proof systems that reason from `truths' in the tradition of Hilbertian axiomatics. It is used particularly to present the [[syntax]] of formal [[logic]] and [[type theory]].

\begin{uremark}
The phrase ``natural deduction'' is not always used to mean the same thing. Some people use it semi-informally to refer to a ``sort of reasoning'' that involves making assumptions, perhaps formalized using hypothetical [[judgments]]. Other people take it to refer specifically to deductive systems which are presented using \emph{introduction} and \emph{elimination} rules, which is the meaning we adopt on this page. There is significant overlap between the two meanings, but they are not identical.

\end{uremark}
\hypertarget{summary}{}\subsection*{{Summary}}\label{summary}

\hypertarget{IntroductionAndElimination}{}\subsubsection*{{Introduction and elimination}}\label{IntroductionAndElimination}

A system of \emph{natural deduction} is a [[deductive system]] containing a class of [[judgments]] generated by some ``constructor'' operations, and for which each constructor comes with two relevant classes of rules:

\begin{itemize}%
\item \textbf{Introduction rules}, which allow us to conclude a judgment built using the constructor from simpler judgments; and


\item \textbf{Elimination rules}, which allow us to conclude some other judgment by using a judgment involving the constructor.



\end{itemize}
For instance, in a system of [[propositional logic]] whose judgments are the truth of [[propositions]], one such constructor might be the ``conjunction'' connective $\wedge$. The introduction rule for $\wedge$ would be

\begin{displaymath}
\frac{A \; true \qquad B\;true}{A\wedge B\; true}
\end{displaymath}
while its elimination rules might be

\begin{displaymath}
\frac{A\wedge B\; true}{A\;true} \qquad \frac{A\wedge B\;true}{B\;true}.
\end{displaymath}
The introduction and elimination rules must fit together in an appropriate way, sometimes referred to as ``harmony''.

Similarly, in a system of [[type theory]], the relevant judgments are typing judgments of the form $a:A$, meaning that the [[term]] $a$ belongs to the [[type]] $A$. In this case, an analogous constructor might be the cartesian [[product type]], whose rules are analogous, but keeping track of the specific terms involved (see [[propositions as types]]):

\begin{displaymath}
\frac{a:A \qquad b:B}{(a,b):A\times B}
\end{displaymath}
and

\begin{displaymath}
\frac{p:A\times B}{\pi_1(p):A} \qquad \frac{p:A\times B}{\pi_2(p):B}.
\end{displaymath}
\hypertarget{formation_and_computation}{}\subsubsection*{{Formation and computation}}\label{formation_and_computation}

In natural deduction systems for type theory, there are usually two other classes of rules:

\begin{itemize}%
\item \textbf{[[type formation|Formation rules]]}, which declare on which basis a new [[type]] can be introduced; and


\item \textbf{[[computation rule|Computation rules]]} or \textbf{conversion rules}, which constrain the result of combining term introduction with term elimination.



\end{itemize}
These two rules refer to different classes of judgments than the introduction and elimination rules: judgments that a certain thing is a type for the formation rules, and judgments that one term reduces to, or converts with, another, for the computation rules.

For instance, the cartesian product type would come with a formation rule

\begin{displaymath}
\frac{A\;type \qquad B\;type}{A\times B\;type}
\end{displaymath}
and computation rules such as [[beta-reduction]]

\begin{displaymath}
\frac{a:A \qquad b:B}{\pi_1(a,b) \to_\beta a} \qquad \frac{a:A \qquad b:B}{\pi_2(a,b) \to_\beta b}
\end{displaymath}
(and possibly [[eta-conversion]]).

Technically, the propositional logic system could also come with a formation rule involving a judgment ``is a proposition'':

\begin{displaymath}
\frac{A\;prop \qquad B\;prop}{A\wedge B\;prop}
\end{displaymath}
But it would not have a computation rule, as there are no terms inhabiting its propositions. (It could, however, be embedded into a type theory via [[propositions as types]], where there would be terms inhabiting its propositions regarded as types).

More generally, natural deduction with computation rules gives a formulation of [[computation]]. See \emph{[[computational trinitarianism]]} for discussion of this unification of concepts.

On the other hand, in type theories that have a [[type of types]], there may be no need for a separate judgment ``$A\;type$'', as it can be replaced by a typing judgment ``$A:Type$'' that $A$ belongs to a type of types.

\hypertarget{hypothetical_reasoning}{}\subsubsection*{{Hypothetical reasoning}}\label{hypothetical_reasoning}

Natural deduction also generally involves \emph{hypothetical judgments} or \emph{[[deductive reasoning|reasoning]] from [[assumptions]]}. For instance, the introduction rule for [[implication]] in a system of [[propositional logic]] says that if, \emph{assuming} ``$A$'', we can derive ``$B$'', then we can derive ``$A\Rightarrow B$''. This is sometimes written as

\begin{equation}
\frac{\itexarray{[A]\\ \vdots \\ B}}{A\Rightarrow B}
\label{impintro}\end{equation}
(We now follow the common practice of writing the judgment ``$A\;true$'' as simply ``$A$''.) Here the $\vdots$ indicate an arbitrary [[derivation]] tree, while the brackets around $A$ indicate that this assumption has been ``discharged'' and is no longer an assumption in the conclusion $A\Rightarrow B$. To be precise, we should annotate each bracket somehow to indicate which rule discharged that assumption.

Another way to indicate hypothetical reasoning (which also allows it to fit once again within the general notion of [[deductive system]]) is to indicate in each judgment the hypotheses on which it depends. Thus, we might write ``$A\vdash B$'' to mean a hypothetical judgment of $B$ assuming $A$. With this notation, the introduction rule for $\Rightarrow$ can be written as:

\begin{displaymath}
\frac{A\vdash B}{\vdash A\Rightarrow B}.
\end{displaymath}
The rule \eqref{impintro}, where $\vdots$ indicates an arbitrary [[derivation]], can then be written as

\begin{displaymath}
\frac{\itexarray{\frac{}{A\vdash A} \\ \vdots \\ A\vdash B}}{\vdash A\Rightarrow B}.
\end{displaymath}
Here we have prefixed the entire derivation $\vdots$ in \eqref{impintro} by ``$A\vdash$'' to indicate that it is all performed with $A$ as an assumption, and the discharge of that assumption is indicated by removing this prefix from the final conclusion. We also begin the deduction with the \emph{axiom} $A\vdash A$ (the [[identity rule]]).

To be fully precise, we should now allow all rules to take place under arbitrary additional hypotheses; thus the introduction rule of $\Rightarrow$ should really be

\begin{displaymath}
\frac{\Gamma, A\vdash B}{\Gamma\vdash A\Rightarrow B}.
\end{displaymath}
where $\Gamma$ denotes an arbitrary list of hypothesis truth judgments. However, often this unchanged ambient context is unstated, but implicitly assumed to be present.

\begin{uremark}
Hypothetical judgments of this sort are very similar to the [[sequents]] which appear in [[sequent calculus]], and are (as is evident) written with very similar notation. However, the rules of natural deduction are different from the rules of sequent calculus, as are its formal properties.

\end{uremark}
This treatment of hypothetical judgments applies also to type theories, where the individual judgments are typing judgments. In this case, the assumed judgments on the left of the $\vdash$ are generally restricted to be of the form $x:A$ with $x$ a [[variable]] (rather than an arbitrary [[term]]), and these assumed judgments are referred to as the [[context]]. When the judgment on the right of the $\vdash$ may involve variables that occur to its left, one speaks of \emph{generic judgments} rather than ``hypothetical'' ones. Thus, a generic judgment is of the form

\begin{displaymath}
(x : A) \;\vdash\; (b(x) : B)
\end{displaymath}
to be read as

\begin{quote}%
In a context where we have a term $x$ of a type $A$, there is a term $b(x)$ of [[types in context|type]] $B$.


\end{quote}
Thus, for instance, the introduction rule for the [[function type]] is

\begin{displaymath}
\frac{(x:A) \;\vdash\; (b:B)}{\vdash (\lambda x.b:A\to B)}.
\end{displaymath}
In natural deduction for [[dependent type theory]], we can also have type judgments with hypotheses, such as

\begin{displaymath}
(x : A) \;\vdash\; B(x) \; type
\end{displaymath}
to be read as

\begin{quote}%
For each $x$ in $A$ there is a type $B(x)$. Or: $B$ is a \emph{[[type in context]]} $A$, a \emph{[[dependent type|type dependent]]} on $A$.


\end{quote}
In a type theory with a [[type of types]], this judgment could be written as $(x:A)\;\vdash\;(B(x):Type)$.

\begin{uremark}
So far, we have been considering hypothetical judgments such as $A\vdash B$ and generic judgments such as $(x:A)\vdash (b(x):B)$ to be ``atomic'' judgments in a particular [[deductive system]]. In particular, the turnstile symbol $\vdash$ has been simply another symbol that we use to build judgments according to a particular syntax, analogous to the colon $:$. As remarked at [[deductive system]], this usage of $\vdash$ is \emph{a priori} completely unrelated to its use to indicate provability of theorems in a particular deductive system (such as a system of natural deduction), and therefore perhaps ought to be denoted by a different symbol.

However, it is also possible to incorporate some ``knowledge'' about the meaning of hypothetical and generic judgments into the deductive system, and thereby bring the two meanings of $\vdash$ back into alignment. See [[logical framework]] for a development of this idea.

\end{uremark}
\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{relation_to_category_theory}{}\subsubsection*{{Relation to category theory}}\label{relation_to_category_theory}

The four classes of rules of natural deduction combined give alternative specifications of [[universal constructions]] in [[category theory]]. In [[categorical semantics]] one considers categories which are such that their [[objects]] are regarded as [[types]] and their [[generalized elements]] as [[terms]], then the rules of natural deductions describe the possible construction of [[morphisms]] in that category.

For instance, the connectives of type theory are presentations of [[functors]], but their action on morphisms is not explicitly defined, because [[representability determines functoriality| the action is definable from the introduction and elimination rules]].

(\ldots{})

\hypertarget{decidability}{}\subsubsection*{{Decidability}}\label{decidability}

(\ldots{})

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[logical framework]], [[metalanguage]]


\item [[deduction calculus]]


\item [[type theory]], [[meaning explanation]]


\item [[sequent calculus]]


\item [[calculus of constructions]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

In a broad sense, the idea of natural deduction can be traced back to [[Aristotle]]`s \textbf{Prior Analytics} as classical work by J. Bacon, J. Corcoran and T. Smiley around 1970 has argued that his theory of [[syllogism]] can be viewed as a [[fragment]] of natural deduction. For more on this see e.g.

\begin{itemize}%
\item J. Bacon, \emph{Natural-deduction rules for syllogistic} , JSL \textbf{31} (1966) pp.686-7.


\item J. Corcoran, \emph{Completeness of an ancient logic} , JSL \textbf{37} (1972) pp.696-702.


\item T. Smiley, \emph{What is a syllogism} , JPL \textbf{2} (1973) pp.136-154.



\end{itemize}
The next step to the modern conception was an observation by the Polish logician (and Aristotle scholar) J. Lukasiewicz in 1926 that the formalization of mathematical reasoning proposed by [[David Hilbert|D. Hilbert]] or \emph{Principia Mathematica} fails to comply with the actual reasoning style of mathematicians. This was taken up by S. Jaskowski who published a system of natural deduction in 1934:

\begin{itemize}%
\item S. Jaskowski, \emph{On the rules of suppositions in formal logic} , Studia Logica \textbf{1} Warsaw 1934. (\href{http://www.logik.ch/daten/jaskowski.pdf}{pdf})

\end{itemize}
At about the same time [[Gerhard Gentzen|G. Gentzen]] developed a system of natural deduction in his thesis\footnote{\emph{It can be said of Gentzen that it was he who first showed how proof theory should be done}. (M. Dummett, \emph{Frege- Philosophy of Language} , Harvard UP 1981$^2$. p.434)}  - a landmark of 20th century [[mathematical logic]] introducing proof systems for [[predicate logic]] (in both [[classical logic|classical]] and [[intuitionistic logic|intuitionistic]] versions) and the concept of [[cut-elimination]] - that was published as

\begin{itemize}%
\item [[Gerhard Gentzen]], \emph{Untersuchungen \"u{}ber das logische Schlie\ss{}en}, \emph{Mathematische Zeitschrift} \textbf{39}(1), Springer-Verlag 1934-35. $<$http://dx.doi.org/10.1007/BF01201353{\tt \symbol{62}} (English translation \emph{Investigations into Logical Deduction} in Szabo)

\end{itemize}
In order to prove the famous \emph{[[Gentzen's Hauptsatz|Hauptsatz]]} for proof normalization Gentzen invented the [[sequent calculus]] though he sketched a similar result for natural deduction in his later work on the [[consistency]] of [[arithmetics]]. Normalization for systems of natural deduction was established by D. Prawitz in his thesis in 1965:

\begin{itemize}%
\item D. Prawitz, \emph{Natural Deduction - A Proof-theoretical Study} , Dover reprint New York 20061965.

\end{itemize}
A standard textbook that describes proof systems in natural deduction format, sequent calculi or Hilbert-style systems is

\begin{itemize}%
\item A. S. Troelstra, H. Schwichtenberg, \emph{Basic Proof Theory} , CUP 2000$^2$.

\end{itemize}
An introductory lecture using [[dependent type theory]] in [[intuitionistic logic]] is

\begin{itemize}%
\item [[Per Martin-Löf]], \emph{On the meaning of logical constants and the justifications of the logical laws}, leture series in Siena (1983) (\href{http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf}{web})

\end{itemize}
A formalization of the general [[logical framework]] of natural deduction is discussed in section 3 of

\begin{itemize}%
\item [[Frank Pfenning]], \emph{Logical frameworks -- A brief introduction} (\href{http://www.cs.cmu.edu/~fp/papers/mdorf01.pdf}{pdf})

\end{itemize}
A good account is at

\begin{itemize}%
\item Wikipedia, \emph{\href{http://en.wikipedia.org/wiki/Natural_deduction}{Natural deduction}}

\end{itemize}
The standard rules for type-formation, term introduction/elimination and computation in [[dependent type theory]] are listed for instance in \href{http://www.math.unipa.it/~ngambino/Research/Lectures/lecture1.pdf}{part I} of

\begin{itemize}%
\item [[Nicola Gambino]], \emph{Lectures on dependent type theory} (\href{http://www.cs.le.ac.uk/events/mgs2009/courses/gambino/lecturenotes-gambino.pdf}{pdf})

\end{itemize}
[[!redirects natural deduction]] [[!redirects natural deductions]]

[[!redirects term introduction]] [[!redirects term introduction rule]] [[!redirects term introduction rules]] [[!redirects introduction rule]] [[!redirects introduction rules]]

[[!redirects term elimination]] [[!redirects term elimination rule]] [[!redirects term elimination rules]] [[!redirects elimination rule]] [[!redirects elimination rules]]

[[!redirects computation rule]] [[!redirects computation rules]] [[!redirects conversion rule]] [[!redirects conversion rules]]

[[!redirects term constructor]] [[!redirects term constructors]]

[[!redirects inference rule]] [[!redirects inference rules]]

[[!redirects rule of inference]] [[!redirects rules of inference]]



\end{document}