Mercurial > 13ws.ds
diff notes/tex/logic.tex @ 35:010d8f7fa899
seventh slides and sheet
author | Markus Kaiser <markus.kaiser@in.tum.de> |
---|---|
date | Mon, 02 Dec 2013 23:36:05 +0100 |
parents | b5094b3e3111 |
children | 3de775b67d8c |
line wrap: on
line diff
--- a/notes/tex/logic.tex Mon Dec 02 23:35:45 2013 +0100 +++ b/notes/tex/logic.tex Mon Dec 02 23:36:05 2013 +0100 @@ -857,3 +857,103 @@ \end{definition} \end{frame} } + +\defineUnit{natuerlichesschliessenquantoren}{% +{ + \newcommand{\F}{\tau} + \newcommand{\G}{\varphi} + \newcommand{\K}{\chi} + \newcommand{\subproof}[2]{% + \begin{tikzpicture}[y=.9em] + \path + (0, 0) node (a) {##1} + ++(0, -1) node (b) {$\vdots$} + ++(0, -1) node[below] (c) {##2}; + \node[fit=(a)(b)(c), draw, inner sep=1pt] {}; + \end{tikzpicture}% + } + \newcommand{\topproof}[1]{% + ##1 + \bottomAlignProof + \DisplayProof + } + \newcommand{\capt}[1]{\vspace{-2em}##1} + + \begin{frame} + \frametitle{Natürliches Schließen} + \setbeamercovered{dynamic} + + \begin{definition}[Ersetzung] + Sei $\G$ eine Formel und $a$ eine Konstante.\\ + Mit \structure{$\G[x/a]$} bezeichnen wir die Formel die man erhält, wenn man alle \alert{freien} Vorkommnisse von \structure{$x$} in \structure{$\G$} durch \structure{$a$} \structure{ersetzt}. + \end{definition} + \vfill + \tabulinesep=4pt + \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]} + & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} + \capt{$\exists$} & + \topproof{ + \AxiomC{$\F[x/a]$} + \RightLabel{\scriptsize $+\exists$} + \UnaryInfC{$\exists x. \F$} + } + & + \topproof{ + \AxiomC{$\exists x. \F$} + \AxiomC{\subproof{$a. \F[x/a]$}{$\K$}} + \RightLabel{\scriptsize $-\exists$} + \BinaryInfC{$\K$} + } + \\ + \capt{$\forall$} & + \topproof{ + \AxiomC{\subproof{$a$}{$\F[x/a]$}} + \RightLabel{\scriptsize $+\forall$} + \UnaryInfC{$\forall x. \F$} + } + & + \topproof{ + \AxiomC{$\forall x. \F$} + \RightLabel{\scriptsize $-\forall$} + \UnaryInfC{$\F[x/a]$} + } + \end{tabu} + \begin{itemize} + \vfill + \item Man muss ein \alert{unbenutztes $a$} in $+\forall$ und $-\exists$ wählen + \end{itemize} + \end{frame} +} +} + +\defineUnit{induktion}{% +\begin{frame} + \frametitle{Vollständige Induktion} + \setbeamercovered{dynamic} + + \begin{block}{Vollständige Induktion} + Die \structure{vollständige Induktion} ist eine Beweistechnik, um zu zeigen, dass alle natürlichen Zahlen ein Prädikat $P$ erfüllen. + \[ \alert{\forall n \in \N_0. P(x)} \] + Ein solcher Beweis besteht aus + \begin{description}[Induktionsanfang\quad] + \item[Induktionsanfang] Man zeigt, dass $P(0)$ gilt. + \item[Induktionsschritt] Man zeigt für ein beliebiges $k$, dass\\ + wenn $P(k)$ gilt (\structure{Induktionshypothese}),\\ + dann auch $P(k+1)$. + \end{description} + Zusammen beweisen die Teile, dass das Prädikat für alle $n \in \N_0$ gilt.\\ + \vspace{1em} + In Prädikatenlogik formuliert gilt in $\N_0$ + \begin{align} + \structure{ P(0) \wedge \forall k . \left( P(k) \rightarrow P(k+1) \right)} &\rightarrow \alert{\forall n. P(n)} + \end{align} + \end{block} + + \vfill + + \begin{itemize} + \item Kann verallgemeinert werden, z.B. auf $\Z$ + \item Aber nicht auf $\R$ (Warum?) + \end{itemize} +\end{frame} +}