forallx-do-quickreference.tex

%!TEX root = forallxdo.tex

\chapter{Schnellüberblick}
%\pagestyle{plain}
\section{Charakteristische Wahrheitstabellen}
\label{app.CharacteristicTTs}

\begin{tabular}{c|c}
\metav{A} & \enot\metav{A}\\
\hline
T & F\\
F & T \\
\phantom{.}\\
\phantom{.}
\end{tabular}
\hfill
\begin{tabular}{c c|c|c|c|c}
\metav{A} & \metav{B} & $\metav{A}\eand\metav{B}$ & $\metav{A}\eor\metav{B}$ & $\metav{A}\eif\metav{B}$ & $\metav{A}\eiff\metav{B}$\\
\hline
T & T & T & T & T & T\\
T & F & F & T & F & F\\
F & T & F & T & T & F\\
F & F & F & F & T & T
\end{tabular}


\vfill

\section{Symbolisierungen}
\begin{center}
\label{app.symbolization}
\begin{tabular*}{\textwidth}{rl}
\multicolumn{2}{c}{\textsc{Junktoren}}\\ \\
Es ist nicht der Fall, dass $P$ & $\enot P$\\
(Entweder) $P$ oder $Q$ & $(P \eor Q)$\\
Weder $P$ noch $Q$ & $\enot(P \eor Q)$\ oder \ $(\enot P \eand \enot Q)$\\
$P$ und $Q$ & $(P \eand Q)$\\
Wenn $P$, dann $Q$ & $(P \eif Q)$\\
$P$ nur wenn $Q$ & $(P \eif Q)$\\
$P$ genau dann, wenn $Q$ & $(P \eiff Q)$\\
$P$, es sei denn, $Q$ & $(P \eor Q)$\\
\\
\multicolumn{2}{c}{\label{SymbolizingPredicates}\textsc{Prädikate}}\\ \\
Alle $F$s sind $G$s & $\forall x(\atom{F}{x} \eif \atom{G}{x})$\\
Manche $F$s sind $G$s & $\exists x(\atom{F}{x} \eand \atom{G}{x})$\\
Nicht alle $F$s sind $G$s & $\enot\forall x(\atom{F}{x} \eif \atom{G}{x})$\ oder\\
& $\exists x(\atom{F}{x} \eand \enot \atom{G}{x})$\\
Keine $F$s sind $G$s & $\forall x(\atom{F}{x} \eif\enot \atom{G}{x})$\ oder\\
& $\enot\exists x(\atom{F}{x} \eand \atom{G}{x})$\\
\\
\multicolumn{2}{c}{\textsc{Identität}}\\ \\
Nur $c$ ist $G$ & $\forall x(\atom{G}{x} \eiff x=c)$\\
Alle/s au{\ss}er $c$ ist $G$ & $\forall x(\enot x = c \eiff \atom{G}{x} )$\\
Niemand au{\ss}er $c$ ist $G$ & $\enot\exists x(\enot x = c \eand \atom{G}{x})$\ oder\\
& $\forall x (\atom{S}{x,h} \eif x = p)$ \\
Der/das/die $F$ ist $G$ & $\exists x(\atom{F}{x} \eand \forall y(\atom{F}{y} \eif x=y) \eand \atom{G}{x} )$\\
Es ist nicht der Fall, dass\\
 der/das/die $F$ $G$ ist & $\enot\exists x(\atom{F}{x} \eand \forall y(\atom{F}{y} \eif x=y) \eand \atom{G}{x} )$\\
Der/das/die $F$ ist kein $G$ & $\exists x(\atom{F}{x} \eand \forall y(\atom{F}{y} \eif x=y) \eand \enot \atom{G}{x} )$
\end{tabular*}
\end{center}

\newpage
\section{Identität nutzen um Quantitäten zu symbolisieren}

\subsection*{Es gibt zumindest \blank\ $F$s.}
\label{summary.atleast}

\begin{tabular*}{\textwidth}{rl}
ein & $\exists x\,\atom{F}{x}$\\
zwei & $\exists x_1\exists x_2(\atom{F}{x_1} \eand \atom{F}{x_2} \eand \enot x_1  = x_2)$\\
drei & $\exists x_1\exists x_2\exists x_3(\atom{F}{x_1} \eand \atom{F}{x_2} \eand \atom{F}{x_3} \eand {}$\\
& $\enot x_1 = x_2 \eand\enot x_1 = x_3 \eand \enot x_2 = x_3)$\\
vier & $\exists x_1\exists x_2\exists x_3\exists x_4 (\atom{F}{x_1} \eand \atom{F}{x_2} \eand \atom{F}{x_3} \eand \atom{F}{x_4} \eand {}$\\
& $\enot x_1 = x_2 \eand \enot x_1 = x_3 \eand \enot x_1 = x_4 \eand {}$\\
& $ \enot x_2 = x_3 \eand \enot x_2 = x_4 \eand \enot x_3 = x_4)$\\
$n$ & $\exists x_1\ldots\exists x_n(\atom{F}{x_1} \eand \ldots \eand \atom{F}{x_n} \eand {}$\\
& $\enot x_1 = x_2 \eand\ldots\eand \enot x_{n-1} = x_n)$ 
\end{tabular*}

