\documentclass[10pt,a4paper]{article}

% Packages
\usepackage{fancyhdr}           % For header and footer
\usepackage{multicol}           % Allows multicols in tables
\usepackage{tabularx}           % Intelligent column widths
\usepackage{tabulary}           % Used in header and footer
\usepackage{hhline}             % Border under tables
\usepackage{graphicx}           % For images
\usepackage{xcolor}             % For hex colours
%\usepackage[utf8x]{inputenc}    % For unicode character support
\usepackage[T1]{fontenc}        % Without this we get weird character replacements
\usepackage{colortbl}           % For coloured tables
\usepackage{setspace}           % For line height
\usepackage{lastpage}           % Needed for total page number
\usepackage{seqsplit}           % Splits long words.
%\usepackage{opensans}          % Can't make this work so far. Shame. Would be lovely.
\usepackage[normalem]{ulem}     % For underlining links
% Most of the following are not required for the majority
% of cheat sheets but are needed for some symbol support.
\usepackage{amsmath}            % Symbols
\usepackage{MnSymbol}           % Symbols
\usepackage{wasysym}            % Symbols
%\usepackage[english,german,french,spanish,italian]{babel}              % Languages

% Document Info
\author{tiziano123}
\pdfinfo{
  /Title (pradikatenlogik-theorie.pdf)
  /Creator (Cheatography)
  /Author (tiziano123)
  /Subject (Pr{\"a}dikatenlogik Theorie Cheat Sheet)
}

% Lengths and widths
\addtolength{\textwidth}{6cm}
\addtolength{\textheight}{-1cm}
\addtolength{\hoffset}{-3cm}
\addtolength{\voffset}{-2cm}
\setlength{\tabcolsep}{0.2cm} % Space between columns
\setlength{\headsep}{-12pt} % Reduce space between header and content
\setlength{\headheight}{85pt} % If less, LaTeX automatically increases it
\renewcommand{\footrulewidth}{0pt} % Remove footer line
\renewcommand{\headrulewidth}{0pt} % Remove header line
\renewcommand{\seqinsert}{\ifmmode\allowbreak\else\-\fi} % Hyphens in seqsplit
% This two commands together give roughly
% the right line height in the tables
\renewcommand{\arraystretch}{1.3}
\onehalfspacing

% Commands
\newcommand{\SetRowColor}[1]{\noalign{\gdef\RowColorName{#1}}\rowcolor{\RowColorName}} % Shortcut for row colour
\newcommand{\mymulticolumn}[3]{\multicolumn{#1}{>{\columncolor{\RowColorName}}#2}{#3}} % For coloured multi-cols
\newcolumntype{x}[1]{>{\raggedright}p{#1}} % New column types for ragged-right paragraph columns
\newcommand{\tn}{\tabularnewline} % Required as custom column type in use

% Font and Colours
\definecolor{HeadBackground}{HTML}{333333}
\definecolor{FootBackground}{HTML}{666666}
\definecolor{TextColor}{HTML}{333333}
\definecolor{DarkBackground}{HTML}{0268A3}
\definecolor{LightBackground}{HTML}{EFF5F9}
\renewcommand{\familydefault}{\sfdefault}
\color{TextColor}

% Header and Footer
\pagestyle{fancy}
\fancyhead{} % Set header to blank
\fancyfoot{} % Set footer to blank
\fancyhead[L]{
\noindent
\begin{multicols}{3}
\begin{tabulary}{5.8cm}{C}
    \SetRowColor{DarkBackground}
    \vspace{-7pt}
    {\parbox{\dimexpr\textwidth-2\fboxsep\relax}{\noindent
        \hspace*{-6pt}\includegraphics[width=5.8cm]{/web/www.cheatography.com/public/images/cheatography_logo.pdf}}
    }
\end{tabulary}
\columnbreak
\begin{tabulary}{11cm}{L}
    \vspace{-2pt}\large{\bf{\textcolor{DarkBackground}{\textrm{Pr{\"a}dikatenlogik Theorie Cheat Sheet}}}} \\
    \normalsize{by \textcolor{DarkBackground}{tiziano123} via \textcolor{DarkBackground}{\uline{cheatography.com/57454/cs/15227/}}}
\end{tabulary}
\end{multicols}}

\fancyfoot[L]{ \footnotesize
\noindent
\begin{multicols}{3}
\begin{tabulary}{5.8cm}{LL}
  \SetRowColor{FootBackground}
  \mymulticolumn{2}{p{5.377cm}}{\bf\textcolor{white}{Cheatographer}}  \\
  \vspace{-2pt}tiziano123 \\
  \uline{cheatography.com/tiziano123} \\
  \end{tabulary}
\vfill
\columnbreak
\begin{tabulary}{5.8cm}{L}
  \SetRowColor{FootBackground}
  \mymulticolumn{1}{p{5.377cm}}{\bf\textcolor{white}{Cheat Sheet}}  \\
   \vspace{-2pt}Published 23rd March, 2018.\\
   Updated 23rd March, 2018.\\
   Page {\thepage} of \pageref{LastPage}.
\end{tabulary}
\vfill
\columnbreak
\begin{tabulary}{5.8cm}{L}
  \SetRowColor{FootBackground}
  \mymulticolumn{1}{p{5.377cm}}{\bf\textcolor{white}{Sponsor}}  \\
  \SetRowColor{white}
  \vspace{-5pt}
  %\includegraphics[width=48px,height=48px]{dave.jpeg}
  Measure your website readability!\\
  www.readability-score.com
\end{tabulary}
\end{multicols}}




\begin{document}
\raggedright
\raggedcolumns

% Set font size to small. Switch to any value
% from this page to resize cheat sheet text:
% www.emerson.emory.edu/services/latex/latex_169.html
\footnotesize % Small font.

\begin{multicols*}{4}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Logische Äquivalenz}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 2.7 {[}Logische Äquivalenz{]}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Zwei Formeln φ, ψ ∈ FO(S) hei{\ss}en (logisch) {\"a}quivalent, gdw. für alle S-Interpretationen J gilt: J |= φ gdw. J |=ψ. {\bf{In Symbolen: φ≡ψ.}}} \tn 
% Row Count 4 (+ 3)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{Bem.: Logische Äquivalenzen der AL übertragen sich auf FO. Hinzu treten charakteristische logische Äquivalenzen im Zusammenhang mit Quantoren. \newline  \newline Z.B. die Dualit{\"a}t zwischen ∀ und ∃, die besagt dass für alle φ ∈ FO(S):  \newline \{\{ac\}\} \newline {\bf{∃xφ ≡ ¬∀x¬φ,}} \newline {\bf{∀xφ ≡ ¬∃x¬φ.}}}  \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Erfüllbarkeits{\"a}quivalenz}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 2.10 Erfüllbarkeits{\"a}quivalenz}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Formeln φ,φ′ hei{\ss}en erfülbarkeits{\"a}quivalent wenn gilt: φ erfüllbar gdw. φ′ erfülbar. Analog wird Erfüllbarkeits{\"a}quivalenz für Formelmengen definiert.} \tn 
% Row Count 5 (+ 4)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Signaturen}}  \tn
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Eine {\bf{Signatur S}} ist eine Menge von Konstanten-, Funktions- und Relationssymbolen, mit angegebenen Stelligkeiten. Spezialfa ̈lle: S ohne Funktionssymbole : relationale Signatur; S ohne Relationssymbole : funktionale Signatur.% Row Count 5 (+ 5)
} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{S-Strukturen}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 1.1 {[}S-Strukturen{]}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Für Signatur S: Eine S-Struktur A = (A,c\textasciicircum{}A\textasciicircum{},...,f\textasciicircum{}A\textasciicircum{},...,R\textasciicircum{}A\textasciicircum{},...) besteht aus ihrer Tr{\"a}germenge A ≠ ∅ zusammen mit einer Interpretation der Symbole in S, d.h., für jedes Konstantensymbol c ∈ S: ein ausgezeichnetes Element c\textasciicircum{}A\textasciicircum{} ∈ A. für jedes n-stellige Funktionssymbol f ∈ S: eine n-stellige Funktion f\textasciicircum{}A\textasciicircum{} : A\textasciicircum{}n\textasciicircum{}→ A. für jedes n-stellige Relationssymbol R ∈ S: eine n-stellige Relation R\textasciicircum{}A\textasciicircum{} ⊆ A\textasciicircum{}n\textasciicircum{}.} \tn 
% Row Count 10 (+ 9)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{S-Terme}}  \tn
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 1.3 {[}S-Terme{]} }}Die Menge der S-Terme, T(S) (mit Variablenmenge V) ist induktiv erzeugt wie folgt: \newline % Row Count 3 (+ 3)
• x∈T(S) für jede Variable x ∈ V. \newline % Row Count 4 (+ 1)
• c ∈ T(S) für jedes Konstantensymbol c ∈ S. \newline % Row Count 6 (+ 2)
• ist f ∈ S ein n-stelliges Funktionssymbol, und sind t`1`, . . . , t`n` ∈ T (S), so ist auch ft`1`...t`n` ∈T(S). \newline % Row Count 9 (+ 3)
T`n`(S) ⊆ T(S): die Mengen der Terme, in denen nur Variablensymbole aus V`n` = \{x`1`, . . . , x`n`\} vorkommen. \newline % Row Count 12 (+ 3)
{\emph{Speziell}} steht {\bf{T`0`(S)}} für die Menge der Variablen-freien Terme (= ∅ wenn S keine Konstanten hat).% Row Count 15 (+ 3)
} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Allgemeingültigkeit}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 2.6 {[}Allgemeingültigkeit{]}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Eine Formel φ ∈ FO(S) hei{\ss}t allgemeingültig gdw. für alle S-Interpretationen J gilt: J |= φ.} \tn 
% Row Count 3 (+ 2)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Folgerungsbeziehung}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 2.5}} {[}{\bf{Folgerungsbeziehung}}{]}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{φ |= ψ bzw. Φ |= ψ.} \tn 
% Row Count 2 (+ 1)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{Für φ,ψ ∈ FO(S): \newline ψ ist eine logische Folgerung von φ, oder ψ folgt aus φ, in Symbolen φ |= ψ, gdw. für alle S-Interpretationen J gilt:{\bf{ J |= φ ⇒ J |= ψ.}} \newline  \newline Entsprechend ist Φ |= ψ für Formelmengen Φ definiert (ψ folgt aus Φ).}  \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{FO mit und ohne Gleichheit}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 2.11 {[}FO ohne Gleichheit{]}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{FO\textasciicircum{}≠\textasciicircum{}(S) ⊆ FO(S) ist aufgebaut wie FO aber ohne Termgleichheiten als atomare Formeln. Die Semantik von FO übertr{\"a}gt sich auf die Teillogik FO\textasciicircum{}≠\textasciicircum{}.} \tn 
% Row Count 5 (+ 4)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Bemerkung 2.13}} Zu jeder Formelmenge Φ ⊆ FO(S) erh{\"a}lt man durch eine systematische Übersetzung in eine explizite Modellierung der Gleichheitsrelation durch eine neues Relationssysmbol ∼ eine erfülbarkeits{\"a}quivalente Formelmenge Φ`∼`  ⊆ F0\textasciicircum{}≠\textasciicircum{}(S ∪ \{∼\}).} \tn 
% Row Count 11 (+ 6)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Termstruktur}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Defintion 1.4 Termstrukturen}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Die Menge der S-Terme ist Tr{\"a}ger einer S`F`-Struktur T = T (S), der Termstruktur ({\bf{Herbrand-Struktur}}) zu S, mit der folgenden natürlichen Interpretation der Konstanten- und Funktionssymbole in S:} \tn 
% Row Count 5 (+ 4)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{• für Konstantensymbol c ∈ S:  \newline c\textasciicircum{}T\textasciicircum{} := c ∈ T(S). \newline • für n-stelliges Funktionssymbol f ∈ S: f \textasciicircum{}T\textasciicircum{}: T(S)\textasciicircum{}n\textasciicircum{}  → T(S) \newline (t`1`,...,t`n`)  → ft`1` ...t`n`. \newline Wenn S Konstantensymbole hat, ist auch T`0`(S) Tr{\"a}ger einer entsprechenden Termstruktur T`0`(S) (eine Substruktur von T (S)).}  \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Pr{\"a}nexe Normalform}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 3.1 {[}pr{\"a}nexe NF{]} }}FO-Formeln in pr{\"a}nexer Normalform sind von der Form Q`1`x`i``1` ...Q`k`x`ik` ψ, wo k ∈ N, Q`i` ∈ \{∀, ∃\} und ψ {\bf{quantorenfrei.}} ψ hei{\ss}t auch quantorenfreier Kern der Formel, Q`1`x`i1` . . . Q`k` x`i``k` ihr Quantorenpr{\"a}fix.} \tn 
% Row Count 6 (+ 6)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Man braucht i.d.R. zus{\"a}tzliche Variablensymbole!} \tn 
% Row Count 7 (+ 1)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{Satz 3.4 Jede FO-Formel ist  {\"a}quivalent zu einer Formel in pr{\"a}nexer NF.} \tn 
% Row Count 9 (+ 2)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Beispiel 3.2}} S = \{E\}, E 2-st. Relations-Symbol. Die folgenden Äquivalenzen liefern auf der rechten Seite pr{\"a}nexe Formalisierungen:  \newline ∃y(Exy ∧ ∀x(Eyx → x = y)) ≡ ∃y∀z Exy ∧ (Eyz → z = y) ,  \newline ∃y∀xExy ∨ ¬∃yExy ≡ ∃y1∀y2∀y3 Ey2y1 ∨ ¬Exy3 .}  \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Belegungen}}  \tn
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 1.5 }} \newline % Row Count 1 (+ 1)
{\bf{{[}Belegungen und Interpretationen{]}}} \newline % Row Count 2 (+ 1)
Eine Funktion β: V → A hei{\ss}t Belegung (für die x ∈ V) in der S-Struktur A = (A,...). Eine S-Struktur A und Belegung β zusammen bilden eine S-Interpretation J = (A, β). \newline % Row Count 6 (+ 4)
\{\{ac\}\} \newline % Row Count 7 (+ 1)
•Für t = x ({\bf{x ∈ V Variable}}): \newline % Row Count 8 (+ 1)
 t\textasciicircum{}J\textasciicircum{}:=β(x). \newline % Row Count 9 (+ 1)
• Für t = c ({\bf{c ∈ S Konstantensymbol}}): \newline % Row Count 10 (+ 1)
 t\textasciicircum{}J\textasciicircum{}:= c\textasciicircum{}A\textasciicircum{}. \newline % Row Count 11 (+ 1)
• Für t = ft`1` ...t`n`, mit n-stelligem Funktionssymbol f ∈ S: \newline % Row Count 13 (+ 2)
 t\textasciicircum{}J\textasciicircum{} := f\textasciicircum{}A\textasciicircum{} (t`1`\textasciicircum{}J\textasciicircum{},...,t`n`\textasciicircum{}J\textasciicircum{} ).% Row Count 14 (+ 1)
} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{Schreibweisen für Belegungen und Interpretationen auf Seite 6 FO Skript über Kapitel 2}  \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Freie Variablen}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 2.2 {[}freie Variablen{]}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Induktive Definition der Menge der freien Variablen, frei(φ) ⊆ V, für φ ∈ FO(S):} \tn 
% Row Count 3 (+ 2)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{Formeln {\bf{ohne}} freie Variablen hei{\ss}en {\bf{S{\"a}tze}}.} \tn 
% Row Count 5 (+ 2)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Schreibweisen: }}FO`n`(S) := \{φ ∈ FO(S): frei(φ) ⊆ V`n`\}. Für φ ∈ FO`n`(S) schreiben wir auch φ = φ(x`1`, . . . , x `n`) um die m{\"o}glicherweise freien Variablen explizit anzudeuten.} \tn 
% Row Count 9 (+ 4)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{frei(t`1` = t`2`) := var(t`1`) ∪ var(t`2`).  \newline frei(Rt`1` . . . t `n`) := var(t`1`) ∪ . . . ∪ var(t `n`). \newline frei(¬φ) := frei(φ).  \newline frei(φ ∧ ψ) = frei(φ ∨ ψ) := frei(φ) ∪ frei(ψ). \newline frei(∃xφ) = frei(∀xφ) := frei(φ) \textbackslash{} \{x\}.}  \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Quantorenrang}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 2.3 {[}Quantorenrang{]}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Induktive Definition des Quantorenrangs, qr(φ) ∈ N, für φ ∈ FO(S):} \tn 
% Row Count 3 (+ 2)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{Formeln von Quantorenrang 0 hei{\ss}en {\bf{quantorenfrei.}}} \tn 
% Row Count 5 (+ 2)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{qr(φ) = 0 für atomares φ. \newline qr(¬φ) := qr(φ). \newline qr(φ ∧ ψ) = qr(φ ∨ ψ) := max(qr(φ), qr(ψ)).  \newline qr(∃xφ) = qr(∀xφ) := qr(φ) + 1.}  \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Semantik}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 2.4 {[}Semantik{]}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Für S-Interpretation J = (A, β) und φ ∈ FO(S): J erfüllt φ gdw. φ \textasciicircum{}J\textasciicircum{} = 1. {\bf{Schreibweise: J|= φ.}}} \tn 
% Row Count 4 (+ 3)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{Für Formelmengen Φ ⊆ AL(V) entsprechend: {\bf{ J|= Φ }}gdw. {\bf{J |= φ für alle φ ∈ Φ.}}} \tn 
% Row Count 6 (+ 2)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Die Relation |= hei{\ss}t Modellbeziehung.} \tn 
% Row Count 7 (+ 1)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Herbrand}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Satz 3.10 (Herbrand)}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{Sei Φ ⊆ FO`0`≠ (S) eine Menge von universellen, gleichheitsfreien S{\"a}tzen. Dann sind {\"a}quivalent:} \tn 
% Row Count 4 (+ 3)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{(i)}} Φ erfüllbar.} \tn 
% Row Count 5 (+ 1)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{{\bf{(ii)}}  Φ hat ein Herbrand-Modell {\bf{{\emph{H}} =  ( T`0`(S), (R\textasciicircum{}H\textasciicircum{})`R`∈`S`) |= Φ}}, dessen Tr{\"a}germenge und Funktions- und \seqsplit{Konstanteninterpretationen} mit der Termstruktur T`0`(S) übereinstimmen (H erweitert die S`F`-Struktur T`0`(S) lediglich um eine geeignete Interpretation der Relationssymbole in S).} \tn 
% Row Count 12 (+ 7)
% Row 4
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Definition 3.8}} Eine Formel ist {\bf{universell}} wenn sie aus atomaren und negiert atomaren Formeln allein mittels{\bf{ ∧, ∨ und ∀-Quantoren}} aufgebaut ist.} \tn 
% Row Count 16 (+ 4)
% Row 5
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Lemma 3.12}} Sei Φ ⊆ FO`0`≠ (S) eine Menge von universell-pr{\"a}nexen S{\"a}tzen. Dann sind  {\"a}quivalent:} \tn 
% Row Count 19 (+ 3)
% Row 6
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{(i)}} Φ erfüllbar. {\bf{(ii)}} {[}{[}Φ{]}{]}\textasciicircum{}AL\textasciicircum{} erfüllbar.} \tn 
% Row Count 21 (+ 2)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Erfülbarkeit}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{• Φ ⊆ FO`0`(S) eine Satzmenge (ohne freie Variablen) ist. Man erh{\"a}lt eine zu einer Formelmenge erfüllbarkeits{\"a}quivalente Satzmenge, indem man neue Konstantensymbole für alle freien Variablen substituiert} \tn 
% Row Count 5 (+ 5)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{• Φ ⊆ FO`0`≠ (S) gleichheitsfrei ist. Eine explizite Modellierung der Gleichheitsrelation durch eine zus{\"a}tzliche Äquivalenzrelation (siehe Bemerkung 2.13) führt zu erfüllbarkeits{\"a}quivalenten Satzmengen ohne Gleichheit.} \tn 
% Row Count 10 (+ 5)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{• Φ ⊆ FO`0`≠ (S) aus universell-pr{\"a}nexen, gleichheitsfreien S{\"a}tzen besteht. Skolemisierung liefert eine erfüllbarkeits{\"a}quivalente Satzmenge in universell-pr{\"a}nexer Form.} \tn 
% Row Count 14 (+ 4)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{• S mindestens ein Konstantensymbol enth{\"a}lt, sodass T`0`(S) ≠ ∅ ist, und wir uns ggf. auf Herbrand-Modelle von Φ ⊆ FO`0`≠ (S) zurückziehen k{\"o}nnen.} \tn 
% Row Count 18 (+ 4)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{Φ erfüllbar ⇔ H |= Φ für eine \newline                         Herbrand-Struktur H =  T`0`(S),(R\textasciicircum{}H\textasciicircum{})`R`∈`S` .}  \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{3.833cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{3.833cm}}{\bf\textcolor{white}{Kompaktheitssatz (FO)}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Satz 4.1 (Kompaktheitssatz)}} Für jede Formelmenge Φ ⊆ FO sind  {\"a}quivalent:} \tn 
% Row Count 2 (+ 2)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{(i) Φ erfüllbar. (ii) Jede endliche Teilemenge Φ`0` ⊆ Φ ist erfüllbar.} \tn 
% Row Count 4 (+ 2)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{{\bf{Korollar 4.2 }}Für jede Formelmenge Φ ⊆ FO und Formel ψ ∈ FO sind  {\"a}quivalent:} \tn 
% Row Count 6 (+ 2)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{3.833cm}}{{\bf{(i)}} Φ |= ψ. {\bf{(ii)}} Es existiert eine endliche Teilemenge Φ`0` ⊆ Φ, sodass Φ`0` |= ψ.} \tn 
% Row Count 8 (+ 2)
% Row 4
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{3.833cm}}{Das Korollar folgt aus dem Satz über den Zusammenhang: {\bf{Φ|=φ gdw. Φ ∪ \{¬φ\} unerfüllbar.}}} \tn 
% Row Count 10 (+ 2)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}


% That's all folks
\end{multicols*}

\end{document}