# HG changeset patch # User Markus Kaiser # Date 1397081434 -7200 # Node ID 8946d732625f9b13dbcc8481ed8271b295b73055 # Parent a78ea627829e5aeadbbb5d6d104767aba6020514 Use less dangerous command names diff -r a78ea627829e -r 8946d732625f notes/tex/logic.tex --- a/notes/tex/logic.tex Thu Apr 10 00:10:18 2014 +0200 +++ b/notes/tex/logic.tex Thu Apr 10 00:10:34 2014 +0200 @@ -208,32 +208,32 @@ \defineUnit{aussagenlogikaequivalenzen}{% { \newcommand{\spc}{\hfill} - \newcommand{\F}{F} - \newcommand{\G}{G} - \newcommand{\K}{H} + \newcommand{\VarF}{F} + \newcommand{\VarG}{G} + \newcommand{\VarK}{H} \begin{frame} \frametitle{Äquivalenzregeln} \begin{description}[Triviale Kontradiktion\quad] - \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$ - \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \false$ - \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$ - \item[Doppelte Negation] $\neg \neg \F \equiv \F$ - \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$ - \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$ + \item[Identität] $\VarF \wedge \true \equiv \VarF \spc \VarF \vee \false \equiv \VarF$ + \item[Dominanz] $\VarF \vee \true \equiv \true \spc \VarF \wedge \false \equiv \false$ + \item[Idempotenz] $\VarF \vee \VarF \equiv \VarF \spc \VarF \wedge \VarF \equiv \VarF$ + \item[Doppelte Negation] $\neg \neg \VarF \equiv \VarF$ + \item[Triviale Tautologie] $\VarF \vee \neg \VarF \equiv \true$ + \item[Triviale Kontradiktion] $\VarF \wedge \neg \VarF \equiv \false$ \bigskip - \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\ - $\F \wedge \G \equiv \G \wedge \F$ - \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\ - $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$ - \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\ - $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$ - \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\ - $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$ + \item[Kommutativität] $\VarF \vee \VarG \equiv \VarG \vee \VarF$\\ + $\VarF \wedge \VarG \equiv \VarG \wedge \VarF$ + \item[Assoziativität] $(\VarF \vee \VarG) \vee \VarK \equiv \VarF \vee (\VarG \vee \VarK)$\\ + $(\VarF \wedge \VarG) \wedge \VarK \equiv \VarF \wedge (\VarG \wedge \VarK)$ + \item[Distributivität] $\VarF \vee (\VarG \wedge \VarK) \equiv (\VarF \vee \VarG) \wedge (\VarF \vee \VarK)$\\ + $\VarF \wedge (\VarG \vee \VarK) \equiv (\VarF \wedge \VarG) \vee (\VarF \wedge \VarK)$ + \item[De Morgan] $\neg(\VarF \wedge \VarG) \equiv \neg \VarF \vee \neg \VarG$\\ + $\neg(\VarF \vee \VarG) \equiv \neg\VarF \wedge \neg\VarG$ \bigskip - \item[Implikation] $\F \rightarrow \G \equiv \neg \F \vee \G$ - \item[Bikonditional] $\F \leftrightarrow \G \equiv \neg(\F \otimes \G) \left[ \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \right]$ + \item[Implikation] $\VarF \rightarrow \VarG \equiv \neg \VarF \vee \VarG$ + \item[Bikonditional] $\VarF \leftrightarrow \VarG \equiv \neg(\VarF \otimes \VarG) \left[ \equiv (\VarF \rightarrow \VarG) \wedge (\VarG \rightarrow \VarF) \right]$ \end{description} \end{frame} @@ -242,24 +242,24 @@ %\vspace{-2em} %\begin{align} - %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\ - %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \false \tag{\structure{Dominanz}}\\ - %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\ - %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\ - %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\ - %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\ + %\VarF \wedge \true &\equiv \VarF \spc \VarF \vee \false \equiv \VarF \tag{\structure{Identität}}\\ + %\VarF \vee \true &\equiv \true \spc \VarF \wedge \false \equiv \false \tag{\structure{Dominanz}}\\ + %\VarF \vee \VarF &\equiv \VarF \spc \VarF \wedge \VarF \equiv \VarF \tag{\structure{Idempotenz}}\\ + %\neg \neg \VarF &\equiv \VarF \tag{\structure{Doppelte Negation}}\\ + %\VarF \vee \neg \VarF &\equiv \true \tag{\structure{Triviale Tautologie}}\\ + %\VarF \wedge \neg \VarF &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\ %\bigskip - %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\ - %\F \wedge \G &\equiv \G \wedge \F\\ - %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\ - %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\ - %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\ - %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\ - %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\ - %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\ + %\VarF \vee \VarG &\equiv \VarG \vee \VarF \tag{\structure{Kommutativität}}\\ + %\VarF \wedge \VarG &\equiv \VarG \wedge \VarF\\ + %(\VarF \vee \VarG) \vee \VarK &\equiv \VarF \vee (\VarG \vee \VarK) \tag{\structure{Assoziativität}}\\ + %(\VarF \wedge \VarG) \wedge \VarK &\equiv \VarF \wedge (\VarG \wedge \VarK)\\ + %\VarF \vee (\VarG \wedge \VarK) &\equiv (\VarF \vee \VarG) \wedge (\VarF \vee \VarK) \tag{\structure{Distributivität}}\\ + %\VarF \wedge (\VarG \vee \VarK) &\equiv (\VarF \wedge \VarG) \vee (\VarF \wedge \VarK)\\ + %\neg(\VarF \wedge \VarG) &\equiv \neg \VarF \vee \neg \VarG \tag{\structure{De Morgan}}\\ + %\neg(\VarF \vee \VarG) &\equiv \neg\VarF \wedge \neg\VarG\\ %\bigskip - %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\ - %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\ + %\VarF \rightarrow \VarG &\equiv \neg \VarF \vee \VarG \tag{\structure{Implikation}}\\ + %\VarF \leftrightarrow \VarG &\equiv (\VarF \rightarrow \VarG) \wedge (\VarG \rightarrow \VarF) \tag{\structure{Bikonditional}}\\ %\end{align} %\end{frame} } @@ -568,9 +568,9 @@ \defineUnit{natuerlichesschliessen}{% { - \newcommand{\F}{\tau} - \newcommand{\G}{\varphi} - \newcommand{\K}{\chi} + \newcommand{\VarF}{\tau} + \newcommand{\VarG}{\varphi} + \newcommand{\VarK}{\chi} \newcommand{\subproof}[2]{% \begin{tikzpicture}[y=.9em] \path @@ -595,69 +595,69 @@ & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} \capt{$\wedge$} & \topproof{ - \AxiomC{$\F$} - \AxiomC{$\G$} + \AxiomC{$\VarF$} + \AxiomC{$\VarG$} \RightLabel{\scriptsize $+\wedge$} - \BinaryInfC{$\F \wedge \G$} + \BinaryInfC{$\VarF \wedge \VarG$} } & \topproof{ - \AxiomC{$\F \wedge \G$} + \AxiomC{$\VarF \wedge \VarG$} \RightLabel{\scriptsize $-\wedge_1$} - \UnaryInfC{$\F$} + \UnaryInfC{$\VarF$} } \quad \topproof{ - \AxiomC{$\F \wedge \G$} + \AxiomC{$\VarF \wedge \VarG$} \RightLabel{\scriptsize $-\wedge_2$} - \UnaryInfC{$\G$} + \UnaryInfC{$\VarG$} } \\ \capt{$\vee$} & \topproof{ - \AxiomC{$\F$} + \AxiomC{$\VarF$} \RightLabel{\scriptsize $+\vee_1$} - \UnaryInfC{$\F \vee \G$} + \UnaryInfC{$\VarF \vee \VarG$} } \quad \topproof{ - \AxiomC{$\G$} + \AxiomC{$\VarG$} \RightLabel{\scriptsize $+\vee_2$} - \UnaryInfC{$\F \vee \G$} + \UnaryInfC{$\VarF \vee \VarG$} } & \topproof{ - \AxiomC{$\F \vee \G$} - \AxiomC{\subproof{$\F$}{$\K$}} - \AxiomC{\subproof{$\G$}{$\K$}} + \AxiomC{$\VarF \vee \VarG$} + \AxiomC{\subproof{$\VarF$}{$\VarK$}} + \AxiomC{\subproof{$\VarG$}{$\VarK$}} \RightLabel{\scriptsize $-\vee$} - \TrinaryInfC{$\K$\vphantom{$\F\G$}} + \TrinaryInfC{$\VarK$\vphantom{$\VarF\VarG$}} } \\ \capt{$\rightarrow$} & \topproof{ - \AxiomC{\subproof{$\F$}{$\G$}} + \AxiomC{\subproof{$\VarF$}{$\VarG$}} \RightLabel{\scriptsize $+\rightarrow$} - \UnaryInfC{$\F \rightarrow \G$} + \UnaryInfC{$\VarF \rightarrow \VarG$} } & \topproof{ - \AxiomC{$\F$} - \AxiomC{$\F \rightarrow \G$} + \AxiomC{$\VarF$} + \AxiomC{$\VarF \rightarrow \VarG$} \RightLabel{\scriptsize $-\rightarrow$, MP} - \BinaryInfC{$\G$} + \BinaryInfC{$\VarG$} } \\ \capt{$\neg$} & \topproof{ - \AxiomC{\subproof{$\F$}{$\bot$}} + \AxiomC{\subproof{$\VarF$}{$\bot$}} \RightLabel{\scriptsize $+\neg$} - \UnaryInfC{$\neg \F$} + \UnaryInfC{$\neg \VarF$} } & \topproof{ - \AxiomC{$\F$} - \AxiomC{$\neg\F$} + \AxiomC{$\VarF$} + \AxiomC{$\neg\VarF$} \RightLabel{\scriptsize $-\neg$} \BinaryInfC{$\bot$} } @@ -675,20 +675,20 @@ \topproof{ \AxiomC{$\bot$} \RightLabel{\scriptsize $-\bot$} - \UnaryInfC{$\F$} + \UnaryInfC{$\VarF$} } \\ \capt{$\neg\neg$} & \topproof{ - \AxiomC{$\F$} + \AxiomC{$\VarF$} \RightLabel{\scriptsize $+\neg\neg$} - \UnaryInfC{$\neg\neg\F$} + \UnaryInfC{$\neg\neg\VarF$} } & \topproof{ - \AxiomC{$\neg\neg\F$} + \AxiomC{$\neg\neg\VarF$} \RightLabel{\scriptsize $-\neg\neg$} - \UnaryInfC{$\F$} + \UnaryInfC{$\VarF$} } \end{tabu} \begin{itemize} @@ -701,22 +701,22 @@ \topproof{ \AxiomC{ } \RightLabel{\scriptsize LEM} - \UnaryInfC{$\F \vee \neg\F$} + \UnaryInfC{$\VarF \vee \neg\VarF$} } & \topproof{ - \AxiomC{\subproof{$\neg\F$}{$\bot$}} + \AxiomC{\subproof{$\neg\VarF$}{$\bot$}} \RightLabel{\scriptsize $-\neg$, PBC} - \UnaryInfC{$\F$} + \UnaryInfC{$\VarF$} } \\ & & \topproof{ - \AxiomC{$\neg\G$} - \AxiomC{$\F \rightarrow \G$} + \AxiomC{$\neg\VarG$} + \AxiomC{$\VarF \rightarrow \VarG$} \RightLabel{\scriptsize MT} - \BinaryInfC{$\neg\F$} + \BinaryInfC{$\neg\VarF$} } \end{tabu} \end{frame} @@ -833,9 +833,9 @@ \defineUnit{natuerlichesschliessenquantoren}{% { - \newcommand{\F}{\tau} - \newcommand{\G}{\varphi} - \newcommand{\K}{\chi} + \newcommand{\VarF}{\tau} + \newcommand{\VarG}{\varphi} + \newcommand{\VarK}{\chi} \newcommand{\subproof}[2]{% \begin{tikzpicture}[y=.9em] \path @@ -856,8 +856,8 @@ \frametitle{Natürliches Schließen} \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}. + Sei $\VarG$ eine Formel und $a$ eine Konstante.\\ + Mit \structure{$\VarG[x/a]$} bezeichnen wir die Formel die man erhält, wenn man alle \alert{freien} Vorkommnisse von \structure{$x$} in \structure{$\VarG$} durch \structure{$a$} \structure{ersetzt}. \end{definition} \vfill \tabulinesep=4pt @@ -865,29 +865,29 @@ & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} \capt{$\exists$} & \topproof{ - \AxiomC{$\F[x/a]$} + \AxiomC{$\VarF[x/a]$} \RightLabel{\scriptsize $+\exists$} - \UnaryInfC{$\exists x. \F$} + \UnaryInfC{$\exists x. \VarF$} } & \topproof{ - \AxiomC{$\exists x. \F$} - \AxiomC{\subproof{$a. \F[x/a]$}{$\K$}} + \AxiomC{$\exists x. \VarF$} + \AxiomC{\subproof{$a. \VarF[x/a]$}{$\VarK$}} \RightLabel{\scriptsize $-\exists$} - \BinaryInfC{$\K$} + \BinaryInfC{$\VarK$} } \\ \capt{$\forall$} & \topproof{ - \AxiomC{\subproof{$a$}{$\F[x/a]$}} + \AxiomC{\subproof{$a$}{$\VarF[x/a]$}} \RightLabel{\scriptsize $+\forall$} - \UnaryInfC{$\forall x. \F$} + \UnaryInfC{$\forall x. \VarF$} } & \topproof{ - \AxiomC{$\forall x. \F$} + \AxiomC{$\forall x. \VarF$} \RightLabel{\scriptsize $-\forall$} - \UnaryInfC{$\F[x/a]$} + \UnaryInfC{$\VarF[x/a]$} } \end{tabu} \begin{itemize}