\subsection*{Es gibt höchstens \blank\ $F$s.}
\label{summary.atmost}

Ein Weg `es gibt höchstens $n$ $F$s' zu symbolisieren ist eine Negation vor die Symbolisierung von `es gibt zumindest $n+1$ $F$s' zu stellen. Äquivalenterweise können wir auch anbieten:
\begin{tabular*}{\textwidth}{rl}
ein & $\forall x_1\forall x_2\bigl[(\atom{F}{x_1} \eand \atom{F}{x_2}) \eif x_1=x_2\bigr]$\\
zwei & $\forall x_1\forall x_2\forall x_3\bigl[(\atom{F}{x_1} \eand \atom{F}{x_2} \eand \atom{F}{x_3}) \eif {}$\\ & $(x_1=x_2 \eor x_1=x_3 \eor x_2=x_3)\bigr]$\\
drei & $\forall x_1\forall x_2\forall x_3\forall x_4\bigl[(\atom{F}{x_1} \eand \atom{F}{x_2} \eand \atom{F}{x_3} \eand \atom{F}{x_4}) \eif {}$\\
& $(x_1=x_2 \eor x_1=x_3 \eor x_1=x_4 \eor {}$\\
& $x_2=x_3 \eor x_2=x_4 \eor x_3=x_4)\bigr]$\\
$n$ & $\forall x_1\ldots\forall x_{n+1}
\bigl[(\atom{F}{x_1} \eand \ldots \eand \atom{F}{x_{n+1}}) \eif {}$\\
& $(x_1=x_2 \eor \ldots \eor x_n=x_{n+1})\bigr]$ 
\end{tabular*}

\subsection*{Es gibt genau \blank\ $F$s.}
\label{summary.exactly}

Ein Weg `es gibt genau $n$ $F$s' auszudrücken ist zwei Symbolisierungen zu konjunktieren und zu sagen `es gibt zumindest $n$ $F$s und höchstens $n$ $F$s.' Die folgenden Sätze sind äquivalent dazu:
\begin{tabular*}{\textwidth}{rl}
null & $\forall x\,\enot \atom{F}{x}$\\
ein & $\exists x\bigl[\atom{F}{x} \eand \forall y(\atom{F}{y} \eif x = y)\bigr]$\\
zwei & $\exists x_1\exists x_2\bigl[\atom{F}{x_1} \eand \atom{F}{x_2} \eand {}$\\
& $\enot x_1 = x_2 \eand \forall y\bigl(\atom{F}{y} \eif (y= x_1 \eor y = x_2)\bigr) \bigr]$\\
drei & $\exists x_1\exists x_2\exists x_3\bigl[\atom{F}{x_1} \eand \atom{F}{x_2} \eand \atom{F}{x_3} \eand {}$\\
& $\enot x_1 =  x_2 \eand \enot  x_1 = x_3 \eand \enot x_2 = x_3 \eand {}$\\
& $\forall y\bigl(\atom{F}{y} \eif (y = x_1 \eor y = x_2 \eor y =  x_3)\bigr) \bigr]$\\
$n$ & $\exists x_1\ldots\exists x_n\bigl[\atom{F}{x_1} \eand\ldots\eand \atom{F}{x_n}  \eand {}$\\
&$ \enot x_1 = x_2 \eand\ldots\eand \enot x_{n-1}= x_n \eand \phantom{.}$\\
& $\forall y\bigl(\atom{F}{y} \eif (y= x_1 \eor \ldots \eor y= x_n)\bigr)\bigr]$ 
\end{tabular*}


\label{ProofRules}
\newpage\section{Grundregeln für Beweise in der WFL}
\renewenvironment{fitchproof}
	{\noindent\par\noindent\small$\begin{nd}}
	{\end{nd}$\noindent\normalsize\ignorespacesafterend}

%{\LARGE \textbf{Basic Rules of Proof}}
\begin{multicols}{2}
\subsection*{Wiederholung}

\begin{fitchproof}
	\have[m]{a}{\metav{A}}
	\have[\ ]{c}{\metav{A}} \by{R}{a}
\end{fitchproof}

\subsection*{Konjunktion}

\begin{fitchproof}
	\have[m]{a}{\metav{A}}
	\have[n]{b}{\metav{B}}
	\have[\ ]{c}{\metav{A}\eand\metav{B}} \ai{a, b}

	\have[m]{ab}{\metav{A}\eand\metav{B}}
