Beweren en bewijzen/de zuilen/Zekerheid/5. Natuurlijke deductie/deductieschema/latex
%<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>
