\documentclass{article} \usepackage[german]{babel} \usepackage{times} \usepackage{amsmath} \usepackage{amssymb} \usepackage{z-eves} \abovedisplayskip 0pt \belowdisplayskip 0pt \zedindent 0pt %\input{prooftree} \parindent 0pt \parskip 1ex plus 0.3ex minus 0.3ex \textheight 24cm \textwidth 16cm \topmargin -2cm \leftmargin -1cm \advance\hsize by 2truecm\hoffset = -1.5truecm % PDF-LaTeX \makeatletter \@ifundefined{pdfvorigin}{}{\pdfvorigin 0pt\pdfhorigin 0pt} \makeatother \renewcommand{\arraystretch}{1.4} \newcommand{\limp}{\implies} \newcommand{\falsum}{\textit{false}} \newcommand{\verum}{\textit{true}} \newcommand{\zname}[1]{\ensuremath{\mathbf{#1}}} \newcommand{\deco}[1]{{\textrm{#1}}} \newcommand{\variable}[1]{{\frenchspacing\textit{#1}}} %\newcommand{\syntax}[1]{\texttt{\def\{{\char123}\def\}{\char125}\def\^{\char94}#1}} \newcommand{\meta}{\ensuremath} \newcommand{\bmeta}[1]{$\disregardspaces} \newcommand{\emeta}{\obeyspaces$} \newenvironment{cmds*}[4]{\par\noindent% \begin{tabular*}{\textwidth}{p{#1}@{\extracolsep{\fill}}p{#2}p{#3}} \hline \multicolumn{3}{|c|}{\textbf{#4}}\\ \hline \multicolumn{1}{|l}{\LaTeX{}-Eingabe} & Ausgabe & \multicolumn{1}{l|}{Erkl\"arung}\\ \hline}{\end{tabular*}} \newenvironment{cmds}[1]{\begin{cmds*}{5cm}{3cm}{7cm}{#1}}{\end{cmds*}} \sloppy \begin{document} \subsection*{Z-Notation} Die folgenden Tabellen geben einen "Uberblick "uber die in Z verwendeten Schreibweisen. Das \LaTeX{}-Eingabeformat wird auch von g"angigen Z-Werkzeugen, u.a. auch von Z/Eves und Jaza akzeptiert; f"ur die Formatierung mit \LaTeX{} wird \texttt{zed-csp.sty} (bzw. \texttt{z-eves.sty}) ben"otigt. Alle Eingaben m"ussen innerhalb einer \texttt{zed}-Umgebung stehen (d.h. innerhalb von \verb|\begin{zed}| \ldots \verb|\end{zed}|), ausgenommen "`boxes"' (axiomatische bzw. generische Definitionen oder Schemata), die selbst als Umgebung geschrieben werden. \bigskip \begin{cmds}{Deklarationen und Definitionen} \verb![Type]! & $[Type]$ & Grund-Typen\\ % \verb!id~params == expr! & $id~params == expr$ & Abk"urzung\\ % {\raggedright \verb!T ::= c |!\\ \verb! d \ldata U \rdata!} & $T ::= c | d \ldata U \rdata$ & Definition freier Typen\\ % {\raggedright \verb!\begin{axdef}!\\ \verb! x: T!\\ \verb!\where!\\ \verb! P!\\ \verb!\end{axdef}!} & \raisebox{3mm}{\parbox[t]{2.5cm}{ \begin{axdef} x: T\\ \where P \end{axdef}}} & axiomatische Definitionen\\ % {\raggedright \verb!\begin{gendef}[X]!\\ \verb! x: X!\\ \verb!\where!\\ \verb! P!\\ \verb!\end{gendef}!} & \raisebox{5mm}{\parbox[t]{2.5cm}{ \begin{gendef}[X] x: X \where P \end{gendef}}} & generische Definitionen\\ % {\raggedright \verb!\begin{schema}{S}!\\ \verb! x: T!\\ \verb!\where!\\ \verb! P!\\ \verb!\end{schema}!} & \raisebox{5mm}{\parbox[t]{2.5cm}{ \begin{schema}{S} x: T \where P \end{schema}}} & Schema-Definition\\ % \verb!S \defs [x:T | P]! & $S \defs [x:T | P]$ & Schema-Definition in "`horizontaler"' Schreibweise \end{cmds} \bigskip \begin{cmds}{Schema-Ausdr"ucke} \verb!Id'!, \verb|Id!|, \verb|Id?|, \verb|Id_n| & $Id'$, $Id!$, $Id?$, $Id_n$ & Dekorationen ($n$ Ziffer)\\ % \verb!\Delta S! & $\Delta S$ & Abk"urzung f"ur $S \land S'$\\ % \verb!\Xi S! & $\Xi S$ & Abk"urzung f"ur $S \land S' \land \theta S = \theta S'$\\ % {\raggedright\verb!\lnot S!,\ \ \verb!S \land T!,\\ \verb!S \lor T!} & {\raggedright$\lnot S$,\ \ $S \land T$,\\ $S \lor T$} & logische Verkn"upfungen von Schemata\\ % {\raggedright\verb!\forall x:T @ S!\\ \verb!\exists x:T @ S!} & {\raggedright$\forall x:T @ S$\\$\exists x:T @ S$} & Quantoren (auch $\exists_1$ erlaubt)\\ % \verb!S \hide (x)! & $S \hide (x)$ & Hiding, "aquivalent zu $\exists x:T @ S$, wobei $T$ der Typ von $x$ in $S$\\ % \verb!S \project T! & $S \project T$ & Projektion, "aquivalent zu $(S \land T) \hide (\vec{x})$, wobei $\vec{x}$ die Variablen in $S$ sind, die in $T$ \emph{nicht} vorkommen\\ % \verb!S \semi T! & $S \semi T$ & sequentielle Komposition\\ % \verb!S \pipe T! & $S \pipe T$ & Pipe-Komposition\\% (Ausgaben von $S$ werden Eingaben von $T$)\\ % \verb!\pre S! & $\pre S$ & Vorbedingung (Hiding der gestrichenen und Ausgabe-Variablen) \end{cmds} \bigskip \begin{cmds}{Ausdr"ucke} \verb!\{ x:T | P @ E \}! & $\{ x:T | P @ E \}$ & {\raggedright Mengenkomprehension ($E$ optional), z.B.\\ $\{ x:\num | x>5 @ x*x \} = \{36,49,64,\ldots\}$} \\ \verb!(\lambda x:T | P @ E)! & $(\lambda x:T | P @ E)$ & $\lambda$-Ausdruck, "aquivalent zu $\{x:T | P @ (x,E)\}$ \\ \verb!f~x! & $f~x$ & Funktionsanwendung \\ \verb!(\mu x:T | P @ E)! & $(\mu x:T | P @ E)$ & {\raggedright eindeutige Beschreibung ($E$ optional), z.B.\\ $(\mu x:\nat_1 | x*x=x @ x+x) = 2$} \\ \verb!\IF P \THEN E1 \ELSE E2! & $\IF P \THEN E1 \ELSE E2$ & bedingter Ausdruck (analog f"ur Formeln) \\ \verb!\LET x==E1 @ E2! & $\LET x==E1 @ E2$ & lokale Definition (analog f"ur Formeln) \end{cmds} \bigskip \begin{cmds}{Formeln} \verb!x = y!,\ \ \verb!x \neq y! & $x=y$,\ \ $x \neq y$ & (Un-)Gleichheit \\ \verb!x \in S!,\ \ \verb!x \notin S! & $x \in S$,\ \ $x \notin S$ & (Nicht-)Enthaltensein \\ \verb!S \subseteq T! & $S \subseteq T$ & Teilmenge \\ \verb!S \subset T! & $S \subset T$ & echte Teilmenge \\ \verb!\lnot P! & $\lnot P$ & Negation \\ \verb!P \land Q! & $P \land Q$ & Konjunktion \\ \verb!P \lor Q! & $P \lor Q$ & Disjunktion \\ \verb!P \implies Q! & $P \implies Q$ & Implikation \\ \verb!P \iff Q! & $P \iff Q$ & "Aquivalenz \\ \verb!\forall x:T @ P! & $\forall x:T @ P$ & Allquantifizierung \\ \verb!\exists x:T @ P! & $\exists x:T @ P$ & Existenzquantifizierung \\ \verb!\exists_1 x:T @ P! & $\exists_1 x:T @ P$ & eindeutige Existenz \\ \verb!a \inrel{R} b! & $a \inrel{R} b$ & Infix-Relation, "aquivalent zu $(a,b) \in R$ \end{cmds} \bigskip \begin{cmds}{Mengen} \verb!\emptyset! & $\emptyset$ & leere Menge \\ \verb!\{a, b\}! & $\{a,b\}$ & Aufz"ahlung endlicher Mengen \\ \verb!S \cup T!,\ \ \verb!S \cap T! & $S \cup T$,\ \ $S \cap T$ & Vereinigung, Durchschnitt \\ \verb!S \setminus T! & $S \setminus T$ & Mengendifferenz \\ \verb!\power S!,\ \ \verb!\power_1 S! & $\power S$,\ \ $\power_1 S$ & Potenzmenge ($\power_1 S = \power S \setminus \emptyset$) \\ \verb!S \cross T! & $S \cross T$ & Mengenprodukt \\ \verb!\bigcup TT! & $\bigcup TT$ & {\raggedright verallgemeinerte Vereinigung,\\ $a \in \bigcup TT \iff \exists S \in TT @ a \in S$} \\ \verb!\bigcap TT! & $\bigcap TT$ & {\raggedright verallgemeinerter Durchschnitt,\\ $a \in \bigcap TT \iff \forall S \in TT @ a \in S$} \end{cmds} \bigskip \begin{cmds*}{4cm}{2cm}{9cm}{Paare und Tupel} \verb!(a, b)! & $(a,b)$ & Paar- und Tupelbildung (beliebige Stelligkeit) \\ \verb!a \mapsto b! & $a \mapsto b$ & geordnetes Paar ("`maplet"'), "aquivalent zu $(a,b)$ \\ \verb!t.n! & $t.n$ & Selektion der $n$-ten Komponente, z.B. $(a,b,c).2 = b$ \\ \verb!first~p! & $first~p$ & erste Komponente, $first (a,b) = a$ ("aquivalent zu $p.1$) \\ \verb!second~p! & $second~p$ & zweite Komponente, $second (a,b) = b$ ("aquivalent zu $p.2$) \end{cmds*} \bigskip \begin{cmds*}{4cm}{2cm}{9cm}{Relationen} \verb!X \rel Y! & $X \rel Y$ & Menge der Relationen, $X \rel Y = \power(X \times Y)$ \\ \verb!\dom R! & $\dom R$ & Vorbereich, $\dom R = \{~ x : X; y : Y | x \inrel{R} y @ x ~\}$ \\ \verb!\ran R! & $\ran R$ & Nachbereich, $\ran R = \{~ x : X; y : Y | x \inrel{R} y @ y ~\}$ \\ \verb!\id X! & $\id X$ & Identit"atsrelation, $\id X = (\lambda x:X @ x)$ \\ \verb!Q \comp R! & $Q \comp R$ & {\raggedright Relationskomposition,\\ $Q \comp R = \{~x:X; z:Z | (\exists y:Y @ x \inrel{Q} y \land y \inrel{R} z) @ x \mapsto z~\}$} \\ \verb!R \circ Q! & $R \circ Q$ & R"uckw"artskomposition, $R \circ Q = Q \comp R$, $(f \circ g)~x = f(g~x)$ \\ \verb!R \inv! & $R \inv$ & Umkehr-Relation, $R\inv = \{~ x : X; y : Y | x \inrel{R} y @ y \mapsto x ~\}$ \\ \verb!A \dres R! & $A \dres R$ & {\raggedright Vorbereichs-Restriktion,\\ $A \dres R = \{~ x : X; y : Y | x \inrel{R} y \land x \in A @ x \mapsto y ~\}$} \\ \verb!A \ndres R! & $A \ndres R$ & {\raggedright Vorbereichs-Antirestriktion,\\ $A \ndres R = \{~ x : X; y : Y | x \inrel{R} y \land x \notin A @ x \mapsto y ~\}$} \\ \verb!A \rres R! & $A \rres R$ & {\raggedright Nachbereichs-Restriktion,\\ $A \rres R = \{~ x : X; y : Y | x \inrel{R} y \land y \in B @ x \mapsto y ~\}$} \\ \verb!A \nrres R! & $A \nrres R$ & {\raggedright Nachbereichs-Antirestriktion,\\ $A \nrres R = \{~ x : X; y : Y | x \inrel{R} y \land y \notin B @ x \mapsto y ~\}$} \\ \verb!R \limg A \rimg! & $R \limg A \rimg$ & relationales Bild, $R\limg A \rimg = \ran(A \dres R)$ \\ \verb!Q \oplus R! & $Q \oplus R$ & "Uberschreiben, $Q \oplus R = (\dom R \ndres Q) \cup R$ \\ \verb!R \plus! & $R \plus$ & transitive H"ulle, $R \plus = \bigcap \{~Q: X \rel X | R \subseteq Q \land Q \comp Q \subseteq Q~\}$ \\ \verb!R \star! & $R \star$ & reflexiv-transitive H"ulle, $R \star = \id X \cup R \plus$ \\ \verb!R^{k}! & $R^{k}$ & Relationsiteration, $R^0 = \id X$, $R^{k+1} = R \comp R^k$, $R^{-k} = (R \inv)^k$ \end{cmds*} \begin{cmds*}{4cm}{2cm}{9cm}{Funktionen} \verb!X \pfun Y! & $X \pfun Y$ & {\raggedright partielle Funktionen,\\ $\{~R : X \rel Y | \forall x:X; y_1,y_2:Y @ x \inrel{R} y_1 \land x \inrel{R} y_2 \implies y_1=y_2~\}$} \\ \verb!X \fun Y! & $X \fun Y$ & totale Funktionen, $X \fun Y = \{~ f : X \pfun Y | \dom f = X \}$ \\ \verb!X \pinj Y! & $X \pinj Y$ & {\raggedright partielle Injektionen,\\ $\{~ f : X \pfun Y | \forall x_1, x_2 : \dom f @ f~x_1 = f~x_2 \implies x_1 = x_2 ~\}$} \\ \verb!X \inj Y! & $X \inj Y$ & totale Injektionen, $X \inj Y = (X \fun Y) \cap (X \pinj Y)$ \\ \verb!X \psurj Y! & $X \psurj Y$ & partielle Surjektionen, $X \psurj Y = \{~ f : X \pfun Y | \ran f = B ~\}$ \\ \verb!X \surj Y! & $X \surj Y$ & totale Surjektionen, $X \surj Y = (X \fun Y) \cap (X \psurj Y)$ \\ \verb!X \bij Y! & $X \bij Y$ & Bijektionen, $X \bij Y = (X \inj Y) \cap (X \surj Y)$ \end{cmds*} \bigskip \begin{cmds*}{4cm}{2cm}{9cm}{Zahlen} \verb!\num! & $\num$ & ganze Zahlen \\ \verb!\nat! & $\nat$ & nat"urliche Zahlen, $\nat = \{~n:\num | n \geq 0~\}$ \\ \verb!\nat_1! & $\nat_1$ & positive ganze Zahlen, $\nat_1 = \nat \setminus \{0\}$ \\ \verb!+!, \verb!-!, \verb!*! & $+$, $-$, $*$ & arithmetische Operationen ($\num \cross \num \fun \num$) \\ \verb!\div!, \verb!\mod! & $\div$, $\mod$ & Division, Modulo-Operation ($\num \cross (\num \setminus \{0\}) \fun \num$) \\ \verb! !, \verb!\geq! & $<$, $\leq$, $>$, $\geq$ & arithmetische Vergleiche ($\num \rel \num$) \\ \verb!succ! & $succ$ & Nachfolger-Operation ($\nat \fun \nat$) \\ \verb!a \upto b! & $a \upto b$ & Intervalle, $a \upto b = \{~n:\num | a \leq n \land n \leq b~\}$ \\ \verb!min~S!, \verb!max~S! & $min~S$, $max~S$ & {\raggedright minimales/maximales Element einer Zahlenmenge (falls ex.)\\ $min~S = (\mu m:S | (\forall n:S @ m \leq n))$} \end{cmds*} \bigskip \begin{cmds*}{4cm}{2cm}{9cm}{Endliche Mengen} \verb!\finset S! & $\finset S$ & {\raggedright Menge der endlichen Teilmengen von $S$,\\ $\finset S = \{~s:\power S | \exists n:\nat @ \exists f:1\upto n \fun S @ \ran f = S ~\}$} \\ \verb!\finset_1 S! & $\finset_1 S$ & nichtleere endliche Teilmengen, $\finset_1 S = \finset S \setminus \emptyset$ \\ \verb!\# S! & $\# S$ & {\raggedright Kardinalit"at einer endlichen Menge,\\ $\#S = (\mu n:\nat | (\exists f:1\upto n \inj S @ \ran f = S))$} \\ \verb!X \ffun Y! & $X \ffun Y$ & {\raggedright endliche partielle Funktionen,\\ $X \ffun Y = \{~ f : X \pfun Y | \dom f \in \finset X ~\}$} \\ \verb!X \finj Y! & $X \finj Y$ & endliche partielle Injektionen, $X \finj Y = (X \ffun Y) \cap (X \pinj Y)$ \end{cmds*} \bigskip \begin{cmds*}{4cm}{2cm}{9cm}{Multimengen} \verb!\bag S! & $\bag S$ & Multimengen "uber $S$, $\bag S = (S \pfun \nat_1)$ \\ \verb!\lbag a, a, b\rbag! & $\lbag a, a, b\rbag$ & Aufz"ahlung endlicher Multimengen, entspricht $\{ a \mapsto 2, b \mapsto 1 \}$ \\ \verb!B \bcount x! & $B \bcount x$ & H"aufigkeit von $x$ in $B$, $B \bcount x = (\lambda x:S @ 0) \oplus B$ \\ \verb!n \otimes B! & $n \otimes B$ & Skalierung, $n \otimes B = (\lambda x:\dom B @ x \mapsto n*(B~x))$ \\ \verb!x \inbag B! & $x \inbag B$ & Enthaltensein in Multimenge, $x \inbag B \iff x \in \dom B$ \\ \verb!A \subbageq B! & $A \subbageq B$ & Teil-Multimengenrelation, $A \subbageq B \iff \forall x:S @ A \bcount x \leq B \bcount x$ \\ \verb!A \uplus B! & $A \uplus B$ & Multimengen-Vereinigung, $(A \uplus B) \bcount x = A \bcount x + B \bcount x$ \\ \verb!A \uminus B! & $A \uminus B$ & Multimengen-Differenz, $(A \uminus B) \bcount x = max~\{0, A \bcount x - B \bcount x\}$ \\ \verb!items~s! & $items~s$ & Multimenge der Elemente einer Folge, $(items~s) \bcount x = \#(s \filter \{x\})$ \end{cmds*} \bigskip \begin{cmds*}{4cm}{2cm}{9cm}{Endliche Folgen} \verb!\seq S! & $\seq S$ & {\raggedright Menge der endlichen Folgen "uber $S$,\\ $\seq S = \{~ s : \nat \ffun S | \exists n : \nat @ \dom s = 1 \upto n ~\}$} \\ \verb!\seq_1 S! & $\seq_1 S$ & nichtleere Folgen, $\seq_1 S = \{~s:\seq S | \#s > 0~\}$ \\ \verb!\iseq S! & $\iseq S$ & dublettenfreie Folgen, $\iseq S = (\seq S) \cap (\nat \pinj S)$ \\ {\raggedright \verb!\langle a, a, b!\\ \verb! \rangle!} & $\langle a, a, b \rangle$ & {\raggedright Aufz"ahlung einer endlichen Folge, entspricht\\ $\{~ 1 \mapsto a, 2 \mapsto a, 3 \mapsto b ~\}$} \\ \verb!s \cat t! & $s \cat t$ & Konkatenation, $s \cat t = s \cup \{~ n:\dom t @ (n+\#s) \mapsto t(n)~\}$ \\ \verb!rev~s! & $rev~s$ & Umkehrung, $rev~s = (\lambda n:\dom s @ s(\#s-n+1))$ \\ \verb!head~s! & $head~s$ & erstes Element, $head~s = s(1)$ \\ \verb!tail~s! & $tail~s$ & Folgenrest, $tail~s = (\lambda n:1 \upto \#s-1 @ s(n+1))$ \\ \verb!last~s! & $last~s$ & letztes Element, $last~s = s(\#s)$ \\ \verb!front~s! & $front~s$ & Folge ohne letztes Element, $front~s = (1 \upto \#s-1) \dres s$ \\ \verb!squash~f! & $squash ~f$ & {\raggedright Kompaktifizierung,\\ $(\mu g : 1 \upto \#f \bij \dom f | g\inv \semi succ \semi g \subseteq (\_ < \_)) \semi f$} \\ \verb!A \extract s! & $A \extract s$ & Extraktion der Elemente an Indizes in $A$, $A \extract s = squash~(A \dres s)$ \\ \verb!s \filter A! & $s \filter A$ & {\raggedright Teilfolge der Elemente von $s$, die in $A$ enthalten sind,\\ $s \filter A = squash~(s \rres A)$} \\ \verb!s \prefix t! & $s \prefix t$ & Pr"afix-Relation, $s \prefix t \iff \exists v:\seq S @ s \cat v = t$ \\ \verb!s \suffix t! & $s \suffix t$ & Suffix-Relation, $s \suffix t \iff \exists v:\seq S @ v \cat s = t$ \\ \verb!s \inseq t! & $s \inseq t$ & Teilfolge, $s \inseq t \iff \exists u,v:\seq S @ u \cat s \cat v = t$ \\ \verb!\dcat s! & $\dcat s$ & {\raggedright Konkatenation aller Folgen in $s$,\\ $\dcat \langle \rangle = \langle \rangle$,\quad $\#s > 1 \implies \dcat s = (head~s) \cat (\dcat tail~s)$} \end{cmds*} \end{document} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Logik \subsection*{Pr"adikatenlogik 1. Stufe} \subsubsection*{Kalk"ul des nat"urlichen Schlie"sens} \begin{equation*} \begin{prooftree} p \quad q \justifies p \land q \using[\text{$\land$-intro}] \end{prooftree} \qquad \begin{prooftree} p \land q \justifies p \using[\text{$\land$-elim1}] \end{prooftree} \qquad \begin{prooftree} p \land q \justifies q \using[\text{$\land$-elim2}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} p \justifies p \lor q \using[\text{$\lor$-intro1}] \end{prooftree} \qquad \begin{prooftree} q \justifies p \lor q \using[\text{$\lor$-intro2}] \end{prooftree} \qquad \begin{prooftree} p \lor q \quad \[ \lceil p \rceil \leadsto r \] \quad \[ \lceil q \rceil \leadsto r \] \justifies r \using[\text{$\lor$-elim}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} \[ \lceil p \rceil \leadsto q \] \justifies p \limp q \using[\text{$\limp$-intro}] \end{prooftree} \qquad \begin{prooftree} p \limp q \quad p \justifies q \using[\text{$\limp$-elim}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} \[ \lceil p \rceil \leadsto \falsum \] \justifies \neg p \using[\text{$\neg$-intro}] \end{prooftree} \qquad \begin{prooftree} p \quad \neg p \justifies \falsum \using[\text{$\neg$-elim}] \end{prooftree} \qquad \begin{prooftree} \[ \lceil \neg p \rceil \leadsto \falsum \] \justifies p \using[\text{$\falsum$-elim}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} \[ \[ \lceil x \in a \rceil \proofdotnumber=0\leadsto \lceil p \rceil \] \leadsto q \] \justifies \forall x : a | p @ q \using[\text{$\forall$-intro}]\quad\text{\parbox{2.9cm}{$x$ nicht frei in\\ Annahmen f"ur $q$}} \end{prooftree} \qquad \begin{prooftree} t \in a \quad \forall x : a | p @ q \quad p[t/x] \justifies q[t/x] \using[\text{$\forall$-elim}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} x \in a \quad p \quad q \justifies \exists x : a | p @ q \using[\text{$\exists$-intro}] \end{prooftree} \qquad \begin{prooftree} \exists x : a | p @ q \quad \[ \lceil x \in a \land p \land q \rceil \leadsto r \] \justifies r \using[\text{$\exists$-elim}]\quad\text{\parbox{3.2cm}{$x$ nicht frei in den\\ Annahmen und $r$}} \end{prooftree} \end{equation*} \newpage \subsubsection*{Hilbertkalk"ul} \paragraph{Axiome} \begin{enumerate} \item Alle aussagenlogischen Tautologien. \item Alle Formeln der Form \[ (\forall v : T @ \varphi) \limp \varphi[t/v] \] falls $t$ frei f"ur $v$ in $\varphi$. \item Alle Formeln der Form \[ \varphi[t/v] \limp (\exists v : T @ \varphi) \] falls $t$ frei f"ur $v$ in $\varphi$. \end{enumerate} \paragraph{Schlu"sregeln} \begin{enumerate} \item $\begin{prooftree} \varphi \limp \psi \quad \varphi \justifies \psi \using[\text{Modus ponens}] \end{prooftree}$ \item $\begin{prooftree} \varphi \limp \psi[x/v] \justifies \varphi \limp \forall y : T @ \psi[y/v] \using\quad\text{$v$ nicht frei in $\varphi$} \end{prooftree}$ \item $\begin{prooftree} \psi[x/v] \limp \varphi \justifies \exists y : T @ \psi[y/v] \limp \varphi \using\quad\text{$v$ nicht frei in $\varphi$} \end{prooftree}$ \end{enumerate} \bigskip \subsection*{Gleichungslogik} \begin{equation*} \begin{prooftree} \justifies t = t \using[\text{eq-ref}] \end{prooftree} \qquad \begin{prooftree} s = t \quad p[t/x] \justifies p[s/x] \using[\text{eq-sub}] \end{prooftree} \end{equation*} \begin{gather*} t = t\\ s = t \limp t = s\\ s = t \land t = u \limp s = u\\ s_1 = t_1 \land \dots \land s_n = t_n \limp R(s_1, \dots, s_n) \limp R(t_1, \dots, t_n)\\ s_1 = t_1 \land \dots \land s_n = t_n \limp t(s_1, \dots, s_n) \limp t(t_1, \dots, t_n) \end{gather*} \newpage %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Mengenlehre \subsection*{Mengenlehre} \begin{equation*} \begin{prooftree} \justifies \forall x : a @ x \notin \emptyset \using[\text{empty}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} (\forall x : t @ x \in u) \land (\forall x : u @ x \in t) \justifies\thickness=0.08em t = u \using[\text{ext}]\quad\text{$x$ nicht frei in $u$ und $t$} \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} t = u_1 \lor \dots \lor t = u_n \justifies\thickness=0.08em t \in \{~ u_1, \dots, u_n ~\} \using[\text{ext-mem}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} \exists x : s | p @ e = f \justifies\thickness=0.08em f \in \{~ x : s | p @ e ~\} \using[\text{compre}]\quad\text{$x$ nicht frei in $f$} \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} \forall x : s @ x \in t \justifies\thickness=0.08em s \subseteq t \using[\text{subset}]\quad\text{$x$ nicht frei in $t$} \end{prooftree} \qquad \begin{prooftree} s \subseteq a \justifies\thickness=0.08em s \in \power a \using[\text{power}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} x_1 \in a_1 \land \dots \land x_n \in a_n \justifies\thickness=0.08em (x_1, \dots, x_n) \in a_1 \times \dots \times a_n \using[\text{cart-mem}] \end{prooftree} \qquad \begin{prooftree} x_1 = y_1 \land \dots \land x_n = y_n \justifies\thickness=0.08em (x_1, \dots, x_n) = (y_1, \dots, y_n) \using[\text{cart-eq}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} t.1 = x_1 \land \dots \land t.n = x_n \justifies\thickness=0.08em t = (x_1, \dots, x_n) \using[\text{cart-proj}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} x \in (a \cup b) \justifies\thickness=0.08em x \in a \lor x \in b \using[\text{union}] \end{prooftree} \qquad \begin{prooftree} x \in \bigcup s \justifies\thickness=0.08em \exists a : s @ x \in a \using[\text{Union}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} x \in (a \cap b) \justifies\thickness=0.08em x \in a \land x \in b \using[\text{inter}] \end{prooftree} \qquad \begin{prooftree} x \in \bigcap s \justifies\thickness=0.08em \forall a : s @ x \in a \using[\text{Inter}] \end{prooftree} \end{equation*} \begin{equation*} \begin{prooftree} x \in (a \setminus b) \justifies\thickness=0.08em x \in a \land x \notin b \using[\text{diff}] \end{prooftree} \end{equation*} \newpage