\\	\have[\ ]{a}{\metav{A}} \ae{ab}

	\have[m]{ab}{\metav{A}\eand\metav{B}}
\\	\have[\ ]{b}{\metav{B}} \ae{ab}
\end{fitchproof}

\subsection*{Konditional}

\begin{fitchproof}
	\open
		\hypo[i]{a}{\metav{A}}
		\have[j]{b}{\metav{B}}
	\close
	\have[\ ]{ab}{\metav{A}\eif\metav{B}}\ci{a-b}

	\have[m]{ab}{\metav{A}\eif\metav{B}}
\\	\have[n]{a}{\metav{A}}
	\have[\ ]{b}{\metav{B}} \ce{ab,a}
\end{fitchproof}

\subsection*{Negation}

\begin{fitchproof}
\open
	\hypo[i]{a}{\metav{A}}
	\have[j]{nb}{\ered}
\close
\have[\ ]{na}{\enot\metav{A}}\ni{a-nb}

\have[m]{na}{\enot\metav{A}}
\\ \have[n]{a}{\metav{A}}
\have[ ]{bot}{\ered}\ri{na, a}
\end{fitchproof}

\subsection*{Indirekter Beweis}

\begin{fitchproof}
\open
	\hypo[i]{a}{\enot\metav{A}}
	\have[j]{nb}{\ered}
\close
\have[\ ]{na}{\metav{A}}\ip{a-nb}
\end{fitchproof}


\subsection*{Explosion}

\begin{fitchproof}
\have[m]{bot}{\ered}
\\\have[ ]{}{\metav{A}}\re{bot}
\end{fitchproof}

\subsection*{Disjunktion}

\begin{fitchproof}
	\have[m]{a}{\metav{A}}
	\have[\ ]{ab}{\metav{A}\eor\metav{B}}\oi{a}

	\have[m]{a}{\metav{A}}
\\	\have[\ ]{ba}{\metav{B}\eor\metav{A}}\oi{a}

	\have[m]{ab}{\metav{A}\eor\metav{B}}
\\	\open
		\hypo[i]{a}{\metav{A}}
		\have[j]{c1}{\metav{C}}
	\close
	\open
		\hypo[k]{b}{\metav{B}}
		\have[l]{c2}{\metav{C}}
	\close
	\have[\ ]{c}{\metav{C}} \oe{ab,a-c1, b-c2}
\end{fitchproof}

\subsection*{Bikonditional}

\begin{fitchproof}
	\open
		\hypo[i]{a1}{\metav{A}} 
		\have[j]{b1}{\metav{B}}
	\close
	\open
		\hypo[k]{b2}{\metav{B}}
		\have[l]{a2}{\metav{A}}
	\close
	\have[\ ]{ab}{\metav{A}\eiff\metav{B}}\bi{a1-b1,b2-a2}

	\have[m]{ab}{\metav{A}\eiff\metav{B}}
\\	\have[n]{a}{\metav{A}}
	\have[\ ]{b}{\metav{B}} \be{ab,a}

	\have[m]{ab}{\metav{A}\eiff\metav{B}}
\\	\have[n]{a}{\metav{B}}
	\have[\ ]{b}{\metav{A}} \be{ab,a}
\end{fitchproof}

\end{multicols}

\newpage
\section{Abgeleitete Regeln der WFL}
\begin{multicols}{2}
\subsection*{Disjunktiver Syllogismus}
\begin{fitchproof}
	\have[m]{ab}{\metav{A} \eor \metav{B}}
	\have[n]{nb}{\enot \metav{A}}
	\have[\ ]{con}{\metav{B}}\by{DS}{ab, nb}

	\have[m]{ab}{\metav{A} \eor \metav{B}}
\\	\have[n]{nb}{\enot \metav{B}}
	\have[\ ]{con}{\metav{A}}\by{DS}{ab, nb}
\end{fitchproof}

\subsection*{Modus Tollens}

\begin{fitchproof}
	\have[m]{ab}{\metav{A}\eif\metav{B}}
	\have[n]{a}{\enot\metav{B}}
	\have[\ ]{b}{\enot\metav{A}} \by{MT}{ab,a}
\end{fitchproof}

\subsection*{Doppelnegationseliminierung}
	\begin{fitchproof}
		\have[m]{dna}{\enot \enot \metav{A}}
		\have[ ]{a}{\metav{A}}\dne{dna}
	\end{fitchproof}


\subsection*{Ausgeschlossenes Drittes}
	\begin{fitchproof}
		\open
			\hypo[i]{a}{\metav{A}}
			\have[j]{c1}{\metav{B}}
		\close
		\open
			\hypo[k]{b}{\enot\metav{A}}
			\have[l]{c2}{\metav{B}}
		\close
		\have[\ ]{ab}{\metav{B}}\tnd{a-c1,b-c2}
	\end{fitchproof}

