Mercurial > 13ws.ds
comparison notes/tex/logic.tex @ 32:b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
| author | Markus Kaiser <markus.kaiser@in.tum.de> |
|---|---|
| date | Mon, 02 Dec 2013 23:35:26 +0100 |
| parents | f639b478a28b |
| children | 010d8f7fa899 |
comparison
equal
deleted
inserted
replaced
| 31:cedc6884dd46 | 32:b5094b3e3111 |
|---|---|
| 181 | 181 |
| 182 \begin{example}[] | 182 \begin{example}[] |
| 183 Für $F \defeq a \rightarrow b$ und $G \defeq \neg a \vee b$ gilt $F \equiv G$. | 183 Für $F \defeq a \rightarrow b$ und $G \defeq \neg a \vee b$ gilt $F \equiv G$. |
| 184 \begin{center} | 184 \begin{center} |
| 185 \begin{tabu} to .4\textwidth {cc|[1.2pt]XcX||Xccc} | 185 \begin{tabu} to .4\textwidth {cc|[1.2pt]XcX||Xccc} |
| 186 a & b & & $a \Rightarrow b$ & & & $\neg a$ & $\vee$ & $b$ \\ \tabucline[1.2pt]{-} | 186 a & b & & $a \rightarrow b$ & & & $\neg a$ & $\vee$ & $b$ \\ \tabucline[1.2pt]{-} |
| 187 0 & 0 & & \structure{1} & & & 1 & \structure{1} \\ | 187 0 & 0 & & \structure{1} & & & 1 & \structure{1} \\ |
| 188 0 & 1 & & \structure{1} & & & 1 & \structure{1} \\ | 188 0 & 1 & & \structure{1} & & & 1 & \structure{1} \\ |
| 189 1 & 0 & & \structure{0} & & & 0 & \structure{0} \\ | 189 1 & 0 & & \structure{0} & & & 0 & \structure{0} \\ |
| 190 1 & 1 & & \structure{1} & & & 0 & \structure{1} \\ | 190 1 & 1 & & \structure{1} & & & 0 & \structure{1} \\ |
| 191 \end{tabu} | 191 \end{tabu} |
| 538 \end{algorithmic} | 538 \end{algorithmic} |
| 539 \end{block} | 539 \end{block} |
| 540 \end{frame} | 540 \end{frame} |
| 541 } | 541 } |
| 542 | 542 |
| 543 \defineUnit{natuerlichesschliessen}{% | 543 \defineUnit{kalkuele}{% |
| 544 \begin{frame} | 544 \begin{frame} |
| 545 \frametitle{Kalküle} | 545 \frametitle{Kalküle} |
| 546 \setbeamercovered{dynamic} | 546 \setbeamercovered{dynamic} |
| 547 | 547 |
| 548 \begin{definition}[Kalkül] | 548 \begin{definition}[Kalkül] |
| 583 \item Arithmetik | 583 \item Arithmetik |
| 584 \end{itemize} | 584 \end{itemize} |
| 585 \item Deshalb sind nicht alle Sätze der Mathematik beweisbar | 585 \item Deshalb sind nicht alle Sätze der Mathematik beweisbar |
| 586 \end{itemize} | 586 \end{itemize} |
| 587 \end{frame} | 587 \end{frame} |
| 588 | 588 } |
| 589 | |
| 590 \defineUnit{natuerlichesschliessen}{% | |
| 589 { | 591 { |
| 590 \newcommand{\F}{\tau} | 592 \newcommand{\F}{\tau} |
| 591 \newcommand{\G}{\varphi} | 593 \newcommand{\G}{\varphi} |
| 592 \newcommand{\K}{\chi} | 594 \newcommand{\K}{\chi} |
| 593 \newcommand{\subproof}[2]{% | 595 \newcommand{\subproof}[2]{% |
| 602 \newcommand{\topproof}[1]{% | 604 \newcommand{\topproof}[1]{% |
| 603 ##1 | 605 ##1 |
| 604 \bottomAlignProof | 606 \bottomAlignProof |
| 605 \DisplayProof | 607 \DisplayProof |
| 606 } | 608 } |
| 609 \newcommand{\capt}[1]{\vspace{-1em}##1} | |
| 607 | 610 |
| 608 \begin{frame} | 611 \begin{frame} |
| 609 \frametitle{Natürliches Schließen} | 612 \frametitle{Natürliches Schließen} |
| 610 \setbeamercovered{dynamic} | 613 \setbeamercovered{dynamic} |
| 611 | 614 |
| 612 \vspace{-4pt} | |
| 613 \tabulinesep=4pt | 615 \tabulinesep=4pt |
| 614 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]} | 616 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]} |
| 615 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} | 617 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} |
| 616 $\wedge$ & | 618 \capt{$\wedge$} & |
| 617 \topproof{ | 619 \topproof{ |
| 618 \AxiomC{$\F$} | 620 \AxiomC{$\F$} |
| 619 \AxiomC{$\G$} | 621 \AxiomC{$\G$} |
| 620 \RightLabel{\scriptsize $+\wedge$} | 622 \RightLabel{\scriptsize $+\wedge$} |
| 621 \BinaryInfC{$\F \wedge \G$} | 623 \BinaryInfC{$\F \wedge \G$} |
| 631 \AxiomC{$\F \wedge \G$} | 633 \AxiomC{$\F \wedge \G$} |
| 632 \RightLabel{\scriptsize $-\wedge_2$} | 634 \RightLabel{\scriptsize $-\wedge_2$} |
| 633 \UnaryInfC{$\G$} | 635 \UnaryInfC{$\G$} |
| 634 } | 636 } |
| 635 \\ | 637 \\ |
| 636 $\vee$ & | 638 \capt{$\vee$} & |
| 637 \topproof{ | 639 \topproof{ |
| 638 \AxiomC{$\F$} | 640 \AxiomC{$\F$} |
| 639 \RightLabel{\scriptsize $+\vee_1$} | 641 \RightLabel{\scriptsize $+\vee_1$} |
| 640 \UnaryInfC{$\F \vee \G$} | 642 \UnaryInfC{$\F \vee \G$} |
| 641 } | 643 } |
| 652 \AxiomC{\subproof{$\G$}{$\K$}} | 654 \AxiomC{\subproof{$\G$}{$\K$}} |
| 653 \RightLabel{\scriptsize $-\vee$} | 655 \RightLabel{\scriptsize $-\vee$} |
| 654 \TrinaryInfC{$\K$\vphantom{$\F\G$}} | 656 \TrinaryInfC{$\K$\vphantom{$\F\G$}} |
| 655 } | 657 } |
| 656 \\ | 658 \\ |
| 657 $\rightarrow$ & | 659 \capt{$\rightarrow$} & |
| 658 \topproof{ | 660 \topproof{ |
| 659 \AxiomC{\subproof{$\F$}{$\G$}} | 661 \AxiomC{\subproof{$\F$}{$\G$}} |
| 660 \RightLabel{\scriptsize $+\rightarrow$} | 662 \RightLabel{\scriptsize $+\rightarrow$} |
| 661 \UnaryInfC{$\F \rightarrow \G$} | 663 \UnaryInfC{$\F \rightarrow \G$} |
| 662 } | 664 } |
| 666 \AxiomC{$\F \rightarrow \G$} | 668 \AxiomC{$\F \rightarrow \G$} |
| 667 \RightLabel{\scriptsize $-\rightarrow$, MP} | 669 \RightLabel{\scriptsize $-\rightarrow$, MP} |
| 668 \BinaryInfC{$\G$} | 670 \BinaryInfC{$\G$} |
| 669 } | 671 } |
| 670 \\ | 672 \\ |
| 671 $\neg$ & | 673 \capt{$\neg$} & |
| 672 \topproof{ | 674 \topproof{ |
| 673 \AxiomC{\subproof{$\F$}{$\bot$}} | 675 \AxiomC{\subproof{$\F$}{$\bot$}} |
| 674 \RightLabel{\scriptsize $+\neg$} | 676 \RightLabel{\scriptsize $+\neg$} |
| 675 \UnaryInfC{$\neg \F$} | 677 \UnaryInfC{$\neg \F$} |
| 676 } | 678 } |
| 686 | 688 |
| 687 \begin{frame} | 689 \begin{frame} |
| 688 \frametitle{Natürliches Schließen} | 690 \frametitle{Natürliches Schließen} |
| 689 \setbeamercovered{dynamic} | 691 \setbeamercovered{dynamic} |
| 690 | 692 |
| 691 \vspace{-4pt} | |
| 692 \tabulinesep=4pt | 693 \tabulinesep=4pt |
| 693 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]} | 694 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]} |
| 694 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} | 695 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} |
| 695 $\bot$ & | 696 \capt{$\bot$} & |
| 696 & | 697 & |
| 697 \topproof{ | 698 \topproof{ |
| 698 \AxiomC{$\bot$} | 699 \AxiomC{$\bot$} |
| 699 \RightLabel{\scriptsize $-\bot$} | 700 \RightLabel{\scriptsize $-\bot$} |
| 700 \UnaryInfC{$\F$} | 701 \UnaryInfC{$\F$} |
| 701 } | 702 } |
| 702 \\ | 703 \\ |
| 703 $\neg\neg$ & | 704 \capt{$\neg\neg$} & |
| 704 \topproof{ | 705 \topproof{ |
| 705 \AxiomC{$\F$} | 706 \AxiomC{$\F$} |
| 706 \RightLabel{\scriptsize $+\neg\neg$} | 707 \RightLabel{\scriptsize $+\neg\neg$} |
| 707 \UnaryInfC{$\neg\neg\F$} | 708 \UnaryInfC{$\neg\neg\F$} |
| 708 } | 709 } |