Brontekst bekijken van Beweren en bewijzen/de zuilen/Zekerheid/5. Natuurlijke deductie/deductieschema/latex

%<noinclude><source lang="tex">
\documentclass[11pt]{article}

\usepackage[a4paper,vmargin={3.0cm,2.5cm},hmargin={1.5cm,1.5cm}]{geometry}
%\usepackage{a4wide}
\usepackage{moreverb}
\usepackage{longtable}
\usepackage{url}
\usepackage{array}
\usepackage{multicol}
\usepackage{amssymb, amsmath}
\usepackage[dutch,english]{babel}
\pagestyle{empty}

\newcommand{\forget}[1]{\addtolength{\textheight}{#1}\setlength{#1}{0pt}}
\forget{\headheight}
\forget{\headsep}
\forget{\footskip}

\selectlanguage{dutch}

\renewcommand{\implies}{\rightarrow}
\renewcommand{\impliedby}{\leftarrow}
\renewcommand{\iff}{\leftrightarrow}

\setlength\extrarowheight{1pt}
\setlength{\columnsep}{0.6cm}
\begin{document}

\centerline{\Large\bf Afleidingsregels voor Natuurlijke Deductie
\tiny{(versie 23/04/14)}}
%\footnote{
%Gebaseerd op J.F.A.K.\ van Benthem, H.P. van Ditmarsch, J.\ Ketting, J.S.\
%Lodder,
%W.P.M.\ Meyer-Viol. \textit{Logica voor informatica, derde editie.} Pearson
%Education.
%ISBN 90-430-0722-6.
%maart 2003, maar aangepast aan de cursus Beweren en Bewijzen.}
\noindent
\begin{longtable}[c]{|ll|}
\hline
Regel & Opmerkingen \hfill Coq commando \\
\hline
\endhead
\hline
\endfoot
\hline
\multicolumn{2}{c}{}\\
\hline
\multicolumn{2}{|c|}{Basisregels voor klassieke logica}\\
\hline
& \hfill\texttt{assumption.} \\
$ \dfrac{}
{~\Sigma, \alpha \vdash \alpha~}\text{hyp} $
& \hfill\texttt{hyp H.} \\
& \\
\hline
& \\
$ \dfrac{~\Sigma \vdash \alpha \implies \beta \qquad \Sigma \vdash \alpha~}
{\Sigma \vdash \beta}{\implies}E $ (\textit{modus ponens})
& \hfill\texttt{imp\_e $\alpha$.}\\
& \\
$ \dfrac{\Sigma, \alpha \vdash \beta}
{~\Sigma \vdash \alpha \implies \beta~}{\implies}I $
& \hfill\texttt{imp\_i H.}\\
& \\
\hline
& \\
$ \dfrac{~\Sigma \vdash \neg \alpha \qquad \Sigma \vdash  \alpha~}
{\Sigma \vdash \beta}\neg E $ (\textit{inconsistentie})
& \hfill\texttt{neg\_e $\alpha$.}\\
& \\
\multicolumn{2}{|l|}{%
$ \dfrac{~\Sigma,\neg \beta \vdash \neg \alpha \qquad \Sigma,\neg \beta \vdash
 \alpha~}
{\Sigma \vdash \beta}\neg E* $ (\textit{bewijs uit het ongerijmde})
\hfill \texttt{neg\_e' $\alpha$ H.}
}\\
& \\
$ \dfrac{~\Sigma,\beta \vdash \neg \alpha \qquad \Sigma,\beta \vdash \alpha~}
{\Sigma \vdash \neg \beta}{\neg}I $ (\textit{weerlegging})
& \hfill\texttt{neg\_i $\alpha$ H.} \\
& \\
\hline
& \\
$ \dfrac{~\Sigma \vdash \alpha \land \beta~}
{\Sigma \vdash \alpha}{\land}E1 $
& \hfill\texttt{con\_e1 $\beta$.}\\
& \\
$ \dfrac{~\Sigma \vdash \alpha \land \beta~}
{\Sigma \vdash \beta}{\land}E2 $
& \hfill\texttt{con\_e2 $\alpha$.}\\
& \\
$ \dfrac{~\Sigma \vdash \alpha \qquad \Sigma \vdash \beta~}
{\Sigma \vdash \alpha \land \beta}{\land}I $
& \hfill\texttt{con\_i.}\\
& \\
\multicolumn{2}{|l|}{%
$ \dfrac{~\Sigma \vdash \alpha \lor \beta \qquad \Sigma,\alpha \vdash
\gamma
\qquad \Sigma,\beta \vdash \gamma~}
{\Sigma \vdash \gamma}{\lor}E $ (\textit{gevalsonderscheiding})
\hfill \texttt{dis\_e ($\alpha$} \url{\/} \texttt{$\beta$) G H.}}\\
& \\
%$ \dfrac{\Sigma \vdash \alpha \lor \beta \qquad \Sigma,\alpha \vdash \gamma
%\qquad \Sigma,\beta \vdash \gamma}{\Sigma \vdash \gamma}{\lor}E $
%(\textit{gevalsonderscheiding}) &\texttt{dis\_e ($\alpha$} \verb+\/+
%\texttt{$\beta$) G H.}\\
 %& \\
$ \dfrac{\Sigma \vdash \alpha}
{~\Sigma \vdash \alpha \lor \beta~}{\lor}I1 $
& \hfill\texttt{dis\_i1.}\\
& \\
$ \dfrac{\Sigma \vdash \beta}
{~\Sigma \vdash \alpha \lor \beta~}{\lor}I2 $
& \hfill\texttt{dis\_i2.}\\
& \\
\hline
\multicolumn{2}{c}{}\\
\hline
\multicolumn{2}{|c|}{Speciaal om klassieke bewijzen korter op te kunnen
schrijven}\\
\hline
& \\
$ \dfrac{}
{~\Sigma \vdash \alpha \lor \neg \alpha~}\text{LEM}$ \textit{(law of
excluded middle)}
& \hfill\texttt{LEM.}\\
& \\
%\hline
\pagebreak
%\hline
\multicolumn{2}{c}{}\\
\hline
\multicolumn{2}{|c|}{Regels om met kwantoren te kunnen werken}\\
\hline
& \\
$ \dfrac{\Sigma \vdash \forall x,\alpha}
{~\Sigma \vdash \alpha[x{:=}t]~}{\forall}E $ (\textit{instantiatie})
& \hfill\texttt{all\_e (forall x, $\alpha$) t.} \\*
& term $t$ is een zeker speciaal geval\\*
& vrije variabelen in $t$ moeten ook vrij zijn in $\alpha[x{:=t}]$\\*
& \\
$ \dfrac{~\Sigma \vdash \alpha[x{:=}y]~}
{\Sigma \vdash \forall x,\alpha}{\forall}I $ (\textit{generalisatie})
& \hfill\texttt{all\_i y.}\\*
& $y$ is vrij in $\alpha[x{:=}y]$\\*
& $y$ komt niet vrij voor in $\Sigma$\\*
& $y$ komt niet vrij voor in $\forall x,\alpha$\\
& \\
$ \dfrac{~\Sigma \vdash \exists x, \alpha \qquad \Sigma, \alpha[x{:=}y]
\vdash \gamma~}
{\Sigma \vdash \gamma}{\exists}E $
& \hfill\texttt{exi\_e (exists x, $\alpha$) y H.}\\*
& $y$ is vrij in $\alpha[x{:=}y]$\\*
& $y$ komt niet vrij voor in $\gamma$\\*
& $y$ komt niet vrij voor in $\Sigma$\\*
& $y$ komt niet vrij voor in $\exists x,\alpha$\\
& \\
$ \dfrac{~\Sigma \vdash \alpha[x{:=}t]~}
{\Sigma \vdash \exists x,\alpha}{\exists}I $ (\textit{abstractie})
& \hfill\texttt{exi\_i t.}\\*
& term $t$ is een zeker speciaal geval\\*
& vrije variabelen in $t$ moeten ook vrij zijn in $\alpha[x{:=t}]$\\
& \\
\hline
\multicolumn{2}{c}{}\\
\hline
\multicolumn{2}{|c|}{Speciaal voor bewijzen met getallen}\\
\hline
& \\
$ \dfrac{~\Sigma \vdash \alpha[t_1{:=}t_2] \qquad \Sigma\vdash t_1 = t_2~}
{\Sigma \vdash \alpha}\text{repl}$
& \hfill\texttt{replace t1 with t2.}\\
& \\
$ \dfrac{~\Sigma \vdash \alpha[t\in[a,b]~{:=}~a\leq t \land t\leq b]~}
{\Sigma \vdash \alpha}\text{int}$
& \hfill\texttt{interval.}\\
& analoog voor intervallen $[a,b)$, $(a,b]$ en $(a,b)$:\\
& gesloten rand `$\leq$' en open rand `$<$'\\
& \\
$ \dfrac{}
{~\Sigma \vdash \alpha~}\text{lins}$
& \hfill\texttt{lin\_solve.}\\
& waarbij $\alpha$ via elementaire wiskunde uit $\Sigma$ volgt\\
& \\
% Sinds 10/02/14 is het volgens de grammatica niet meer toegestaan
% om te kwantificeren over intervallen, dus zijn deze regels overbodig.
%$ \dfrac{~\Sigma \vdash \forall t:T,\; t\in[a,b] \to \alpha~}
%{\Sigma \vdash \forall t:[a,b],\; \alpha}\text{$\forall$dom}$
%& \hfill\texttt{n.v.t.}\\
%& waarbij $[a,b]\subseteq T$\\
%& analoog voor intervallen $[a,b)$, $(a,b]$ en $(a,b)$\\
%& \\
%$ \dfrac{~\Sigma \vdash \exists t:T,\; t\in[a,b] \land \alpha~}
%{\Sigma \vdash \exists t:[a,b],\; \alpha}\text{$\exists$dom}$
%& \hfill\texttt{n.v.t.}\\
%& waarbij $[a,b]\subseteq T$ \\
%& analoog voor intervallen $[a,b)$, $(a,b]$ en $(a,b)$
\end{longtable}

\centerline{\large\bf Notaties en toelichting}

\begin{multicols}{2}
\begin{tabular}{ll}
 $\Sigma$ & een (mogelijk lege) rij aannames \\
 $\alpha, \beta, \gamma$ & beweringen \\
 $x, y$ & variabelen \\
 $t, t_1, t_2$ & termen \\
 $G, H$ & namen voor nieuwe aannames \\
 $a, b$ & intervalgrenzen
\end{tabular}

\smallskip
\noindent Een rij aannames schrijven we als $\alpha, \beta,
\gamma$.
De rij aannames $\Sigma, \alpha$ wordt gevormd door $\Sigma$ uit te
breiden met $\alpha$.

\smallskip
\noindent
De bewering $\alpha[x{:=}t]$ ontstaat uit de bewering $\alpha$ door daarin
alle vrije voorkomens van variabele $x$ te vervangen door term $t$.
Voorbeeld: $\mathit{P~x~\land~\neg P~x \implies (\forall
x,P~x)[x{:=}t_1{+}t_2]}$ staat voor $\mathit{P~(t_1{+}t_2) \land \neg
P~(t_1{+}t_2) \implies (\forall x,P~x)}$.

\smallskip
\noindent
De bewering $\alpha[t_1{:=}t_2]$ ontstaat uit de bewering $\alpha$ door
daarin
alle voorkomens van term $t_1$ te vervangen door term $t_2$.

\smallskip
\noindent
Let op de analogie\"en tussen $\land$ en $\forall$ en tussen $\lor$ en
$\exists$ en op de dualiteiten tussen $\land$ en $\lor$ en tussen $\forall$
en $\exists$.
\end{multicols}
\end{document}
%</source></noinclude>