edl-l1nd.tex

%!TEX root = edl.tex


\paragraph{Inferentialism}

A less sceptical take on any mooted correspondence between formal arguments which follow good rules and valid arguments is that the formal rules do in fact provide meanings for the expressions of the language. Rather than simply setting down the meanings of expressions by stipulation, or despairing about how there could be any facts about meaning at all, we might think meaning emerges from the underlying syntax.

This inferentialism……XXX



\section{Natural Deduction Proofs}
\paragraph{Proof}

In the last chapter, we saw that using truth tables was a decidable method for evaluating sequents, but it is cumbersome and inelegant. Here, we consider elegant and powerful \emph{proof systems} for sentential logic.

A \emph{proof} in the informal sense is something which establishes the truth of some claim. Our proofs are structures made out of sentences of \lone, with the following desirable properties: \begin{itemize}
	\item Each step in the proof involves an obviously correct rule.
	\item Whenever the earlier sentences are true, the later sentences will be also; so the terminal conclusion of a proof should always be true whenever the assumptions are.
	\item All the logical truths should have a proof.
\end{itemize}

In this chapter, we'll see that there do exist proofs that meet these conditions for \lone; and thus that we can establish various claims in \lone\ without needing to consider all the \lone-structures.

\paragraph{Natural Deduction: Assumptions and $\vdash$}

The first proof system is the \emph{natural deduction} system introduced in The Logic Manual. 

In this system, every proof begins with \emph{assumptions}. \emph{Any sentence may be an assumption.} A proof terminates with a \emph{conclusion}. 

 Whenever there is a correctly constructed proof that $\phi$, on the basis of assumptions $\gamma_{1},\ldots,\gamma_{n}$, we write this \emph{syntactic sequent}: {$$\gamma_{1},\ldots,\gamma_{n}\vdash\phi.$$} This is to be read `$\phi$ is \emph{provable from} $\gamma_{1},\ldots,\gamma_{n}$', or `$\gamma_{1},\ldots,\gamma_{n}$ \emph{syntactically entail(s)} $\phi$'. If $\phi$ can be proved with no assumptions at all, we write $\vdash\phi$; in that case, we say that $\phi$ is a \emph{theorem}.

Any sentence $\phi$ may be assumed; applying no rules at all, the proof therefore terminates with $\phi$. So $\phi\vdash\phi$; not perhaps the most interesting result, but nevertheless intuitively correct.




\paragraph{Natural Deduction Rules}

 As any assumption is a proof on its own, our rules are rules for constructing new proofs from existing proofs, often (but not always) retaining the assumptions of the existing proofs.

Some rules permit an assumption to be \emph{discharged}. Suppose you have a proof of $\phi$ on the basis of assumption $\gamma$.  You thus show that \emph{if} you had a proof of $\gamma$, \emph{then} you could construct a proof of $\phi$; and this on its own is a proof of $\gamma\to\phi$, \emph{whether or not $\gamma$ is actually true}. The assumption $\gamma$ has been discharged.
 Note that $\gamma$ needn't be used, or even occur in the proof, to be discharged: the rules entitle one to discharge \emph{every} occurence of a sentence – even if there are none!

 We can consider two types of obvious rules: those which construct a proof of a new sentence of less complexity than sentence proved by the existing proof(s), and those which construct a proof of a sentence of increased complexity. We call the first type of rule \emph{elimination} rules, and the second type \emph{introduction} rules.




