Mercurial > 13ws.ds
comparison 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 |
comparison
equal
deleted
inserted
replaced
| 34:189900976413 | 35:010d8f7fa899 |
|---|---|
| 855 \end{itemize} | 855 \end{itemize} |
| 856 \end{itemize} | 856 \end{itemize} |
| 857 \end{definition} | 857 \end{definition} |
| 858 \end{frame} | 858 \end{frame} |
| 859 } | 859 } |
| 860 | |
| 861 \defineUnit{natuerlichesschliessenquantoren}{% | |
| 862 { | |
| 863 \newcommand{\F}{\tau} | |
| 864 \newcommand{\G}{\varphi} | |
| 865 \newcommand{\K}{\chi} | |
| 866 \newcommand{\subproof}[2]{% | |
| 867 \begin{tikzpicture}[y=.9em] | |
| 868 \path | |
| 869 (0, 0) node (a) {##1} | |
| 870 ++(0, -1) node (b) {$\vdots$} | |
| 871 ++(0, -1) node[below] (c) {##2}; | |
| 872 \node[fit=(a)(b)(c), draw, inner sep=1pt] {}; | |
| 873 \end{tikzpicture}% | |
| 874 } | |
| 875 \newcommand{\topproof}[1]{% | |
| 876 ##1 | |
| 877 \bottomAlignProof | |
| 878 \DisplayProof | |
| 879 } | |
| 880 \newcommand{\capt}[1]{\vspace{-2em}##1} | |
| 881 | |
| 882 \begin{frame} | |
| 883 \frametitle{Natürliches Schließen} | |
| 884 \setbeamercovered{dynamic} | |
| 885 | |
| 886 \begin{definition}[Ersetzung] | |
| 887 Sei $\G$ eine Formel und $a$ eine Konstante.\\ | |
| 888 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}. | |
| 889 \end{definition} | |
| 890 \vfill | |
| 891 \tabulinesep=4pt | |
| 892 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]} | |
| 893 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} | |
| 894 \capt{$\exists$} & | |
| 895 \topproof{ | |
| 896 \AxiomC{$\F[x/a]$} | |
| 897 \RightLabel{\scriptsize $+\exists$} | |
| 898 \UnaryInfC{$\exists x. \F$} | |
| 899 } | |
| 900 & | |
| 901 \topproof{ | |
| 902 \AxiomC{$\exists x. \F$} | |
| 903 \AxiomC{\subproof{$a. \F[x/a]$}{$\K$}} | |
| 904 \RightLabel{\scriptsize $-\exists$} | |
| 905 \BinaryInfC{$\K$} | |
| 906 } | |
| 907 \\ | |
| 908 \capt{$\forall$} & | |
| 909 \topproof{ | |
| 910 \AxiomC{\subproof{$a$}{$\F[x/a]$}} | |
| 911 \RightLabel{\scriptsize $+\forall$} | |
| 912 \UnaryInfC{$\forall x. \F$} | |
| 913 } | |
| 914 & | |
| 915 \topproof{ | |
| 916 \AxiomC{$\forall x. \F$} | |
| 917 \RightLabel{\scriptsize $-\forall$} | |
| 918 \UnaryInfC{$\F[x/a]$} | |
| 919 } | |
| 920 \end{tabu} | |
| 921 \begin{itemize} | |
| 922 \vfill | |
| 923 \item Man muss ein \alert{unbenutztes $a$} in $+\forall$ und $-\exists$ wählen | |
| 924 \end{itemize} | |
| 925 \end{frame} | |
| 926 } | |
| 927 } | |
| 928 | |
| 929 \defineUnit{induktion}{% | |
| 930 \begin{frame} | |
| 931 \frametitle{Vollständige Induktion} | |
| 932 \setbeamercovered{dynamic} | |
| 933 | |
| 934 \begin{block}{Vollständige Induktion} | |
| 935 Die \structure{vollständige Induktion} ist eine Beweistechnik, um zu zeigen, dass alle natürlichen Zahlen ein Prädikat $P$ erfüllen. | |
| 936 \[ \alert{\forall n \in \N_0. P(x)} \] | |
| 937 Ein solcher Beweis besteht aus | |
| 938 \begin{description}[Induktionsanfang\quad] | |
| 939 \item[Induktionsanfang] Man zeigt, dass $P(0)$ gilt. | |
| 940 \item[Induktionsschritt] Man zeigt für ein beliebiges $k$, dass\\ | |
| 941 wenn $P(k)$ gilt (\structure{Induktionshypothese}),\\ | |
| 942 dann auch $P(k+1)$. | |
| 943 \end{description} | |
| 944 Zusammen beweisen die Teile, dass das Prädikat für alle $n \in \N_0$ gilt.\\ | |
| 945 \vspace{1em} | |
| 946 In Prädikatenlogik formuliert gilt in $\N_0$ | |
| 947 \begin{align} | |
| 948 \structure{ P(0) \wedge \forall k . \left( P(k) \rightarrow P(k+1) \right)} &\rightarrow \alert{\forall n. P(n)} | |
| 949 \end{align} | |
| 950 \end{block} | |
| 951 | |
| 952 \vfill | |
| 953 | |
| 954 \begin{itemize} | |
| 955 \item Kann verallgemeinert werden, z.B. auf $\Z$ | |
| 956 \item Aber nicht auf $\R$ (Warum?) | |
| 957 \end{itemize} | |
| 958 \end{frame} | |
| 959 } |