\subsection*{De Morgan Regeln}
\begin{fitchproof}
	\have[m]{ab}{\enot (\metav{A} \eor \metav{B})}
	\have[\ ]{dm}{\enot \metav{A} \eand \enot \metav{B}}\dem{ab}

	\have[m]{ab}{\enot \metav{A} \eand \enot \metav{B}}
\\	\have[\ ]{dm}{\enot (\metav{A} \eor \metav{B})}\dem{ab}

	\have[m]{ab}{\enot (\metav{A} \eand \metav{B})}
\\	\have[\ ]{dm}{\enot \metav{A} \eor \enot \metav{B}}\dem{ab}

	\have[m]{ab}{\enot \metav{A} \eor \enot \metav{B}}
\\	\have[\ ]{dm}{\enot (\metav{A} \eand \metav{B})}\dem{ab}
\end{fitchproof}
\end{multicols}

\newpage

\section{Grundregeln der LEO}

\begin{multicols}{2}
\subsection*{Universaleliminierung}

\begin{fitchproof}
	\have[m]{a}{\forall \metav{x}\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)}
	\have[\ ]{c}{\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)} \Ae{a}
\end{fitchproof}

\subsection*{Universaleinführung}

\begin{fitchproof}
	\have[m]{a}{\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)}
	\have[\ ]{c}{\forall \metav{x}\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)} \Ai{a}
\end{fitchproof}

\medskip
\noindent \metav{c} darf nicht in einer ungetilgten Annahme vorkommen

\noindent \metav{x} darf nicht in $\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)$ vorkommen

\subsection*{Existenzeinführung}

\begin{fitchproof}
	\have[m]{a}{\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)}
	\have[\ ]{c}{\exists \metav{x}\metav{A}(\ldots \metav{x} \ldots \metav{c}\ldots)}\Ei{a}
\end{fitchproof}

\medskip
\noindent \metav{x} darf nicht in $\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)$ vorkommen

%\noindent You can replace one or more instance of \metav{c} with \metav{x}.

\subsection*{Existenzeliminierung}

\begin{fitchproof}
	\have[m]{a}{\exists \metav{x}\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)}
	\open	
		\hypo[i]{b}{\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)}
		\have[j]{c}{\metav{B}}
	\close
	\have[\ ]{d}{\metav{B}}\Ee{a,b-c}
\end{fitchproof}

\medskip
\noindent \metav{c} darf weder in $\exists \metav{x}\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)$, in \metav{B}, noch in einer ungetilgten Annahme vorkommen

\vfill\columnbreak

\end{multicols}

\subsection*{Identitätseinführung}

\begin{fitchproof}
	\have[\ \,\,\,]{x}{\metav{c}=\metav{c}} \by{=I}{}
\end{fitchproof}


\subsection*{Identitätseliminierung}

\begin{multicols}{2}
\begin{fitchproof}
	\have[m]{e}{\metav{a}=\metav{b}}
	\have[n]{a}{\metav{A}(\ldots \metav{a} \ldots \metav{a}\ldots)}
	\have[\ ]{ea1}{\metav{A}(\ldots \metav{b} \ldots \metav{a}\ldots)} \by{=E}{e,a}
\end{fitchproof}
\begin{fitchproof}
	\have[m]{e}{\metav{a}=\metav{b}}
	\have[n]{a}{\metav{A}(\ldots \metav{b} \ldots \metav{b}\ldots)}
	\have[\ ]{ea2}{\metav{A}(\ldots \metav{a} \ldots \metav{b}\ldots)} \by{=E}{e,a}
\end{fitchproof}
\end{multicols}

\begin{minipage}{\textwidth} 
\section{Abgeleitete Regeln der LEO}

\begin{multicols}{2}
\begin{fitchproof}
	\have[m]{ab}{\forall \metav{x}\enot \metav{A}}
	\have[\ ]{ac}{\enot \exists \metav{x} \metav{A}}\cq{m}

	\have[m]{ab}{\enot \exists \metav{x}  \metav{A}}
\\	\have[\ ]{ac}{\forall \metav{x}\enot\metav{A}}\cq{m}
\end{fitchproof}
\begin{fitchproof}
	\have[m]{ab}{\exists \metav{x}\enot\metav{A}}
	\have[\ ]{ac}{\enot \forall \metav{x} \metav{A}}\cq{m}

	\have[m]{ab}{\enot \forall \metav{x}  \metav{A}}
\\	\have[\ ]{ac}{\exists \metav{x}\enot \metav{A}}\cq{m}
\end{fitchproof}
\end{multicols}
\end{minipage}