{
\paragraph{Natural Deduction Rules for $\mathcal{L}_{\neg,\to}$}
Let us consider for the moment the fragment of \lone\ involving only $\neg$ and $\to$, $\mathcal{L}_{\neg,\to}$. We have in this fragment four rules, laid out in Table \ref{tfour}, elimination rules and introduction rules for each connective. I write $[\gamma]$ to show that the rule permits the assumption $\gamma$ to be discharged.
 \begin{table}
 	\centering
	\begin{tabular}{cc}
	
	\begin{prooftree}
	\[ [\gamma] \leadsto \phi
	\]
 \justifies \gamma\to\phi \using{{\to}\text{Intro}}
\end{prooftree} & \begin{prooftree}
	\gamma \to \phi \qquad \gamma \justifies \phi \using{{\to}\text{Elim}}
\end{prooftree}\\[30pt]
\begin{prooftree}
	\[ [\phi] \leadsto \psi\]
	\[ [\phi] \leadsto \neg\psi\] \justifies \neg\phi \using{\neg\text{Intro}} 
\end{prooftree} &
\begin{prooftree}
	\[ [\neg\phi] \leadsto \psi\]
	\[ [\neg\phi] \leadsto \neg\psi\] \justifies \phi \using{\neg\text{Elim}} 
\end{prooftree}
	\end{tabular} \caption{Natural Deduction Rules for $\mathcal{L}_{\neg,\to}$\label{tfour}}
 \end{table}
Call this system of rules, plus the rules about assumptions, $ND_{\neg,\to}$.

\paragraph{Deduction Theorem for $ND_{\neg,\to}$}

\begin{theorem}[Deduction Theorem] $\Gamma \vdash \psi \to \phi$ iff $\Gamma,\psi \vdash \phi$.\end{theorem}
Suppose $\Gamma,\psi \vdash \phi$. Then we can apply $\to$Intro as follows: 
	\begin{equation*}
		\begin{prooftree}
\[\Gamma, [\psi] \leadsto \phi\] 
			\justifies \psi \to \phi \using{\to}\text{Intro}
				\end{prooftree}
	\end{equation*}
	
Therefore, $\Gamma\vdash\psi\to\phi$. Similarly, suppose $\Gamma\vdash\psi\to\phi$: \begin{equation*}
	\begin{prooftree}
		\[\Gamma \leadsto \psi\to\phi\] 
		\qquad \psi \justifies \phi \using {\to}\text{Elim}
	\end{prooftree}
\end{equation*} That is, $\Gamma,\psi\vdash\phi$. 


\paragraph{$\neg$Elim can be replaced by $\neg\neg$Elim}

Consider the rule: \begin{equation*}
	 \begin{prooftree}\neg\neg\phi \justifies \phi \using \neg\neg\text{Elim}
	\end{prooftree}
\end{equation*}
This rule can obviously be derived from our rules: the correctness of the syntactic sequent $\neg\neg\phi \vdash \phi$ is demonstrated by this proof: \begin{equation*}
	\begin{prooftree}
		\neg\neg\phi \quad [\neg\phi] \justifies \phi \using \neg\text{Elim} 
	\end{prooftree}
\end{equation*}   But with $\neg\neg$Elim we can show the rule $\neg$Elim is redundant, using $\neg$Intro: \begin{equation*}
	\begin{prooftree}
\[		\[[\neg \phi] \leadsto \psi\]\quad \[[\neg\phi] \leadsto \neg\psi\] \justifies \neg\neg\phi \using \neg\text{Intro} \] \justifies \phi\using\neg\neg\text{Elim}
	\end{prooftree}
\end{equation*} 




\section{A Little More Proof Theory}

`Proof theory' is the mathematical examination of proofs conceived of as mathematical objects in their own right. In this section we explore a little of what this involves. We've already seen one some proof theory in section 1 of this chapter, where we showed the redundancy of the proof rule $\neg$Elim in the presence of $\neg\neg$Elim, and vice versa.

\paragraph{The Language $\mathcal{L}_{DP}$}

Consider the language $\mathcal{L}_{DP}$ which contains all sentence letters, and all sentences involving only the connectives $\wedge,\to$, and also contains a \emph{sentential constant} $\bot$. A sentential constant is syntactically like a sentence letter, but (unlike sentence letters) it gets a constant interpretation in every structure – in this case, for any structure $\mathscr{A}$, $|\bot|_{\mathscr{A}}=F$. The atomic sentences of $\mathcal{L}_{DP}$ thus include $\bot$ and all sentence letters; complex sentences are then built up in the usual way. 

\paragraph{Translating between $\mathcal{L}_{DP}$ and \lone} It's clear that the \lone\ sentence `$\neg \phi$' expresses the same truth function as the $\mathcal{L}_{DP}$ sentence `$\phi \to \bot$' (consideration of a truth table will suffice to show this). 
Using this translation, we can give $\mathcal{L}_{DP}$-versions of the natural deduction rules for $\neg$ in \lone, as seen in Table \ref{negldp}.
\begin{table}
	\centering
	\begin{tabular}{cc}
		\begin{prooftree}
			\[[\phi] \leadsto \psi\] \[[\phi] \leadsto \psi \to \bot\] \justifies \phi \to \bot \using{\neg\text{Intro}_{DP}}
		\end{prooftree}	&	\begin{prooftree}
					\[[\phi\to\bot] \leadsto \psi\] \[[\phi\to\bot] \leadsto \psi \to \bot\] \justifies \phi \using{\neg\text{Elim}_{DP}}
				\end{prooftree}		
	\end{tabular}\caption{Negation rules in $\mathcal{L}_{DP}$\label{negldp}}
\end{table}

With the negation rules as specified, we can prove this: \begin{theorem}[Alternative Negation Rules for $\mathcal{L}_{DP}$] \label{altneg}
 $\Pi$ is a proof of some sequent in the language $\mathcal{L}_{DP}$ that makes a use $u$ of one of the Table \ref{negldp} versions of Halbach's rules iff there is another proof $\Pi'$ of the same sequent which replaces that use $u$ by a construction which only uses this rule for $\neg$ (together with the  rules for  $\to$):
	\begin{equation*}
		\begin{prooftree}
	\[	[\phi \to \bot] \leadsto \bot\] \justifies \quad\phi\quad \using{\bot_{\mathsf{C}}}
		\end{prooftree}
	\end{equation*} \begin{proof}
	\emph{If:} There are two cases. Case 1: Suppose $\Pi$ is a proof that makes use of $\neg$Intro$_{DP}$. Then we can replace that use by the following construction, which yields another proof $\Pi'$ which uses only the rules for $\to$:
	\begin{equation*}
			\begin{prooftree}
					\[\[[\phi] \leadsto \psi\] \[[\phi] \leadsto \psi \to \bot\] \justifies\bot \using{\to\text{Elim}}\]\justifies\phi\to\bot\using{\to\text{Intro}} 
			\end{prooftree}
	\end{equation*}
	Case 2: Suppose $\Pi$ is a proof that makes use of $\neg$Elim$_{DP}$. Then we can replace that use by the following construction, which yields another proof $\Pi'$ which uses only the new rule $\bot_{\mathsf{C}}$ and the rule $\to$Elim:
\begin{equation*}
		\begin{prooftree}
				\[	\[[\phi\to\bot] \leadsto \psi\] \[[\phi\to\bot] \leadsto \psi \to \bot\] \justifies \bot \using{\to\text{Elim}}							
				\] \justifies \phi \using{\bot_{\mathsf{C}}}
				\end{prooftree}
\end{equation*}

\emph{Only if}: Suppose $\Pi$ is a proof which makes use of the new rule $\bot_{\mathsf{C}}$. Then we may replace that use by the following construction which uses only the old rules for $\to$ and $\neg$Elim$_{DP}$.
\begin{equation*}
	 \begin{prooftree}
		\[[\phi \to \bot] \leadsto \bot\] \[[\bot]\justifies\bot\to\bot \using{\to\text{Intro}}\]\justifies\phi\using{\neg\text{Elim}_{DP}} 
	\end{prooftree}
\end{equation*}								
	\end{proof}
\end{theorem} 


\paragraph{Reducing Complexity of Proofs}

Return now to the \lone-fragment containing only $\to,\wedge,\neg$. Let the \emph{(degree of) complication} of a sentence be the number of connectives occurring in the sentence (a sentence letter has degree of complication 0, if $\phi$ and $\psi$ have degree of complication $m$ and $n$ respectively, then $(\phi \wedge \psi)$ has degree of complication $m+n+1$, etc.) We can now show: \begin{theorem}[Reducing Complexity of Proofs] \label{redcompl}
	If $\Pi$ is a proof in Halbach's system for $\mathcal{L}_{\to,\wedge,\neg}$  that $\Gamma \vdash \phi$, in which the most complicated sentence resulting from an application of $\neg$Elim is $\psi$, then (when $\psi$ is not atomic) there is a distinct proof $\Pi'$ of $\Gamma \vdash \phi$ in which the results of all applications of $\neg$Elim are \emph{less complicated} than $\psi$. Indeed, there exists a proof $\Pi^{\dag}$ of that sequent, in which the result of every application of $\neg$Elim is atomic.
	\begin{proof}
		Suppose that the most complicated result of $\neg$Elim in $\Pi$ is $\psi$. So part of $\Pi$ looks like this: \begin{equation*}
			\begin{prooftree}
				\[\Gamma \quad [\neg \psi] \justifies \leadsto \chi\] \[\Delta \quad [\neg \psi] \leadsto \neg\chi\] \justifies \psi \using{\neg\text{Elim}}
			\end{prooftree}
		\end{equation*} $\psi$ is complicated (not a sentence letter), so given there are three connectives in this language,  there are three cases: \begin{enumerate}
			\item $\psi = \neg \pi$. In which case replace that part of the proof sketched above with this one: \begin{equation*}
				\begin{prooftree}
					\[\Gamma \[[\pi] \quad [\neg \pi] \justifies \neg\neg\pi \using{\neg\text{Intro}}\] \leadsto \chi\]
					\[\Delta  \[[\pi] \quad [\neg \pi] \justifies \neg\neg\pi \using{\neg\text{Intro}}\] \leadsto \neg\chi\] \justifies \neg\pi \using{\neg\text{Intro}}
				\end{prooftree}
			\end{equation*}
		\item $\psi = \pi \wedge \xi$. Proof left for Exercise.
			\item $\psi = \pi \to \xi$. In which case replace that part of the proof sketched above with this one: \begin{equation*}
	\hskip-1.5cm			\begin{prooftree}
				\[	\[\Gamma  \[\[ [\pi \to \xi] \quad [\pi] \justifies \xi \using{\to\text{Elim}}\] \quad [\neg \xi] \justifies \neg(\pi \to \xi) \using{\neg\text{Intro}}\] \leadsto \chi\]
				\[\Delta \[\[ [\pi \to \xi] \quad [\pi] \justifies \xi \using{\to\text{Elim}}\] \quad [\neg \xi] \justifies \neg(\pi \to \xi) \using{\neg\text{Intro}}\] \leadsto \neg\chi\]
					 \justifies  \xi \using{\neg\text{Elim}}\]\justifies \pi \to \xi \using{\to\text{Intro}}
				\end{prooftree}
			\end{equation*}
		\end{enumerate}	

Notice that applying these replacements repeatedly to uses of $\neg$Elim in a proof will eventually replace all complex sentences in uses of $\neg$Elim by simpler ones. All sentences of \lone\ are finitely complex, and all proofs involve only finitely many applications of a given rule, this process terminates after a finite time with only atomic sentences as the conclusions of uses of $\neg$Elim. 
	\end{proof}
\end{theorem}

It is clear that we can put the results of Theorems \ref{altneg} and \ref{redcompl} together, to establish that, in the system which involves the normal rules for $\wedge$ and $\to$, and has $\bot_{\mathsf{C}}$ as its only other rule, if $\Pi$ is a proof in the system $DP$ that $\Gamma \vdash_{DP}\phi$, then there exists a proof of that sequent, $\Pi^{\dag}$, in which the result of any application of $\bot_{\mathsf{C}}$ is atomic. (I leave the proof as a problem.)







{\small
\subsection*{Further Reading}
\addcontentsline{toc}{subsection}{Further Reading}

Natural deduction was invented  by \citet{geninvinl}, the founder of proof theory. 
The proof theory of natural deduction systems discussed in this chapter is based on \citet[39--41]{pranatde}; he uses Theorems \ref{altneg} and \ref{redcompl}, and the last problem, and proves the famous `cut elimination' theorem for natural deduction, unfortunately a topic beyond the scope of these notes.



 The axiom system here was developed by Jan \L ukasiewicz, simplifying Frege's system: see \citet[p. 25]{boslogwol}. (The Polish notation used in this article is initially confusing, but has the wonderful feature that it is entirely unambiguous without the use of parentheses.)
See also \citet[ch. 5--6]{bosintlo}; he gives a direct proof of the completeness of a system based on \L\ at pp.\ 217--9.


\subsection*{Exercises}
\addcontentsline{toc}{subsection}{Exercises}


\begin{enumerate}
	\item \begin{enumerate}
\item Devise introduction and elimination rules for a natural deduction system for the language $\mathcal{L}_{\uparrow}$ with the Sheffer Stroke as its only connective, being sure to fully justify your answer. How many such rules do we need?
	\item Suppose in a system of natural deduction $ND$ for \lone\ we replaced the $\neg$Elim rule by the following, \emph{ex falso quodlibet}: \begin{equation*}
		\begin{prooftree}
			\psi \qquad \neg\psi \justifies \phi \using \text{EFQ}
		\end{prooftree}
	\end{equation*}
\begin{enumerate}
	\item Is the resulting system $ND'$ equivalent (in terms of what can be proved) to the original system? (Justify your answer; it is somewhat difficult to prove conclusively, but give some reasons for your view.)
	\item What happens if we, in addition, replace $\neg$Intro by the following rule, \emph{tertium non datur}, yielding the system $ND''$? \begin{equation*}
		\begin{prooftree}
			\[[\phi] \leadsto \psi\] \[[\neg\phi] \leadsto \psi\] \justifies \psi \using\text{TND}
		\end{prooftree}
	\end{equation*}
\end{enumerate}	
\item Consider the natural deduction system $ND_{\to,\vee}$ for the language $\mathcal{L}_{\to,\vee}$ in which the only connectives are $\to,\vee$. Suppose we introduce to the language the zero-place sentential constant $\bot$, and add the following rules to the proof system, yielding $ND_{\to,\vee,\bot}$: \begin{equation*}
	\begin{prooftree}
		\bot \justifies \phi \using\bot
	\end{prooftree}\qquad
	\begin{prooftree}
		\[[\phi \to \bot] \leadsto \bot\]
		\justifies \phi \using \text{C}
	\end{prooftree}
\end{equation*}\begin{enumerate}
	\item Give a natural translation between $\mathcal{L_{\to,\vee,\bot}}$  and $\mathcal{L}_{\to,\vee,\neg}$.
	\item Using that translation, can you show that the proof system $ND_{\to,\vee,\bot}$ just introduced is equivalent to the natural deduction system $ND_{\to,\vee,\neg}$ involving just Halbach's rules for $\to$, $\vee$ and $\neg$?
	\end{enumerate}
\item A mystery connective $\oplus$ has the following introduction and elimination rules: 

\begin{equation*}
	\begin{prooftree}
		\phi\oplus\psi \justifies \psi \using\oplus\text{Elim}
	\end{prooftree}\qquad \begin{prooftree}
		\phi \justifies \phi\oplus\psi \using\oplus\text{Intro}
	\end{prooftree}
\end{equation*}

\begin{enumerate}
	\item Show that no system containing a connective defined by these rules is sound. 
	\item What limits should be placed on the ability of introduction and elimination rules to define or characterise the inferential role of a connective in light on this result? (This question invites discussion, not a definitive answer. You may wish to consult \citet{prirunint}.)
	\end{enumerate}
	\item  Relatedly to 1.(d).ii: \label{fouronee}\begin{enumerate}
		\item Check, by means of truth tables, that $(((P\to Q)\to P)\to P)$ is a tautology.	
		\item Give a natural deduction proof of $(((P\to Q)\to P)\to P)$.
		\item Every valid argument involving only sentences containing $\wedge$ as their only connective can be proved valid using just the rules $\wedge$Intro and $\wedge$Elim. In that sense, $\wedge$ is completely characterised by its introduction and elimination rules. What do the previous results show about $\to$ in this connection?
\end{enumerate}
\end{enumerate}
\item Prove the omitted case (where the complex sentence is a conjunction) in the proof of Theorem \ref{redcompl}.
\item Show  that, in the system which involves the normal rules for $\wedge$ and $\to$, and has $\bot_{\mathsf{C}}$ as its only other rule, if $\Pi$ is a proof in the system $DP$ that $\Gamma \vdash_{DP}\phi$, then there exists a proof of that sequent, $\Pi^{\dag}$, in which the result of any application of $\bot_{\mathsf{C}}$ is atomic.
\end{enumerate}





}