Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
Loading items

Target

Select target project
  • general/stups/prob-teaching-notebooks
1 result
Select Git revision
Loading items
Show changes

Commits on Source 2

%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Theoretische Informatik - Vorlesung 0 - Teil 1 Logik # Theoretische Informatik - Vorlesung 0 - Teil 1 Logik
* April 2023 * April 2020
* Michael Leuschel * Michael Leuschel
* Lehrstuhl Softwaretechnik und Programmiersprachen * Lehrstuhl Softwaretechnik und Programmiersprachen
* Heinrich-Heine Universität Düsseldorf * Heinrich-Heine Universität Düsseldorf
Grundlagen der Logik und Mengentheorie sind nicht im Skript. Grundlagen der Logik und Mengentheorie sind nicht im Skript.
Hier definieren wir einige Grundlagen und Notationen, die im Skript verwendet werden. Hier definieren wir einige Grundlagen und Notationen, die im Skript verwendet werden.
Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich. Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich.
Die Folien für diese Grundlagen sind als Jupyter Notebooks erstellt worden und im [GitLab der Informatik](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) erhältlich. Die Folien für diese Grundlagen sind als Jupyter Notebooks erstellt worden und im [GitLab der Informatik](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) erhältlich.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Was ist ein Notebook? ## Was ist ein Notebook?
* Dokument mit Text und ausführbaren Code-Abschnitten * Dokument mit Text und ausführbaren Code-Abschnitten
* Code kann interaktiv ausgeführt werden * Code kann interaktiv ausgeführt werden
* Ergebnisse erscheinen im Notebook unter dem jeweiligem Code * Ergebnisse erscheinen im Notebook unter dem jeweiligem Code
* Ähnlich wie eine REPL (read-eval-print-loop), mit einigen Unterschieden: * Ähnlich wie eine REPL (read-eval-print-loop), mit einigen Unterschieden:
* Ausgaben können formatierten Text und Grafiken enthalten * Ausgaben können formatierten Text und Grafiken enthalten
* Speicherbar als Datei * Speicherbar als Datei
* Code kann später neu ausgeführt werden * Code kann später neu ausgeführt werden
* Weitergabe an andere Nutzer möglich * Weitergabe an andere Nutzer möglich
* Implementierungen: Mathematica, Maple, Jupyter, u. a. * Implementierungen: Mathematica, Maple, Jupyter, u. a.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Jupyter Notebook ## Jupyter Notebook
* Browserbasierte Notebook-Oberfläche * Browserbasierte Notebook-Oberfläche
* Open Source und plattformübergreifend * Open Source und plattformübergreifend
* Stammt aus der Python-Community, in Python implementiert * Stammt aus der Python-Community, in Python implementiert
* ACM System Software Award 2017 * ACM System Software Award 2017
* Jupyter-Notebooks verschiedene Programmiersprachen verwenden * Jupyter-Notebooks verschiedene Programmiersprachen verwenden
* Ein sprachspezifischer **Kernel** stellt die Sprache dem Jupyter Frontend zur Verfügung * Ein sprachspezifischer **Kernel** stellt die Sprache dem Jupyter Frontend zur Verfügung
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## [ProB](https://prob.hhu.de/w/) Kernel ## [ProB](https://prob.hhu.de/w/) Kernel
![ProB](img/prob_logo.png) ![ProB](img/prob_logo.png)
* [ProB](https://prob.hhu.de/w/) ist ein Werkzeug zur Animation, Verifikation und Visualisierung formaler Spezifikationen * [ProB](https://prob.hhu.de/w/) ist ein Werkzeug zur Animation, Verifikation und Visualisierung formaler Spezifikationen
* Unterstützt B-Spezifikationen für sicherheitskritsche Anwendungen * Unterstützt B-Spezifikationen für sicherheitskritsche Anwendungen
* Entwicklung am STUPS Lehrstuhl * Entwicklung am STUPS Lehrstuhl
* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik. * Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.
* Eignet sich aber auch für mathematische Ausführungen * Eignet sich aber auch für mathematische Ausführungen
* Der [ProB-Jupyter-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) stellt die B-Sprache und die mathematischen Grundlagen für Jupyter Notebooks zur Verfügung * Der [ProB-Jupyter-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) stellt die B-Sprache und die mathematischen Grundlagen für Jupyter Notebooks zur Verfügung
Um diese Notebooks zu starten kann man entweder selber Jupyter und den [ProB-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren. Um diese Notebooks zu starten kann man entweder selber Jupyter und den [ProB-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren.
Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger): Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger):
[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob-teaching-notebooks.git/HEAD?urlpath=%2Ftree%2Finfo4%2F) [![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob-teaching-notebooks.git/HEAD?urlpath=%2Ftree%2Finfo4%2F)
Damit Jupyter formattierte Ausgabe für Formeln und Tabellen zulässt muss rechts oben in der Menuleiste auf "Not Trusted" drücken. Wenn das Notebook als "Trusted" markiert ist wird JavaScript aktiviert und die Ausgabe wird besser ausgegeben. Damit Jupyter formattierte Ausgabe für Formeln und Tabellen zulässt muss rechts oben in der Menuleiste auf "Not Trusted" drücken. Wenn das Notebook als "Trusted" markiert ist wird JavaScript aktiviert und die Ausgabe wird besser ausgegeben.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Was ist Logik? # Was ist Logik?
Quelle [Wikipedia](https://de.wikipedia.org/wiki/Logik): Quelle [Wikipedia](https://de.wikipedia.org/wiki/Logik):
* vernünftiges Schlussfolgern, Denklehre * vernünftiges Schlussfolgern, Denklehre
* In der Logik wird die Struktur von Argumenten im Hinblick auf ihre Gültigkeit untersucht, unabhängig vom Inhalt der Aussagen * In der Logik wird die Struktur von Argumenten im Hinblick auf ihre Gültigkeit untersucht, unabhängig vom Inhalt der Aussagen
* Traditionell ist die Logik ein Teil der Philosophie. * Traditionell ist die Logik ein Teil der Philosophie.
* Seit dem 20. Jahrhundert versteht man unter Logik überwiegend symbolische Logik, die auch als grundlegende Strukturwissenschaft, z. B. innerhalb der Mathematik und der theoretischen Informatik, behandelt wird. * Seit dem 20. Jahrhundert versteht man unter Logik überwiegend symbolische Logik, die auch als grundlegende Strukturwissenschaft, z. B. innerhalb der Mathematik und der theoretischen Informatik, behandelt wird.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Warum Logik studieren? # Warum Logik studieren?
* Hardware: logische Schaltkreise * Hardware: logische Schaltkreise
* Wissensdarstellung und intelligentes Denken: Künstliche Intelligenz, deklarative Darstellung von Wissen, semantisches Web, ... * Wissensdarstellung und intelligentes Denken: Künstliche Intelligenz, deklarative Darstellung von Wissen, semantisches Web, ...
* Überlegungen über Programme: Verifikation, statische Programmanalyse, Programmoptimierung,... * Überlegungen über Programme: Verifikation, statische Programmanalyse, Programmoptimierung,...
* Universale Vorrichtung zur Berechnung: Datenbanken, logische Programmierung, ... * Universale Vorrichtung zur Berechnung: Datenbanken, logische Programmierung, ...
* Grundlage der Mathematik und auch der theoretischen Informatik * Grundlage der Mathematik und auch der theoretischen Informatik
* Halpern et al. On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.cmu.edu/~rwh/papers/unreasonable/basl.pdf * Halpern et al. On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.cmu.edu/~rwh/papers/unreasonable/basl.pdf
* Zitat aus diesem Artikel: * Zitat aus diesem Artikel:
> The effectiveness of logic in computer science is not by any means limited to the areas mentioned in here. As a matter of fact, it spans a wide spectrum of areas, from artificial intelligence to software engineering. Overall, logic provides computer science with both a unifying foundational framework and a powerful tool for modeling and reasoning about aspects of computation. > The effectiveness of logic in computer science is not by any means limited to the areas mentioned in here. As a matter of fact, it spans a wide spectrum of areas, from artificial intelligence to software engineering. Overall, logic provides computer science with both a unifying foundational framework and a powerful tool for modeling and reasoning about aspects of computation.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Welche Logik studieren? # Welche Logik studieren?
* Aussagenlogik * Aussagenlogik
* Prädikatenlogik der ersten Stufe (FOL - First Order Logic) * Prädikatenlogik der ersten Stufe (FOL - First Order Logic)
* Logik höherer Stufe (HOL - Higher Order Logic) * Logik höherer Stufe (HOL - Higher Order Logic)
* eine temporale Logik * eine temporale Logik
* eine mehrwertige Logik oder gar Fuzzy Logik * eine mehrwertige Logik oder gar Fuzzy Logik
* Relevanzlogik, lineare Logik * Relevanzlogik, lineare Logik
* eine nichtmonotone Logik * eine nichtmonotone Logik
Wir werden die klassische, zweiwertige, monotone **Aussagenlogik** Wir werden die klassische, zweiwertige, monotone **Aussagenlogik**
und **Prädikatenlogik** studieren (zusammen mit Mengentheorie). und **Prädikatenlogik** studieren (zusammen mit Mengentheorie).
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Aussagenlogik # Aussagenlogik
Eine Aussage ist endweder wahr ($\mathit{TRUE}$) oder falsch ($\mathit{FALSE}$). Eine Aussage ist endweder wahr ($\mathit{TRUE}$) oder falsch ($\mathit{FALSE}$).
Hier sind vier Aussagen: Hier sind vier Aussagen:
1. Siegfried ist ein Ritter 1. Siegfried ist ein Ritter
2. Alle Ritter sagen die Wahrheit 2. Alle Ritter sagen die Wahrheit
3. Siegfried sagt "Ich habe den Drachen getötet" 3. Siegfried sagt "Ich habe den Drachen getötet"
4. Siegfried hat den Drachen getötet. 4. Siegfried hat den Drachen getötet.
Die Logik interessiert sich weniger ob Aussagen wahr oder falsch sind, sondern mehr um Zusammenhänge zwischen möglichen Wahrheitswerten verschiedener Aussagen und Formeln. Die Logik interessiert sich weniger ob Aussagen wahr oder falsch sind, sondern mehr um Zusammenhänge zwischen möglichen Wahrheitswerten verschiedener Aussagen und Formeln.
Zum Beispiel, wenn wir die Aussagen 1,2 und 3 als wahr annehmen, dann müssen wir auch die Aussage 4 als wahr annehmen. Zum Beispiel, wenn wir die Aussagen 1,2 und 3 als wahr annehmen, dann müssen wir auch die Aussage 4 als wahr annehmen.
Einige Aussagen haben manchmal vordefinierte Wahrheitswerte. Einige Aussagen haben manchmal vordefinierte Wahrheitswerte.
Wir zum Beispiel benutzen Arithmetik und Mengetheorie in unseren logischen Formeln, ohne diese selber in Logik zu formalisieren. Wir zum Beispiel benutzen Arithmetik und Mengetheorie in unseren logischen Formeln, ohne diese selber in Logik zu formalisieren.
Hier sind ein paar Aussagen in Arithmetik: Hier sind ein paar Aussagen in Arithmetik:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>1 2>1
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1+1 = 2 1+1 = 2
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2<1 2<1
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Junktoren und Formeln # Junktoren und Formeln
Jede Aussage ist auch eine Formel der Aussagenlogik. Jede Aussage ist auch eine Formel der Aussagenlogik.
Mit den Junktoren kann man Aussagen und Formeln zu grösseren Formeln der Aussagenlogik kombinieren. Mit den Junktoren kann man Aussagen und Formeln zu grösseren Formeln der Aussagenlogik kombinieren.
Die Negation `¬(F)` einer Formel F ist auch eine Formel. Die negierte Formel ist wahr genau dann wenn (gdw) die ursprünglihe Formel falsch ist: Die Negation `¬(F)` einer Formel F ist auch eine Formel. Die negierte Formel ist wahr genau dann wenn (gdw) die ursprünglihe Formel falsch ist:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
¬(2<1) ¬(2<1)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
¬(1+1=2) ¬(1+1=2)
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In diesen Notebooks muss der Inhalt der Negation immer geklammert werden. Im Skript ist das nicht immer nötig. In diesen Notebooks muss der Inhalt der Negation immer geklammert werden. Im Skript ist das nicht immer nötig.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Konjunktion `F ∧ G` von zwei Formeln ist wahr gdw beide Formeln wahr sind: Die Konjunktion `F ∧ G` von zwei Formeln ist wahr gdw beide Formeln wahr sind:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>1 ∧ 1>0 2>1 ∧ 1>0
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>1 ∧ 1>2 2>1 ∧ 1>2
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Disjunktion `F ∨ G` von zwei Formeln ist wahr gdw mindestes eine der beiden Formeln wahr sind: Die Disjunktion `F ∨ G` von zwei Formeln ist wahr gdw mindestes eine der beiden Formeln wahr sind:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1>1 ∨ 1>2 1>1 ∨ 1>2
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>1 ∨ 3>1 2>1 ∨ 3>1
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Implikation `F ⇒ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder die erste Formel F falsch ist: Die Implikation `F ⇒ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder die erste Formel F falsch ist:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>1 ⇒ 3>1 2>1 ⇒ 3>1
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2<1 ⇒ 1+1 = 5 2<1 ⇒ 1+1 = 5
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>1 ⇒ 1+1=5 2>1 ⇒ 1+1=5
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Äquivalenz `F ⇔ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder beide Formeln falsch sind: Die Äquivalenz `F ⇔ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder beide Formeln falsch sind:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1=2 ⇔ 2=1 1=2 ⇔ 2=1
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1=3 ⇔ 1=1024 1=3 ⇔ 1=1024
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1=1 ⇔ 2=3 1=1 ⇔ 2=3
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Prioritäten ## Prioritäten
Anmerkung: Wir nehmen an, dass $\neg$ am stärksten bindet, dann kommen $\wedge$, $\vee$, $\Rightarrow$ und schließlich ⇔. Anmerkung: Wir nehmen an, dass $\neg$ am stärksten bindet, dann kommen $\wedge$, $\vee$, $\Rightarrow$ und schließlich ⇔.
Die Formel $(p \vee (\neg p \wedge q))$ steht also für $(p \vee (\neg(p) \wedge q)$. Die Formel $(p \vee (\neg p \wedge q))$ steht also für $(p \vee (\neg(p) \wedge q)$.
Eine Formel kann man immer als einen Baum sehen. Eine Formel kann man immer als einen Baum sehen.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref OPTIMIZE_AST=FALSE :pref OPTIMIZE_AST=FALSE
``` ```
%% Output %% Output
Preference changed: OPTIMIZE_AST = FALSE Preference changed: OPTIMIZE_AST = FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot formula_tree (2>3 ⇒ 4>1) ⇔ ¬(5<1) :dot formula_tree (2>3 ⇒ 4>1) ⇔ ¬(5<1)
``` ```
%% Output %% Output
<Dot visualization: formula_tree [(2>3 ⇒ 4>1) ⇔ ¬(5<1)]> <Dot visualization: formula_tree [(2>3 ⇒ 4>1) ⇔ ¬(5<1)]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Wahrheitstabellen # Wahrheitstabellen
Die Bedeutung der Junktoren der Aussagenlogik kann man in folgender Wahrheitstabelle zusammenfassen: Die Bedeutung der Junktoren der Aussagenlogik kann man in folgender Wahrheitstabelle zusammenfassen:
<img src="./img/wahrheitstabelle.png" width="600"> <img src="./img/wahrheitstabelle.png" width="600">
Wie berechnet man damit den Wahrheitswert einer Formel wie $(p \vee (\neg p \wedge q))$? Wie berechnet man damit den Wahrheitswert einer Formel wie $(p \vee (\neg p \wedge q))$?
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Interpretationen ## Interpretationen
Man braucht erst die Wahrheitswerte für die atomaren Aussagen $p$ und $q$. Man braucht erst die Wahrheitswerte für die atomaren Aussagen $p$ und $q$.
Diese Information nennt man eine **Interpretation** für die Formel. Diese Information nennt man eine **Interpretation** für die Formel.
Die Formel oben hat 4 Interpretationen, da $p$ und $q$ jeweils wahr oder falsch sein können. Die Formel oben hat 4 Interpretationen, da $p$ und $q$ jeweils wahr oder falsch sein können.
Mit einer Interpretation kann man nun Mit einer Interpretation kann man nun
* den Wahrheitswert aller (atomaren) Aussagen berechnen * den Wahrheitswert aller (atomaren) Aussagen berechnen
* und mit der Wahrheitstabelle dann den Wert von immer grösseren Unterformeln berechnen. * und mit der Wahrheitstabelle dann den Wert von immer grösseren Unterformeln berechnen.
Beispiel: Beispiel:
Sei $i$ = $\{p\mapsto \mathit{TRUE},q\mapsto \mathit{FALSE}\}$ eine Interpretation für die Formel $(p \vee (\neg p \wedge q))$. Sei $i$ = $\{p\mapsto \mathit{TRUE},q\mapsto \mathit{FALSE}\}$ eine Interpretation für die Formel $(p \vee (\neg p \wedge q))$.
* Schritt 1: alle Aussagen berechnen: $~(\mathit{TRUE} \vee (\neg \mathit{TRUE} \wedge \mathit{FALSE})$ * Schritt 1: alle Aussagen berechnen: $~(\mathit{TRUE} \vee (\neg \mathit{TRUE} \wedge \mathit{FALSE})$
* Schritt 2: $\neg \mathit{TRUE} = \mathit{FALSE}$: $~(\mathit{TRUE} \vee (\mathit{FALSE} \wedge \mathit{FALSE})$ * Schritt 2: $\neg \mathit{TRUE} = \mathit{FALSE}$: $~(\mathit{TRUE} \vee (\mathit{FALSE} \wedge \mathit{FALSE})$
* Schritt 3: $\mathit{FALSE} \wedge \mathit{FALSE} = \mathit{FALSE}$: $~(\mathit{TRUE} \vee \mathit{FALSE})$ * Schritt 3: $\mathit{FALSE} \wedge \mathit{FALSE} = \mathit{FALSE}$: $~(\mathit{TRUE} \vee \mathit{FALSE})$
* Schritt 3: $\mathit{TRUE} \vee \mathit{FALSE} = \mathit{TRUE}$: $~\mathit{TRUE}$ * Schritt 3: $\mathit{TRUE} \vee \mathit{FALSE} = \mathit{TRUE}$: $~\mathit{TRUE}$
Unter der Interpretation $i$ ist die Formel $(p \vee (\neg p \wedge q)$ wahr. Unter der Interpretation $i$ ist die Formel $(p \vee (\neg p \wedge q)$ wahr.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Modelle ## Modelle
Man nennt so eine Interpretation ein **Modell** für die Formel. Man nennt so eine Interpretation ein **Modell** für die Formel.
* eine Interpretation $i$ so dass $i(\phi)={\color{olive}{\mathit{TRUE}}}$ ist ein **Modell** für $\phi$ * eine Interpretation $i$ so dass $i(\phi)={\color{olive}{\mathit{TRUE}}}$ ist ein **Modell** für $\phi$
* eine Formel $\phi$ die mindestens ein Modell hat heißt **erfüllbar** * eine Formel $\phi$ die mindestens ein Modell hat heißt **erfüllbar**
* eine Formel $\phi$ wo alle Interpretationen auch Modelle sind wird eine **Tautologie** genannt * eine Formel $\phi$ wo alle Interpretationen auch Modelle sind wird eine **Tautologie** genannt
* eine Formel ohne Modell heißt **unerfüllbar** oder ein Widerspruch * eine Formel ohne Modell heißt **unerfüllbar** oder ein Widerspruch
Die Interpretation $i'$ = $\{p\mapsto \mathit{FALSE},q\mapsto \mathit{FALSE}\}$ ist kein Modell von $(p \vee (\neg p \wedge q))$. Die Interpretation $i'$ = $\{p\mapsto \mathit{FALSE},q\mapsto \mathit{FALSE}\}$ ist kein Modell von $(p \vee (\neg p \wedge q))$.
Die Formel ist also keine Tautologie, aber erfüllbar. Die Formel ist also keine Tautologie, aber erfüllbar.
Die Formel $p \vee \neg p$ ist eine Tautologie: alle Interpretation machen die Formel wahr. Die Formel $p \vee \neg p$ ist eine Tautologie: alle Interpretation machen die Formel wahr.
$p \wedge \neg p$ hingegen ist ein Widerspruch und hat kein Modell. $p \wedge \neg p$ hingegen ist ein Widerspruch und hat kein Modell.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Äquivalenz von Formeln # Äquivalenz von Formeln
Zwei Formeln sind **äquivalent** gdw sie die selben Modelle haben. Zwei Formeln sind **äquivalent** gdw sie die selben Modelle haben.
$(p \vee (\neg p \wedge q))$ ist zum Beispiel äquivalent zu $p \vee q$. $(p \vee (\neg p \wedge q))$ ist zum Beispiel äquivalent zu $p \vee q$.
Hier stellen wir die Interpretationen und Modelle tabellarisch dar: Hier stellen wir die Interpretationen und Modelle tabellarisch dar:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {p,q,F1,F2| p:BOOL & q:BOOL & :table {p,q,F1,F2| p:BOOL & q:BOOL &
F1=bool(p=TRUE ∨ (¬(p=TRUE) ∧ q=TRUE)) & // p ∨ (¬p ∧ q) F1=bool(p=TRUE ∨ (¬(p=TRUE) ∧ q=TRUE)) & // p ∨ (¬p ∧ q)
F2=bool(p=TRUE ∨ q=TRUE) // p ∨ q F2=bool(p=TRUE ∨ q=TRUE) // p ∨ q
} }
``` ```
%% Output %% Output
|p|q|F1|F2| |p|q|F1|F2|
|---|---|---|---| |---|---|---|---|
|FALSE|FALSE|FALSE|FALSE| |FALSE|FALSE|FALSE|FALSE|
|FALSE|TRUE|TRUE|TRUE| |FALSE|TRUE|TRUE|TRUE|
|TRUE|FALSE|TRUE|TRUE| |TRUE|FALSE|TRUE|TRUE|
|TRUE|TRUE|TRUE|TRUE| |TRUE|TRUE|TRUE|TRUE|
p q F1 F2 p q F1 F2
FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
FALSE TRUE TRUE TRUE FALSE TRUE TRUE TRUE
TRUE FALSE TRUE TRUE TRUE FALSE TRUE TRUE
TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir schreiben diesen Tatbestand als $(p \vee (\neg p \wedge q)) \equiv p \vee q$. Wir schreiben diesen Tatbestand als $(p \vee (\neg p \wedge q)) \equiv p \vee q$.
Kleine Anmerkung: das Werkzeug im Jupyter Notebook akzeptiert keine aussagenlogische Variablen sondern nur Bool'sche Datenvariablen. Anstatt $p$ muss man `p=TRUE` schreiben und anstatt $p \vee q$ muss man `p=TRUE ∨ q=TRUE` schreiben. Mit `bool(P)` konvertiert man den Wahrheitswert einer Formel in einen Bool'schen Datenwert um. Kleine Anmerkung: das Werkzeug im Jupyter Notebook akzeptiert keine aussagenlogische Variablen sondern nur Bool'sche Datenvariablen. Anstatt $p$ muss man `p=TRUE` schreiben und anstatt $p \vee q$ muss man `p=TRUE ∨ q=TRUE` schreiben. Mit `bool(P)` konvertiert man den Wahrheitswert einer Formel in einen Bool'schen Datenwert um.
$\equiv$ ist eine Relation zwischen logischen Formeln. $\equiv$ ist eine Relation zwischen logischen Formeln.
$\equiv$ ist transitiv und kommutativ. $\equiv$ ist transitiv und kommutativ.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Wichtige Äquivalenzen # Wichtige Äquivalenzen
Für alle Formeln $\phi, \psi$ der Aussagenlogik gilt: Für alle Formeln $\phi, \psi$ der Aussagenlogik gilt:
* $\phi \wedge \psi \equiv \psi \wedge \phi$ (Kommutativität) * $\phi \wedge \psi \equiv \psi \wedge \phi$ (Kommutativität)
* $\phi \vee \psi \equiv \psi \vee \phi$ (Kommutativität) * $\phi \vee \psi \equiv \psi \vee \phi$ (Kommutativität)
Mit diesen Regeln kann man $\Rightarrow$ und $\Leftrightarrow$ umwandeln: Mit diesen Regeln kann man $\Rightarrow$ und $\Leftrightarrow$ umwandeln:
* $\phi \Rightarrow \psi \equiv (\neg \phi) \vee \psi$ * $\phi \Rightarrow \psi \equiv (\neg \phi) \vee \psi$
* $\phi \Leftrightarrow \psi \equiv (\phi \Rightarrow \psi) \wedge (\psi \Rightarrow \phi)$ * $\phi \Leftrightarrow \psi \equiv (\phi \Rightarrow \psi) \wedge (\psi \Rightarrow \phi)$
Mit diesen Regeln kann man die Negation zu den atomaren Aussagen verschieben: Mit diesen Regeln kann man die Negation zu den atomaren Aussagen verschieben:
* $\neg \neg \phi \equiv \phi$ * $\neg \neg \phi \equiv \phi$
* $\neg(\phi \wedge \psi) \equiv (\neg \phi) \vee (\neg \psi)$ (De Morgan) * $\neg(\phi \wedge \psi) \equiv (\neg \phi) \vee (\neg \psi)$ (De Morgan)
* $\neg(\phi \vee \psi) \equiv (\neg \phi) \wedge (\neg \psi)$ (De Morgan) * $\neg(\phi \vee \psi) \equiv (\neg \phi) \wedge (\neg \psi)$ (De Morgan)
Hier illustrieren wir die Äquivalenz $\neg(\phi \vee \psi) \equiv (\neg \phi) \wedge (\neg \psi)$ als Wahrheitstabelle: Hier illustrieren wir die Äquivalenz $\neg(\phi \vee \psi) \equiv (\neg \phi) \wedge (\neg \psi)$ als Wahrheitstabelle:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {p,q,ODER,NODER,NUND,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) & :table {p,q,ODER,NODER,NUND,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &
ODER=bool(p=TRUE ∨ q=TRUE) & ODER=bool(p=TRUE ∨ q=TRUE) &
NODER = bool(¬(ODER=TRUE)) & NODER = bool(¬(ODER=TRUE)) &
NUND=bool((np=TRUE) ∧ (nq=TRUE))} NUND=bool((np=TRUE) ∧ (nq=TRUE))}
``` ```
%% Output %% Output
|p|q|ODER|NODER|NUND|np|nq| |p|q|ODER|NODER|NUND|np|nq|
|---|---|---|---|---|---|---| |---|---|---|---|---|---|---|
|FALSE|FALSE|FALSE|TRUE|TRUE|TRUE|TRUE| |FALSE|FALSE|FALSE|TRUE|TRUE|TRUE|TRUE|
|FALSE|TRUE|TRUE|FALSE|FALSE|TRUE|FALSE| |FALSE|TRUE|TRUE|FALSE|FALSE|TRUE|FALSE|
|TRUE|FALSE|TRUE|FALSE|FALSE|FALSE|TRUE| |TRUE|FALSE|TRUE|FALSE|FALSE|FALSE|TRUE|
|TRUE|TRUE|TRUE|FALSE|FALSE|FALSE|FALSE| |TRUE|TRUE|TRUE|FALSE|FALSE|FALSE|FALSE|
p q ODER NODER NUND np nq p q ODER NODER NUND np nq
FALSE FALSE FALSE TRUE TRUE TRUE TRUE FALSE FALSE FALSE TRUE TRUE TRUE TRUE
FALSE TRUE TRUE FALSE FALSE TRUE FALSE FALSE TRUE TRUE FALSE FALSE TRUE FALSE
TRUE FALSE TRUE FALSE FALSE FALSE TRUE TRUE FALSE TRUE FALSE FALSE FALSE TRUE
TRUE TRUE TRUE FALSE FALSE FALSE FALSE TRUE TRUE TRUE FALSE FALSE FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Kontraposition ## Kontraposition
$\neg \psi \Rightarrow \neg \phi$ ist die Kontraposition von $\phi \Rightarrow \psi$. $\neg \psi \Rightarrow \neg \phi$ ist die Kontraposition von $\phi \Rightarrow \psi$.
Ist diese Form äquivalent? Ist diese Form äquivalent?
Zur Prüfung kann man die komplette Wahrheitstabelle aufbauen, mit allen möglichen Werten für die "offenen" Formeln $\phi$, $\psi$ Zur Prüfung kann man die komplette Wahrheitstabelle aufbauen, mit allen möglichen Werten für die "offenen" Formeln $\phi$, $\psi$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {p,q,IMPL,KONT,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) & :table {p,q,IMPL,KONT,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &
IMPL=bool(p=TRUE => q=TRUE) & IMPL=bool(p=TRUE => q=TRUE) &
KONT=bool((nq=TRUE) => (np=TRUE))} KONT=bool((nq=TRUE) => (np=TRUE))}
``` ```
%% Output %% Output
|p|q|IMPL|KONT|np|nq| |p|q|IMPL|KONT|np|nq|
|---|---|---|---|---|---| |---|---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE|TRUE| |FALSE|FALSE|TRUE|TRUE|TRUE|TRUE|
|FALSE|TRUE|TRUE|TRUE|TRUE|FALSE| |FALSE|TRUE|TRUE|TRUE|TRUE|FALSE|
|TRUE|FALSE|FALSE|FALSE|FALSE|TRUE| |TRUE|FALSE|FALSE|FALSE|FALSE|TRUE|
|TRUE|TRUE|TRUE|TRUE|FALSE|FALSE| |TRUE|TRUE|TRUE|TRUE|FALSE|FALSE|
p q IMPL KONT np nq p q IMPL KONT np nq
FALSE FALSE TRUE TRUE TRUE TRUE FALSE FALSE TRUE TRUE TRUE TRUE
FALSE TRUE TRUE TRUE TRUE FALSE FALSE TRUE TRUE TRUE TRUE FALSE
TRUE FALSE FALSE FALSE FALSE TRUE TRUE FALSE FALSE FALSE FALSE TRUE
TRUE TRUE TRUE TRUE FALSE FALSE TRUE TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Es gilt also: Es gilt also:
$\phi \Rightarrow \psi$ $\equiv$ $\neg \psi \Rightarrow \neg \phi$. $\phi \Rightarrow \psi$ $\equiv$ $\neg \psi \Rightarrow \neg \phi$.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Logisches Schließen # Logisches Schließen
Wenn $p \wedge q$ gilt, dann ist $p$ eine logische Konsequenz (Schlussfolgerung) von $p\wedge q$. Wenn $p \wedge q$ gilt, dann ist $p$ eine logische Konsequenz (Schlussfolgerung) von $p\wedge q$.
* Wir schreiben dies als $p \wedge q \models p$ * Wir schreiben dies als $p \wedge q \models p$
* Formal bedeutet dies, dass alle Modelle von $p \wedge q$ auch Modelle von $p$ sind. * Formal bedeutet dies, dass alle Modelle von $p \wedge q$ auch Modelle von $p$ sind.
Die Tabelle zeigt, dass $p \Leftrightarrow q \models p \Rightarrow q$. Die Tabelle zeigt, dass $p \Leftrightarrow q \models p \Rightarrow q$.
Die beiden Formeln sind nicht äquivalent. Die beiden Formeln sind nicht äquivalent.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {p,q,F1,F2| p:BOOL & q:BOOL & F1=bool(p=TRUE ⇔ q=TRUE) & F2=bool(p=TRUE ⇒ q=TRUE)} :table {p,q,F1,F2| p:BOOL & q:BOOL & F1=bool(p=TRUE ⇔ q=TRUE) & F2=bool(p=TRUE ⇒ q=TRUE)}
``` ```
%% Output %% Output
|p|q|F1|F2| |p|q|F1|F2|
|---|---|---|---| |---|---|---|---|
|FALSE|FALSE|TRUE|TRUE| |FALSE|FALSE|TRUE|TRUE|
|FALSE|TRUE|FALSE|TRUE| |FALSE|TRUE|FALSE|TRUE|
|TRUE|FALSE|FALSE|FALSE| |TRUE|FALSE|FALSE|FALSE|
|TRUE|TRUE|TRUE|TRUE| |TRUE|TRUE|TRUE|TRUE|
p q F1 F2 p q F1 F2
FALSE FALSE TRUE TRUE FALSE FALSE TRUE TRUE
FALSE TRUE FALSE TRUE FALSE TRUE FALSE TRUE
TRUE FALSE FALSE FALSE TRUE FALSE FALSE FALSE
TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Wichtige logische Schlussfolgerungen # Wichtige logische Schlussfolgerungen
Für alle Formeln $\phi, \psi$ gilt: Für alle Formeln $\phi, \psi$ gilt:
* $\phi \wedge \psi \models \phi$ * $\phi \wedge \psi \models \phi$
* $(\phi \Rightarrow \psi) \wedge \phi \models \psi$ (Modus Ponens) * $(\phi \Rightarrow \psi) \wedge \phi \models \psi$ (Modus Ponens)
* $(\phi \Rightarrow \psi) \wedge \neg\psi \models \neg\phi$ (Modus Tollens) * $(\phi \Rightarrow \psi) \wedge \neg\psi \models \neg\phi$ (Modus Tollens)
Beispiel: $\phi$ = "Es regnet", $\psi$ = "Die Straße wird nass". Beispiel: $\phi$ = "Es regnet", $\psi$ = "Die Straße wird nass".
* $(\phi \Leftrightarrow \psi) \wedge \psi \models \phi$ * $(\phi \Leftrightarrow \psi) \wedge \psi \models \phi$
* $(\phi \Leftrightarrow \psi) \wedge \neg\psi \models \neg\phi$ * $(\phi \Leftrightarrow \psi) \wedge \neg\psi \models \neg\phi$
Achtung $\phi \wedge \neg \phi \models \psi$ für beliebiges $\psi$! Achtung $\phi \wedge \neg \phi \models \psi$ für beliebiges $\psi$!
Also: Also:
* $1>2 \models 1+1=100$ * $1>2 \models 1+1=100$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Smullyan - Einfaches Puzzle # Smullyan - Einfaches Puzzle
Raymond Smullyan beschreibt in seinen Büchern eine Insel auf der es (nur) zwei Arten von Personen gibt: Raymond Smullyan beschreibt in seinen Büchern eine Insel auf der es (nur) zwei Arten von Personen gibt:
* Ritter, die immer die Wahrheit sagen, und * Ritter, die immer die Wahrheit sagen, und
* Schurken, die immer lügen. * Schurken, die immer lügen.
Hier ist ein Puzzle aus einem seiner Bücher: Hier ist ein Puzzle aus einem seiner Bücher:
* X sagt: "Y ist ein Ritter" * X sagt: "Y ist ein Ritter"
* Y sagt: "X und ich sind von einem unterschiedlichen Typ" * Y sagt: "X und ich sind von einem unterschiedlichen Typ"
Können wir bestimmen ob X und Y Ritter oder Schurken sind? Können wir bestimmen ob X und Y Ritter oder Schurken sind?
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Lösen des Puzzles ## Lösen des Puzzles
Schritt 1: was sind die Aussagen? Schritt 1: was sind die Aussagen?
* $X$: die Person X ist ein Ritter * $X$: die Person X ist ein Ritter
* $Y$: die Person Y ist ein Ritter * $Y$: die Person Y ist ein Ritter
Schritt 2: Übersetzung der Informationen in Aussagenlogik Schritt 2: Übersetzung der Informationen in Aussagenlogik
* $\mathit{X} \Leftrightarrow \mathit{Y}$ ist die Übersetzung von: * $\mathit{X} \Leftrightarrow \mathit{Y}$ ist die Übersetzung von:
* X sagt: "Y ist ein Ritter" * X sagt: "Y ist ein Ritter"
* $\mathit{Y} \Leftrightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von: * $\mathit{Y} \Leftrightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von:
* Y sagt: "X und ich sind von einem unterschiedlichen Typ" * Y sagt: "X und ich sind von einem unterschiedlichen Typ"
Schritt 3: Bestimmung der Modelle: Schritt 3: Bestimmung der Modelle:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & :table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇔ y=TRUE) & S1=bool(x=TRUE ⇔ y=TRUE) &
S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) & S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE)} Puzzle=bool(S1=TRUE & S2=TRUE)}
``` ```
%% Output %% Output
|x|y|S1|S2|Puzzle| |x|y|S1|S2|Puzzle|
|---|---|---|---|---| |---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE| |FALSE|FALSE|TRUE|TRUE|TRUE|
|FALSE|TRUE|FALSE|TRUE|FALSE| |FALSE|TRUE|FALSE|TRUE|FALSE|
|TRUE|FALSE|FALSE|FALSE|FALSE| |TRUE|FALSE|FALSE|FALSE|FALSE|
|TRUE|TRUE|TRUE|FALSE|FALSE| |TRUE|TRUE|TRUE|FALSE|FALSE|
x y S1 S2 Puzzle x y S1 S2 Puzzle
FALSE FALSE TRUE TRUE TRUE FALSE FALSE TRUE TRUE TRUE
FALSE TRUE FALSE TRUE FALSE FALSE TRUE FALSE TRUE FALSE
TRUE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE FALSE
TRUE TRUE TRUE FALSE FALSE TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Unser Puzzle hat nur ein einziges Modell und beide Personen sind also Schurken. Unser Puzzle hat nur ein einziges Modell und beide Personen sind also Schurken.
Ein typische fehlerhafte Übersetzung des Puzzles ist diese: Ein typische fehlerhafte Übersetzung des Puzzles ist diese:
* $\mathit{X} \Rightarrow \mathit{Y}$ ist die Übersetzung von: * $\mathit{X} \Rightarrow \mathit{Y}$ ist die Übersetzung von:
* X sagt: "Y ist ein Ritter" * X sagt: "Y ist ein Ritter"
* $\mathit{Y} \Rightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von: * $\mathit{Y} \Rightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von:
* Y sagt: "X und ich sind von einem unterschiedlichen Typ" * Y sagt: "X und ich sind von einem unterschiedlichen Typ"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & :table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇒ y=TRUE) & S1=bool(x=TRUE ⇒ y=TRUE) &
S2=bool(y=TRUE ⇒ (x=TRUE ⇔ ¬(y=TRUE))) & S2=bool(y=TRUE ⇒ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE)} Puzzle=bool(S1=TRUE & S2=TRUE)}
``` ```
%% Output %% Output
|x|y|S1|S2|Puzzle| |x|y|S1|S2|Puzzle|
|---|---|---|---|---| |---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE| |FALSE|FALSE|TRUE|TRUE|TRUE|
|FALSE|TRUE|TRUE|TRUE|TRUE| |FALSE|TRUE|TRUE|TRUE|TRUE|
|TRUE|FALSE|FALSE|TRUE|FALSE| |TRUE|FALSE|FALSE|TRUE|FALSE|
|TRUE|TRUE|TRUE|FALSE|FALSE| |TRUE|TRUE|TRUE|FALSE|FALSE|
x y S1 S2 Puzzle x y S1 S2 Puzzle
FALSE FALSE TRUE TRUE TRUE FALSE FALSE TRUE TRUE TRUE
FALSE TRUE TRUE TRUE TRUE FALSE TRUE TRUE TRUE TRUE
TRUE FALSE FALSE TRUE FALSE TRUE FALSE FALSE TRUE FALSE
TRUE TRUE TRUE FALSE FALSE TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Diese Übersetzung erlaubt zwei Modelle, und auch eine fehlerhafte "Lösung" mit X als Schurken und Y als Ritter. Diese Lösung ist falsch, da X und Y die Wahrheit sagen, aber nur Y ein Ritter ist. Diese Übersetzung erlaubt zwei Modelle, und auch eine fehlerhafte "Lösung" mit X als Schurken und Y als Ritter. Diese Lösung ist falsch, da X und Y die Wahrheit sagen, aber nur Y ein Ritter ist.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Beweis durch Widerspruch # Beweis durch Widerspruch
* Theorem: $\phi \models \psi$ genau dann wenn $\phi \wedge \neg \psi$ kein Modell hat * Theorem: $\phi \models \psi$ genau dann wenn $\phi \wedge \neg \psi$ kein Modell hat
Beweis (ist ein Äquivalenzbeweis auf Metaebene): Beweis (ist ein Äquivalenzbeweis auf Metaebene):
* $\phi \models \psi$ * $\phi \models \psi$
* $\Longleftrightarrow$ alle Modelle von $\phi$ sind auch Modelle von $\psi$ (per Definition von $\models$) * $\Longleftrightarrow$ alle Modelle von $\phi$ sind auch Modelle von $\psi$ (per Definition von $\models$)
* $\Longleftrightarrow$ in allen Modellen von $\phi$ hat $\neg \psi$ den Wahrheitswert falsch (per Definition von $\neg$) * $\Longleftrightarrow$ in allen Modellen von $\phi$ hat $\neg \psi$ den Wahrheitswert falsch (per Definition von $\neg$)
* $\Longleftrightarrow$ alle Modelle von $\phi$ sind kein Modell von $\phi \wedge \neg \psi$ (per Definition von $\wedge$) * $\Longleftrightarrow$ alle Modelle von $\phi$ sind kein Modell von $\phi \wedge \neg \psi$ (per Definition von $\wedge$)
* $\Longleftrightarrow$ $\phi \wedge \neg \psi$ hat kein Modell (da auch kein Modell von $\neg \phi$ ein Modell von $\phi \wedge \neg \psi$ sein kann) * $\Longleftrightarrow$ $\phi \wedge \neg \psi$ hat kein Modell (da auch kein Modell von $\neg \phi$ ein Modell von $\phi \wedge \neg \psi$ sein kann)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Anwendung auf unser Puzzle: Anwendung auf unser Puzzle:
* Sei $\phi$ = $(\mathit{X} \Leftrightarrow \mathit{Y}) \wedge (\mathit{Y} \Leftrightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y})))$ * Sei $\phi$ = $(\mathit{X} \Leftrightarrow \mathit{Y}) \wedge (\mathit{Y} \Leftrightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y})))$
* Sei $\psi$ = $\neg X \wedge \neg Y$ (X und Y sind Schurken) * Sei $\psi$ = $\neg X \wedge \neg Y$ (X und Y sind Schurken)
* Wir haben $\phi \models \psi$ und * Wir haben $\phi \models \psi$ und
* $\phi \wedge \neg \psi$ ist ein Widerspruch: * $\phi \wedge \neg \psi$ ist ein Widerspruch:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {x,y,S1,S2,Puzzle,WS | x:BOOL & y:BOOL & :table {x,y,S1,S2,Puzzle,WS | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇔ y=TRUE) & S1=bool(x=TRUE ⇔ y=TRUE) &
S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) & S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE) & Puzzle=bool(S1=TRUE & S2=TRUE) &
WS=bool(Puzzle=TRUE & not( not(x=TRUE) & not(y=TRUE)))} WS=bool(Puzzle=TRUE & not( not(x=TRUE) & not(y=TRUE)))}
``` ```
%% Output %% Output
|x|y|S1|S2|Puzzle|WS| |x|y|S1|S2|Puzzle|WS|
|---|---|---|---|---|---| |---|---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE|FALSE| |FALSE|FALSE|TRUE|TRUE|TRUE|FALSE|
|FALSE|TRUE|FALSE|TRUE|FALSE|FALSE| |FALSE|TRUE|FALSE|TRUE|FALSE|FALSE|
|TRUE|FALSE|FALSE|FALSE|FALSE|FALSE| |TRUE|FALSE|FALSE|FALSE|FALSE|FALSE|
|TRUE|TRUE|TRUE|FALSE|FALSE|FALSE| |TRUE|TRUE|TRUE|FALSE|FALSE|FALSE|
x y S1 S2 Puzzle WS x y S1 S2 Puzzle WS
FALSE FALSE TRUE TRUE TRUE FALSE FALSE FALSE TRUE TRUE TRUE FALSE
FALSE TRUE FALSE TRUE FALSE FALSE FALSE TRUE FALSE TRUE FALSE FALSE
TRUE FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE FALSE FALSE
TRUE TRUE TRUE FALSE FALSE FALSE TRUE TRUE TRUE FALSE FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Widerspruchsbeweise werden wir oft im Verlauf der Vorlesung verwenden. Widerspruchsbeweise werden wir oft im Verlauf der Vorlesung verwenden.
Es gibt zwei andere Arten von Beweisen: Äquivalenzbeweise und Deduktionsbeweise. Es gibt zwei andere Arten von Beweisen: Äquivalenzbeweise und Deduktionsbeweise.
# Äquivalenzbeweis # Äquivalenzbeweis
Hier schreiben wir die Schritte des Beweises oft in folgender Form auf: Hier schreiben wir die Schritte des Beweises oft in folgender Form auf:
* $\phi_1$ * $\phi_1$
* $\Longleftrightarrow$ $\phi_2$ * $\Longleftrightarrow$ $\phi_2$
* ... * ...
* $\Longleftrightarrow$ $\phi_k$ * $\Longleftrightarrow$ $\phi_k$
wobei immer gilt $\phi_i \equiv \phi_{i+1}$. wobei immer gilt $\phi_i \equiv \phi_{i+1}$.
Wir haben per Transitivität von $\equiv$, dass $\phi_1 \equiv \phi_k$. Wir haben per Transitivität von $\equiv$, dass $\phi_1 \equiv \phi_k$.
Da $\equiv$ auch kommutativ ist, gilt der Beweis auch in die andere Richtung: $\phi_k \equiv \phi_1$. Da $\equiv$ auch kommutativ ist, gilt der Beweis auch in die andere Richtung: $\phi_k \equiv \phi_1$.
Wir haben sowohl $\phi_1 \models \phi_k$ als auch $\phi_k \models \phi_1$. Wir haben sowohl $\phi_1 \models \phi_k$ als auch $\phi_k \models \phi_1$.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Als kleines Beispiel beweisen wir, dass $\neg b \Rightarrow a \equiv a \vee b$: Als kleines Beispiel beweisen wir, dass $\neg b \Rightarrow a \equiv a \vee b$:
* $\neg b \Rightarrow a$ * $\neg b \Rightarrow a$
* $\Longleftrightarrow$ $\neg \neg b \vee a$ (Regel: $\phi \Rightarrow \psi \equiv \neg \phi \vee \psi$) * $\Longleftrightarrow$ $\neg \neg b \vee a$ (Regel: $\phi \Rightarrow \psi \equiv \neg \phi \vee \psi$)
* $\Longleftrightarrow$ $b \vee a$ (Regel: $\neg \neg \phi \equiv \phi$)) * $\Longleftrightarrow$ $b \vee a$ (Regel: $\neg \neg \phi \equiv \phi$))
* $\Longleftrightarrow$ $a \vee b$ (Kommutativität von $\vee$) * $\Longleftrightarrow$ $a \vee b$ (Kommutativität von $\vee$)
Anmerkung: im Skript verwenden wir $\Longleftrightarrow$ für Äquivalenzbeweise; die "präzise" logische Schreibweise wäre $\equiv$. Anmerkung: im Skript verwenden wir $\Longleftrightarrow$ für Äquivalenzbeweise; die "präzise" logische Schreibweise wäre $\equiv$.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Deduktiver Beweis # Deduktiver Beweis
Hier schreiben wir die Schritte des Beweises oft in folgender Form auf: Hier schreiben wir die Schritte des Beweises oft in folgender Form auf:
* $\phi_1$ * $\phi_1$
* $\phi_2$ * $\phi_2$
* ... * ...
* $\phi_k$ * $\phi_k$
wobei immer gilt $\phi_1 \wedge ...\phi_i \models \phi_{i+1}$. wobei immer gilt $\phi_1 \wedge ...\phi_i \models \phi_{i+1}$.
Wir haben per Transitiviät von $\models$, dass $\phi_1 \models \phi_k$. Wir haben per Transitiviät von $\models$, dass $\phi_1 \models \phi_k$.
Aber im Gegensatz zum Äquivalenzbeweis gilt hier generell nicht $\phi_k \models \phi_1$! Aber im Gegensatz zum Äquivalenzbeweis gilt hier generell nicht $\phi_k \models \phi_1$!
Dieser Beweis kann nicht umgekehrt werden. Dieser Beweis kann nicht umgekehrt werden.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir illustrieren dies Art der Beweisführung mit einem anderen kleinen Puzzle von unserer Insel der Ritter und Schurken: Wir illustrieren dies Art der Beweisführung mit einem anderen kleinen Puzzle von unserer Insel der Ritter und Schurken:
* A sagt: "B ist ein Ritter" * A sagt: "B ist ein Ritter"
* B sagt: "1+1=3" * B sagt: "1+1=3"
* $\phi_1$ = $A \Leftrightarrow B$ $\wedge$ $B \Leftrightarrow \mathit{FALSE}$ * $\phi_1$ = $A \Leftrightarrow B$ $\wedge$ $B \Leftrightarrow \mathit{FALSE}$
* $\neg B$ (nach der zweiten Aussage $B \Leftrightarrow \mathit{FALSE}$ muss B ein Schurke sein) * $\neg B$ (nach der zweiten Aussage $B \Leftrightarrow \mathit{FALSE}$ muss B ein Schurke sein)
* $\neg A$ (nach der ersten Aussage $A \Leftrightarrow B$ muss A demnach auch ein Schurke sein) * $\neg A$ (nach der ersten Aussage $A \Leftrightarrow B$ muss A demnach auch ein Schurke sein)
Wir haben per Transitiviät, dass $\phi_1 \models \neg A$, d.h. es folgt aus dem Puzzle, dass A ein Schurke ist. Wir haben per Transitiviät, dass $\phi_1 \models \neg A$, d.h. es folgt aus dem Puzzle, dass A ein Schurke ist.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Aristoteles: Anfänge der Logik # Aristoteles: Anfänge der Logik
Die [Syllogistik](https://de.wikipedia.org/wiki/Syllogismus), einer Vorform der Prädikatenlogik, geht auf Aristoteles zurück. Die [Syllogistik](https://de.wikipedia.org/wiki/Syllogismus), einer Vorform der Prädikatenlogik, geht auf Aristoteles zurück.
Was ist der Zusammenhang zwischen folgenden vier Aussagen, unter der Annahme, dass es mindestens einen Mensch gibt? Was ist der Zusammenhang zwischen folgenden vier Aussagen, unter der Annahme, dass es mindestens einen Mensch gibt?
(In die Aussagenlogik sind alle vier Aussagen unabhängig.) (In die Aussagenlogik sind alle vier Aussagen unabhängig.)
1. Alle Menschen sind sterblich. 1. Alle Menschen sind sterblich.
2. Einige Menschen sind sterblich. 2. Einige Menschen sind sterblich.
3. Alle Menschen sind unsterblich. 3. Alle Menschen sind unsterblich.
4. Einige Menschen sind unsterblich. 4. Einige Menschen sind unsterblich.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Prädikatenlogik # Prädikatenlogik
Im Vergleich zur Aussagenlogik mit den Wahrheitswerten und Aussagen, gibt es in der Prädikatenlogik: Im Vergleich zur Aussagenlogik mit den Wahrheitswerten und Aussagen, gibt es in der Prädikatenlogik:
* **Objekte** * **Objekte**
* **Konstanten** und **Variablen** die Objekte darstellen, * **Konstanten** und **Variablen** die Objekte darstellen,
* **Funktionen** die Objekte auf Objekte abbilden, * **Funktionen** die Objekte auf Objekte abbilden,
* **Prädikate** die Objekte oder Objekt-kombinationen auf einen Wahrheitswert abbilden, * **Prädikate** die Objekte oder Objekt-kombinationen auf einen Wahrheitswert abbilden,
* **Quantoren** mit denen man Variablen einführt und Aussagen über alle Objekte machen kann, oder die Existenz eines Objekts zusichert * **Quantoren** mit denen man Variablen einführt und Aussagen über alle Objekte machen kann, oder die Existenz eines Objekts zusichert
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Erläuterung: Erläuterung:
* `2+2 < 5` ist eine Aussage * `2+2 < 5` ist eine Aussage
* `2` und `5` sind **Konstanten**: sie stellen keinen Wahrheitswert dar, sondern ein Objekt (hier eine Zahl) * `2` und `5` sind **Konstanten**: sie stellen keinen Wahrheitswert dar, sondern ein Objekt (hier eine Zahl)
* `+` ist eine **Funktion**: sie bekommt Objekte als Parameter und stellt ein Objekt dar. `2+2` stellt die Zahl `4` dar. * `+` ist eine **Funktion**: sie bekommt Objekte als Parameter und stellt ein Objekt dar. `2+2` stellt die Zahl `4` dar.
* `x < 5` falls der Wert von $x$ nicht bestimmt ist, ist dies keine Aussage, der Wahrheitswert hängt von dem Wert der Variable `x` ab * `x < 5` falls der Wert von $x$ nicht bestimmt ist, ist dies keine Aussage, der Wahrheitswert hängt von dem Wert der Variable `x` ab
* `x < 5` ist ein **Prädikat**, für jeden möglichen Wert von `x` können wir bestimmen ob das Prädikat wahr oder falsch ist * `x < 5` ist ein **Prädikat**, für jeden möglichen Wert von `x` können wir bestimmen ob das Prädikat wahr oder falsch ist
* Prädikate sind parametrisierte Aussagen * Prädikate sind parametrisierte Aussagen
Weitere Beispiele: Weitere Beispiele:
* `<` ist ein **binäres Prädikat**, für jede Kombination an Werten können wir bestimmen ob das Prädikat wahr oder falsch ist: * `<` ist ein **binäres Prädikat**, für jede Kombination an Werten können wir bestimmen ob das Prädikat wahr oder falsch ist:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {x,y,res | x:1..2 & y:1..3 & res=bool(x<y)} :table {x,y,res | x:1..2 & y:1..3 & res=bool(x<y)}
``` ```
%% Output %% Output
|x|y|res| |x|y|res|
|---|---|---| |---|---|---|
|1|1|FALSE| |1|1|FALSE|
|1|2|TRUE| |1|2|TRUE|
|1|3|TRUE| |1|3|TRUE|
|2|1|FALSE| |2|1|FALSE|
|2|2|FALSE| |2|2|FALSE|
|2|3|TRUE| |2|3|TRUE|
x y res x y res
1 1 FALSE 1 1 FALSE
1 2 TRUE 1 2 TRUE
1 3 TRUE 1 3 TRUE
2 1 FALSE 2 1 FALSE
2 2 FALSE 2 2 FALSE
2 3 TRUE 2 3 TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Freie Variablen # Freie Variablen
Die Formel `x<5` besteht formal gesehen aus: Die Formel `x<5` besteht formal gesehen aus:
* einer logischen Variable $x$, * einer logischen Variable $x$,
* der Konstante $5$ die für die Zahl $5$ steht, * der Konstante $5$ die für die Zahl $5$ steht,
* dem binären Prädikatensymbol $<$, hier in Infix-Notation, mit zwei Argumenten: $x$ und $5$. (In Präfix-Notation würde man $<(x,5)$ schreiben.) * dem binären Prädikatensymbol $<$, hier in Infix-Notation, mit zwei Argumenten: $x$ und $5$. (In Präfix-Notation würde man $<(x,5)$ schreiben.)
Innerhalb von `x<5` ist $x$ eine freie Variable. Innerhalb von `x<5` ist $x$ eine freie Variable.
In einer **geschlossenen** Formel der Prädikatenlogik müssen alle Variablen durch Quantoren gebunden werden. In einer **geschlossenen** Formel der Prädikatenlogik müssen alle Variablen durch Quantoren gebunden werden.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Quantoren # Quantoren
In der Prädikatenlogik gibt es zwei Quantoren: In der Prädikatenlogik gibt es zwei Quantoren:
* den **Existenzquantor** $\exists$ * den **Existenzquantor** $\exists$
$\exists x. P$ ist wahr, wenn es mindestens ein Objekt $o$ gibt, so dass wenn man $x$ durch $o$ in $P$ ersetzt die Formel (ohne den Quantor) wahr ist $\exists x. P$ ist wahr, wenn es mindestens ein Objekt $o$ gibt, so dass wenn man $x$ durch $o$ in $P$ ersetzt die Formel (ohne den Quantor) wahr ist
* den **Allquantor** $\forall$ (auch Universalquantor genannt) * den **Allquantor** $\forall$ (auch Universalquantor genannt)
$\forall x. P$ ist wahr wenn die Formel $P$ für alle möglichen Ersetzungen von $x$ durch ein Objekt $o$ wahr ist $\forall x. P$ ist wahr wenn die Formel $P$ für alle möglichen Ersetzungen von $x$ durch ein Objekt $o$ wahr ist
* $\exists x. x<5$ ist eine geschlossene Formel (aka eine Aussage). Mit der Standardinterpretation von $<$ und $5$ ist diese Formel wahr; eine Lösung ist $x=4$. * $\exists x. x<5$ ist eine geschlossene Formel (aka eine Aussage). Mit der Standardinterpretation von $<$ und $5$ ist diese Formel wahr; eine Lösung ist $x=4$.
* $\forall x. x<5$ ist auch eine geschlossene Formel. * $\forall x. x<5$ ist auch eine geschlossene Formel.
Mit der Standardinterpretation von $<$ und $5$ ist diese Formel falsch. Ein Gegenbeispiel ist $x=5$. Mit der Standardinterpretation von $<$ und $5$ ist diese Formel falsch. Ein Gegenbeispiel ist $x=5$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∃x.(x<5) ∃x.(x<5)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = 0$ * $\mathit{x} = 0$
TRUE TRUE
Solution: Solution:
x = 0 x = 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In diesem Jupyter Notebook werden automatisch Existenzquantoren für alle offenen Variablen eingefügt: In diesem Jupyter Notebook werden automatisch Existenzquantoren für alle offenen Variablen eingefügt:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x<5 x<5
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = 0$ * $\mathit{x} = 0$
TRUE TRUE
Solution: Solution:
x = 0 x = 0
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x+20 = 30 x+20 = 30
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = 10$ * $\mathit{x} = 10$
TRUE TRUE
Solution: Solution:
x = 10 x = 10
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x*x = 10000 x*x = 10000
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = -100$ * $\mathit{x} = -100$
TRUE TRUE
Solution: Solution:
x = −100 x = −100
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Logische Äquivalenz, Schlussfolgerung # Logische Äquivalenz, Schlussfolgerung
Diese beiden Definitionen übernehmen wir wortwörtlich aus der Aussagenlogik: Diese beiden Definitionen übernehmen wir wortwörtlich aus der Aussagenlogik:
* Zwei Formeln $\phi$ und $\psi$ sind **äquivalent** gdw sie die selben Modelle haben. * Zwei Formeln $\phi$ und $\psi$ sind **äquivalent** gdw sie die selben Modelle haben.
* Wir schreiben dies als $\phi \equiv \psi$. * Wir schreiben dies als $\phi \equiv \psi$.
* Eine Formel $\psi$ ist eine **logische Schlussfolgerung** von $\phi$, wenn alle Modelle von $\phi$ auch Modelle von $\psi$ sind. * Eine Formel $\psi$ ist eine **logische Schlussfolgerung** von $\phi$, wenn alle Modelle von $\phi$ auch Modelle von $\psi$ sind.
* Wir schreiben dies als $\phi \models \psi$. * Wir schreiben dies als $\phi \models \psi$.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Das Konzept der Modelle ist aber in Prädikatenlogik komplizierter: Das Konzept der Modelle ist aber in Prädikatenlogik komplizierter:
* eine Menge an Objekten muss ausgewählt werden * eine Menge an Objekten muss ausgewählt werden
* die Konstanten und Funktionen müssen den Objekten zugeordnet werden * die Konstanten und Funktionen müssen den Objekten zugeordnet werden
* die Prädikate müssen Objekte auf Wahrheitswerte abbilden; Aussagen sind ein Spezialfall von Prädikaten. * die Prädikate müssen Objekte auf Wahrheitswerte abbilden; Aussagen sind ein Spezialfall von Prädikaten.
* (manchmal sind bestimmte Symbole vordefiniert, wie $<$, $+$ oder $5$) * (manchmal sind bestimmte Symbole vordefiniert, wie $<$, $+$ oder $5$)
Dies ist nicht Inhalt dieser Vorlesung. Dies ist nicht Inhalt dieser Vorlesung.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Quantoren: Einige Gesetze der Prädikatenlogik # Quantoren: Einige Gesetze der Prädikatenlogik
Mit diesen beiden Gesetzen kann man die Negation zu den atomaren Aussagen und Prädikaten verschieben: Mit diesen beiden Gesetzen kann man die Negation zu den atomaren Aussagen und Prädikaten verschieben:
* $\neg \exists x. P \equiv \forall x. \neg P$ * $\neg \exists x. P \equiv \forall x. \neg P$
* $\neg \exists x. (x>0 \wedge x<0) \equiv \forall x. \neg (x>0 \wedge x<0) \equiv$ $\forall x. (x\leq 0 \vee x\geq 0)$ * $\neg \exists x. (x>0 \wedge x<0) \equiv \forall x. \neg (x>0 \wedge x<0) \equiv$ $\forall x. (x\leq 0 \vee x\geq 0)$
* $\neg \forall x. P \equiv \exists x. \neg P$ * $\neg \forall x. P \equiv \exists x. \neg P$
Diese Gesetze erlauben es einem Quantoren zu vertauschen: Diese Gesetze erlauben es einem Quantoren zu vertauschen:
* $\forall x.( \forall y. P) \equiv \forall y.( \forall x. P)$ * $\forall x.( \forall y. P) \equiv \forall y.( \forall x. P)$
* Beispiel: $\forall x. (\forall y. (x \leq y \vee x>y)) \equiv \forall y. (\forall x. (x \leq y \vee x>y))$ * Beispiel: $\forall x. (\forall y. (x \leq y \vee x>y)) \equiv \forall y. (\forall x. (x \leq y \vee x>y))$
* $\exists x.( \exists y. P) \equiv \exists y.( \exists x. P)$ * $\exists x.( \exists y. P) \equiv \exists y.( \exists x. P)$
* Beispiel: $\exists x. (\exists y. (x+y=0)) \equiv \exists y. (\exists x. (x+y=0))$ * Beispiel: $\exists x. (\exists y. (x+y=0)) \equiv \exists y. (\exists x. (x+y=0))$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Aber Achtung: Aber Achtung:
* $\forall x.( \exists y. P) \not\equiv \exists y.( \forall x. P)$ * $\forall x.( \exists y. P) \not\equiv \exists y.( \forall x. P)$
* Beispiel: $\forall x. (\exists y. (y > x)) \not\equiv \exists y. (\forall x. (y > x)$ * Beispiel: $\forall x. (\exists y. (y > x)) \not\equiv \exists y. (\forall x. (y > x)$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Werkzeuge für Logik # Werkzeuge für Logik
* SAT Solver: Erfüllbarkeit von Aussagenlogik prüfen (miniSAT, glucose, lingeling, Sat4j, ...) * SAT Solver: Erfüllbarkeit von Aussagenlogik prüfen (miniSAT, glucose, lingeling, Sat4j, ...)
* SMT Solver: Erfüllbarkeit von Prädikatenlogik mit Theorien (Bit-Vektoren, ...): Z3 von Microsoft * SMT Solver: Erfüllbarkeit von Prädikatenlogik mit Theorien (Bit-Vektoren, ...): Z3 von Microsoft
* Beweiser: Atelier-B, Rodin, Isabelle, Coq, Vampire, ... * Beweiser: Atelier-B, Rodin, Isabelle, Coq, Vampire, ...
* Model-Finder, Constraint Solver: ProB, Alloy, IDP, ... * Model-Finder, Constraint Solver: ProB, Alloy, IDP, ...
* Programmiersprache: Prolog * Programmiersprache: Prolog
Einige Anwendungen dieser Werkzeuge: Einige Anwendungen dieser Werkzeuge:
* Hardware Verifikation * Hardware Verifikation
* schwere Probleme lösen (Abhängigkeiten in Eclipse/Linux, ...) * schwere Probleme lösen (Abhängigkeiten in Eclipse/Linux, ...)
* https://wiki.eclipse.org/Equinox_P2_Resolution * https://wiki.eclipse.org/Equinox_P2_Resolution
* Software Verifikation, Fehler finden (NullPointerException, Overflows), Windows Driver Verification (SLAM2, ...) * Software Verifikation, Fehler finden (NullPointerException, Overflows), Windows Driver Verification (SLAM2, ...)
* SLAM2: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/slam-sdvrpcav2010.pdf * SLAM2: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/slam-sdvrpcav2010.pdf
* https://www.microsoft.com/en-us/research/publication/slam-and-static-driver-verifier-technology-transfer-of-formal-methods-inside-microsoft/ * https://www.microsoft.com/en-us/research/publication/slam-and-static-driver-verifier-technology-transfer-of-formal-methods-inside-microsoft/
* Stellwerkprüfung (Prover Technologies, ...) * Stellwerkprüfung (Prover Technologies, ...)
* Datenvalidierung (ProB bei Siemens, Alstom, Thales; Paris L1) * Datenvalidierung (ProB bei Siemens, Alstom, Thales; Paris L1)
* Software Entwicklung (AtelierB, Paris L14, L1, ...: seit 1999 kein einziger Bug!) * Software Entwicklung (AtelierB, Paris L14, L1, ...: seit 1999 kein einziger Bug!)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Andere Logiken # Andere Logiken
* Aussagenlogik und Prädikatenlogik sind klassische zweiwertige Logiken * Aussagenlogik und Prädikatenlogik sind klassische zweiwertige Logiken
* sie sind **monoton** wenn $\phi \models \psi$ dann gilt für alle $\rho$: $\phi \wedge \rho \models \psi$ * sie sind **monoton** wenn $\phi \models \psi$ dann gilt für alle $\rho$: $\phi \wedge \rho \models \psi$
* Aussagenlogik ist entscheidbar * Aussagenlogik ist entscheidbar
* Prädikatenlogik ist semi-entscheidbar: wenn $\phi \models \psi$ kann man einen Beweis finden * Prädikatenlogik ist semi-entscheidbar: wenn $\phi \models \psi$ kann man einen Beweis finden
* [Gödelscher Vollständigkeitssatz](https://de.wikipedia.org/wiki/Gödelscher_Vollständigkeitssatz) * [Gödelscher Vollständigkeitssatz](https://de.wikipedia.org/wiki/Gödelscher_Vollständigkeitssatz)
* (Anmerkung: Wir werden später in der Vorlesung das Konzept der Entscheidbarkeit formal beschreiben) * (Anmerkung: Wir werden später in der Vorlesung das Konzept der Entscheidbarkeit formal beschreiben)
* reine Prädikatenlogik ist nicht ausreichend um Arithmetik zu axiomatisieren * reine Prädikatenlogik ist nicht ausreichend um Arithmetik zu axiomatisieren
* [Gödelscher Unvollständigkeitssatz](https://de.wikipedia.org/wiki/Gödelscher_Unvollständigkeitssatz) * [Gödelscher Unvollständigkeitssatz](https://de.wikipedia.org/wiki/Gödelscher_Unvollständigkeitssatz)
Nicht-klassische Logiken: Nicht-klassische Logiken:
* es gibt Intuitionistische Logik: Beweis durch Widerspruch dort nicht erlaubt * es gibt Intuitionistische Logik: Beweis durch Widerspruch dort nicht erlaubt
* es gibt dreiwertige Logiken ($2/0=1 \wedge 1=2$) * es gibt dreiwertige Logiken ($2/0=1 \wedge 1=2$)
* es gibt die Fuzzy Logik, modale Logiken, temporale Logiken, ... * es gibt die Fuzzy Logik, modale Logiken, temporale Logiken, ...
* nicht-monotone Logiken * nicht-monotone Logiken
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Zusammenfassung Logik # Zusammenfassung Logik
* Formeln der Aussagenlogik und Prädikatenlogik * Formeln der Aussagenlogik und Prädikatenlogik
* Interpretation, Modell, Äquivalenz ($\equiv$), logisches Schließen ($\models$) * Interpretation, Modell, Äquivalenz ($\equiv$), logisches Schließen ($\models$)
* Deduktiver Beweis, Äquivalenzbeweis * Deduktiver Beweis, Äquivalenzbeweis
* Beweis durch Widerspruch * Beweis durch Widerspruch
* Äquivalenzen (Kommutativität, de Morgan, ...) * Äquivalenzen (Kommutativität, de Morgan, ...)
* Ziel: logische Formeln verstehen und erstellen können * Ziel: logische Formeln verstehen und erstellen können
* Nächste Vorlesung: Grundlagen der Mengentheorie * Nächste Vorlesung: Grundlagen der Mengentheorie
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Anhang mit Erläuterungen # Anhang mit Erläuterungen
## Unterschied zwischen $\equiv$ und $\Leftrightarrow$ ## Unterschied zwischen $\equiv$ und $\Leftrightarrow$
* $\Leftrightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen * $\Leftrightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen
* wenn $\phi$ und $\psi$ Formeln der Aussagenlogik sind, dann ist $\phi \Leftrightarrow \psi$ also auch eine Formel der Aussagenlogik * wenn $\phi$ und $\psi$ Formeln der Aussagenlogik sind, dann ist $\phi \Leftrightarrow \psi$ also auch eine Formel der Aussagenlogik
* $\equiv$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen * $\equiv$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen
* Mit $\equiv$ trifft man mathematische Aussagen über zwei Formeln. * Mit $\equiv$ trifft man mathematische Aussagen über zwei Formeln.
Es gilt aber folgendes Theorem: Es gilt aber folgendes Theorem:
Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik. Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik.
Dann gilt: Dann gilt:
* $\phi \equiv \psi$ gdw die Formel $\phi \Leftrightarrow \psi$ eine Tautologie ist. * $\phi \equiv \psi$ gdw die Formel $\phi \Leftrightarrow \psi$ eine Tautologie ist.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Zum Beispiel haben wir $p \vee \neg q \equiv q \Rightarrow p$ und in der Tat is die Formel $(p \vee \neg q) \Leftrightarrow (q \Rightarrow p)$ eine Tautologie: Zum Beispiel haben wir $p \vee \neg q \equiv q \Rightarrow p$ und in der Tat is die Formel $(p \vee \neg q) \Leftrightarrow (q \Rightarrow p)$ eine Tautologie:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {p,q,ODER,IMPL,EQUIV| p:BOOL & q:BOOL & :table {p,q,ODER,IMPL,EQUIV| p:BOOL & q:BOOL &
ODER = bool(p=TRUE ∨ ¬(q=TRUE)) & // 𝑝∨¬𝑞 ODER = bool(p=TRUE ∨ ¬(q=TRUE)) & // 𝑝∨¬𝑞
IMPL = bool(q=TRUE ⇒ p=TRUE) & // 𝑞⇒p IMPL = bool(q=TRUE ⇒ p=TRUE) & // 𝑞⇒p
EQUIV = bool((ODER=TRUE) ⇔ (IMPL=TRUE))} EQUIV = bool((ODER=TRUE) ⇔ (IMPL=TRUE))}
``` ```
%% Output %% Output
|p|q|ODER|IMPL|EQUIV| |p|q|ODER|IMPL|EQUIV|
|---|---|---|---|---| |---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE| |FALSE|FALSE|TRUE|TRUE|TRUE|
|FALSE|TRUE|FALSE|FALSE|TRUE| |FALSE|TRUE|FALSE|FALSE|TRUE|
|TRUE|FALSE|TRUE|TRUE|TRUE| |TRUE|FALSE|TRUE|TRUE|TRUE|
|TRUE|TRUE|TRUE|TRUE|TRUE| |TRUE|TRUE|TRUE|TRUE|TRUE|
p q ODER IMPL EQUIV p q ODER IMPL EQUIV
FALSE FALSE TRUE TRUE TRUE FALSE FALSE TRUE TRUE TRUE
FALSE TRUE FALSE FALSE TRUE FALSE TRUE FALSE FALSE TRUE
TRUE FALSE TRUE TRUE TRUE TRUE FALSE TRUE TRUE TRUE
TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Formel $(p \vee q) \Leftrightarrow (p \wedge q)$ hingegen ist eine erfüllbare Formel, aber keine Tautologie. Die Formel $(p \vee q) \Leftrightarrow (p \wedge q)$ hingegen ist eine erfüllbare Formel, aber keine Tautologie.
Es gilt also $(p \vee q) \not\equiv (p \wedge q)$! Es gilt also $(p \vee q) \not\equiv (p \wedge q)$!
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {p,q,ODER,UND,EQUIV| p:BOOL & q:BOOL & :table {p,q,ODER,UND,EQUIV| p:BOOL & q:BOOL &
ODER = bool(p=TRUE ∨ q=TRUE) & // 𝑝∨𝑞 ODER = bool(p=TRUE ∨ q=TRUE) & // 𝑝∨𝑞
UND = bool(p=TRUE & q=TRUE) & // p&q UND = bool(p=TRUE & q=TRUE) & // p&q
EQUIV = bool((ODER=TRUE) ⇔ (UND=TRUE))} EQUIV = bool((ODER=TRUE) ⇔ (UND=TRUE))}
``` ```
%% Output %% Output
|p|q|ODER|UND|EQUIV| |p|q|ODER|UND|EQUIV|
|---|---|---|---|---| |---|---|---|---|---|
|FALSE|FALSE|FALSE|FALSE|TRUE| |FALSE|FALSE|FALSE|FALSE|TRUE|
|FALSE|TRUE|TRUE|FALSE|FALSE| |FALSE|TRUE|TRUE|FALSE|FALSE|
|TRUE|FALSE|TRUE|FALSE|FALSE| |TRUE|FALSE|TRUE|FALSE|FALSE|
|TRUE|TRUE|TRUE|TRUE|TRUE| |TRUE|TRUE|TRUE|TRUE|TRUE|
p q ODER UND EQUIV p q ODER UND EQUIV
FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE FALSE TRUE
FALSE TRUE TRUE FALSE FALSE FALSE TRUE TRUE FALSE FALSE
TRUE FALSE TRUE FALSE FALSE TRUE FALSE TRUE FALSE FALSE
TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Unterschied zwischen $\models$ und $\Rightarrow$ ## Unterschied zwischen $\models$ und $\Rightarrow$
Das Gleiche gilt für diese beiden Symbole: Das Gleiche gilt für diese beiden Symbole:
* $\Rightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen * $\Rightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen
* wenn $\phi$ und $\psi$ Formeln der Aussagenlogik sind, dann ist $\phi \Rightarrow \psi$ also auch eine Formel der Aussagenlogik * wenn $\phi$ und $\psi$ Formeln der Aussagenlogik sind, dann ist $\phi \Rightarrow \psi$ also auch eine Formel der Aussagenlogik
* $\models$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen * $\models$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen
* Mit $\models$ trifft man mathematische Aussagen über zwei Formeln. * Mit $\models$ trifft man mathematische Aussagen über zwei Formeln.
Es gilt aber folgendes Theorem: Es gilt aber folgendes Theorem:
Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik. Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik.
Dann gilt: Dann gilt:
* $\phi \models \psi$ gdw die Formel $\phi \Rightarrow \psi$ eine Tautologie ist. * $\phi \models \psi$ gdw die Formel $\phi \Rightarrow \psi$ eine Tautologie ist.
......
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Theoretische Informatik - Vorlesung 0 - Teil 2 Mengentheorie # Theoretische Informatik - Vorlesung 0 - Teil 2 Mengentheorie
* April 2023 * April 2020
* Michael Leuschel * Michael Leuschel
* Lehrstuhl Softwaretechnik und Programmiersprachen * Lehrstuhl Softwaretechnik und Programmiersprachen
* Heinrich-Heine Universität Düsseldorf * Heinrich-Heine Universität Düsseldorf
Grundlagen der Logik und Mengentheorie sind nicht im Skript. Grundlagen der Logik und Mengentheorie sind nicht im Skript.
Hier definieren wir einige Grundlagen und Notationen die im Skript verwendet werden. Hier definieren wir einige Grundlagen und Notationen die im Skript verwendet werden.
Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich. Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich.
Auswertung der Formeln erfolgt mit dem [Jupyter Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) für [ProB](https://prob.hhu.de/w/) Auswertung der Formeln erfolgt mit dem [Jupyter Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) für [ProB](https://prob.hhu.de/w/)
Um dieses Notebook zu starten kann man entweder selber Jupyter und den [ProB-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren. Um dieses Notebook zu starten kann man entweder selber Jupyter und den [ProB-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren.
Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger): Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger):
[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob-teaching-notebooks.git/HEAD?urlpath=%2Ftree%2Finfo4%2Fkapitel-0%2FMengentheorie.ipynb) [![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob-teaching-notebooks.git/HEAD?urlpath=%2Ftree%2Finfo4%2Fkapitel-0%2FMengentheorie.ipynb)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Mengen # Mengen
Fundamentale Idee der Mengentheorie: Fundamentale Idee der Mengentheorie:
* _"Unter einer ‚Menge‘ verstehen wir jede Zusammenfassung M von bestimmten wohlunterschiedenen Objekten m unserer Anschauung oder unseres Denkens (welche die ‚Elemente‘ von M genannt werden) zu einem Ganzen."_ Georg Cantor (siehe [Textstelle als Bild in Wikipedia](https://de.wikipedia.org/wiki/Datei:Textstelle_mit_der_Mengendefinition_von_Georg_Cantor.png)) * _"Unter einer ‚Menge‘ verstehen wir jede Zusammenfassung M von bestimmten wohlunterschiedenen Objekten m unserer Anschauung oder unseres Denkens (welche die ‚Elemente‘ von M genannt werden) zu einem Ganzen."_ Georg Cantor (siehe [Textstelle als Bild in Wikipedia](https://de.wikipedia.org/wiki/Datei:Textstelle_mit_der_Mengendefinition_von_Georg_Cantor.png))
* _"The ability to regard any collection of objects as a single entity (i.e., as a set)."_ (Keith Devlin. Joy of Sets. Springer-Verlag.) * _"The ability to regard any collection of objects as a single entity (i.e., as a set)."_ (Keith Devlin. Joy of Sets. Springer-Verlag.)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In der Regel gibt es eine Domäne an "Objekten" mit denen man Mengen bauen kann. In der Regel gibt es eine Domäne an "Objekten" mit denen man Mengen bauen kann.
Was genau diese Objekte sind interessiert uns in der Mengentheorie nicht. Was genau diese Objekte sind interessiert uns in der Mengentheorie nicht.
Fundamental sind diese beiden Symbole: Fundamental sind diese beiden Symbole:
* wenn $a$ ein Objekt ist und $x$ eine Menge, dann * wenn $a$ ein Objekt ist und $x$ eine Menge, dann
* ist $a \in x$ wahr, wenn $a$ ein Element von $x$ ist * ist $a \in x$ wahr, wenn $a$ ein Element von $x$ ist
* ist $a \not\in x$ wahr, wenn $a$ **kein** Element von $x$ ist. * ist $a \not\in x$ wahr, wenn $a$ **kein** Element von $x$ ist.
$\in$ und $\not\in$ sind Prädikate, verbunden durch die Eigenschaft: $\in$ und $\not\in$ sind Prädikate, verbunden durch die Eigenschaft:
* $\forall(a,x).(a\not\in x \Leftrightarrow \neg(a \in x))$ * $\forall(a,x).(a\not\in x \Leftrightarrow \neg(a \in x))$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Die leere Menge und Gleichheit ## Die leere Menge und Gleichheit
Eine besondere Menge ist die leere Menge $\emptyset$. Eine besondere Menge ist die leere Menge $\emptyset$.
Sie hat keine Elemente: Sie hat keine Elemente:
* $z = \emptyset \Leftrightarrow \forall(a).(a\not\in z)$ * $z = \emptyset \Leftrightarrow \forall(a).(a\not\in z)$
Zwei Mengen $x$ und $y$ sind gleich gdw sie die gleichen Elemente haben: Zwei Mengen $x$ und $y$ sind gleich gdw sie die gleichen Elemente haben:
* $\forall(x,y).(x=y \Leftrightarrow \forall(a).(a\in x \Leftrightarrow a \in y))$ * $\forall(x,y).(x=y \Leftrightarrow \forall(a).(a\in x \Leftrightarrow a \in y))$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∅ = {1} ∅ = {1}
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1} = {1,2} {1} = {1,2}
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1,2} = {2,1} {1,2} = {2,1}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Notationen für Mengen: endliche Enumeration # Notationen für Mengen: endliche Enumeration
* explizite Auflistung aller Elemente $\{a_1,\ldots,a_n\}$ * explizite Auflistung aller Elemente $\{a_1,\ldots,a_n\}$
* die Reihenfolge spielt keine Rolle: * die Reihenfolge spielt keine Rolle:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2,5,3} = {2,3,5} {2,5,3} = {2,3,5}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Dies ist im Unterschied zu Tupeln und Listen oder Folgen, die oft mit runden und eckigen Klammern geschriben werden: Dies ist im Unterschied zu Tupeln und Listen oder Folgen, die oft mit runden und eckigen Klammern geschriben werden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(TRUE,5,3) = (TRUE,3,5) // Vergleich von zwei Tripeln (TRUE,5,3) = (TRUE,3,5) // Vergleich von zwei Tripeln
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[2,5,3] = [2,3,5] // Vergleich von zwei Folgen/Listen [2,5,3] = [2,3,5] // Vergleich von zwei Folgen/Listen
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
* Elemente können in der Enumeration mehrfach auftauchen: * Elemente können in der Enumeration mehrfach auftauchen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2,5,3,2,5} = {2,3,5} {2,5,3,2,5} = {2,3,5}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Vereinigung, Schnitt, Differenz # Vereinigung, Schnitt, Differenz
Drei wichtige Operationen auf Mengen sind wie folgt. Drei wichtige Operationen auf Mengen sind wie folgt.
Vereinigung von Mengen $\cup$: Vereinigung von Mengen $\cup$:
* $z = x\cup y \Leftrightarrow \forall(a).(a\in z \Leftrightarrow (a\in x \vee a \in y))$ * $z = x\cup y \Leftrightarrow \forall(a).(a\in z \Leftrightarrow (a\in x \vee a \in y))$
Schnitt von Mengen $\cap$: Schnitt von Mengen $\cap$:
* $z = x\cap y \Leftrightarrow \forall(a).(a\in z \Leftrightarrow (a\in x \wedge a \in y))$ * $z = x\cap y \Leftrightarrow \forall(a).(a\in z \Leftrightarrow (a\in x \wedge a \in y))$
Differenz von Mengen $\setminus$: Differenz von Mengen $\setminus$:
* $z = x \setminus y \Leftrightarrow \forall(a).(a\in z \Leftrightarrow (a\in x \wedge a \not\in y))$ * $z = x \setminus y \Leftrightarrow \forall(a).(a\in z \Leftrightarrow (a\in x \wedge a \not\in y))$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2,3,5} ∪ {5,7} {2,3,5} ∪ {5,7}
``` ```
%% Output %% Output
$\{2,3,5,7\}$ $\{2,3,5,7\}$
{2,3,5,7} {2,3,5,7}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2,3,5} ∩ {5,7} {2,3,5} ∩ {5,7}
``` ```
%% Output %% Output
$\{5\}$ $\{5\}$
{5} {5}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2,3,5} \ {5,7} {2,3,5} \ {5,7}
``` ```
%% Output %% Output
$\{2,3\}$ $\{2,3\}$
{2,3} {2,3}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Notationen für Mengen: per Prädikat # Notationen für Mengen: per Prädikat
Man kann die Elemente einer Menge auch durch ein Prädikat beschreiben:$\{a \mid P(a)\}$. Man kann die Elemente einer Menge auch durch ein Prädikat beschreiben:$\{a \mid P(a)\}$.
Es gilt: Es gilt:
* $z = \{a \mid P(a)\} \Leftrightarrow \forall(a).(a\in z \Leftrightarrow P(a))$ * $z = \{a \mid P(a)\} \Leftrightarrow \forall(a).(a\in z \Leftrightarrow P(a))$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{a | a∈ℕ ∧ a>1 ∧ a<6 ∧ a≠4} {a | a∈ℕ ∧ a>1 ∧ a<6 ∧ a≠4}
``` ```
%% Output %% Output
$\{2,3,5\}$ $\{2,3,5\}$
{2,3,5} {2,3,5}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann mit dieser Schreibweise auch unendliche Mengen darstellen: Man kann mit dieser Schreibweise auch unendliche Mengen darstellen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{a | a∈ℕ ∧ a>10} {a | a∈ℕ ∧ a>10}
``` ```
%% Output %% Output
$\newcommand{\nat}{\mathord{\mathbb N}}\{\mathit{a}\mid\mathit{a} \in \nat \land \mathit{a} > 10\}$ $\newcommand{\nat}{\mathord{\mathbb N}}\{\mathit{a}\mid\mathit{a} \in \nat \land \mathit{a} > 10\}$
{a∣a ∈ ℕ ∧ a > 10} {a∣a ∈ ℕ ∧ a > 10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{a | a∈ℕ ∧ a mod 2 = 0} ∩ {2,3,5} {a | a∈ℕ ∧ a mod 2 = 0} ∩ {2,3,5}
``` ```
%% Output %% Output
$\{2\}$ $\{2\}$
{2} {2}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann mit dieser Schreibweise auch die drei Mengenoperationen definieren: Man kann mit dieser Schreibweise auch die drei Mengenoperationen definieren:
* $x \cup y = \{a \mid a\in x \vee a\in y\}$ * $x \cup y = \{a \mid a\in x \vee a\in y\}$
* $x \cap y = \{a \mid a\in x \wedge a\in y\}$ * $x \cap y = \{a \mid a\in x \wedge a\in y\}$
* $x \setminus y = \{a \mid a\in x \wedge a\not\in y\}$ * $x \setminus y = \{a \mid a\in x \wedge a\not\in y\}$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x = {2,3} ∧ y = {2,5} ∧ xy = {a | a∈x ∨ a∈y} x = {2,3} ∧ y = {2,5} ∧ xy = {a | a∈x ∨ a∈y}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xy} = \{2,3,5\}$ * $\mathit{xy} = \{2,3,5\}$
* $\mathit{x} = \{2,3\}$ * $\mathit{x} = \{2,3\}$
* $\mathit{y} = \{2,5\}$ * $\mathit{y} = \{2,5\}$
TRUE TRUE
Solution: Solution:
xy = {2,3,5} xy = {2,3,5}
x = {2,3} x = {2,3}
y = {2,5} y = {2,5}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x = {2,3} ∧ y = {2,5} ∧ xy = {a | a∈x ∧ a∈y} x = {2,3} ∧ y = {2,5} ∧ xy = {a | a∈x ∧ a∈y}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xy} = \{2\}$ * $\mathit{xy} = \{2\}$
* $\mathit{x} = \{2,3\}$ * $\mathit{x} = \{2,3\}$
* $\mathit{y} = \{2,5\}$ * $\mathit{y} = \{2,5\}$
TRUE TRUE
Solution: Solution:
xy = {2} xy = {2}
x = {2,3} x = {2,3}
y = {2,5} y = {2,5}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x = {2,3} ∧ y = {2,5} ∧ xy = {a | a∈x ∧ a∉y} x = {2,3} ∧ y = {2,5} ∧ xy = {a | a∈x ∧ a∉y}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{xy} = \{3\}$ * $\mathit{xy} = \{3\}$
* $\mathit{x} = \{2,3\}$ * $\mathit{x} = \{2,3\}$
* $\mathit{y} = \{2,5\}$ * $\mathit{y} = \{2,5\}$
TRUE TRUE
Solution: Solution:
xy = {3} xy = {3}
x = {2,3} x = {2,3}
y = {2,5} y = {2,5}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Als Kürzel führen wir auch die Notation $a..b$ für $\{x \mid x \in \mathbb{Z} \wedge x \geq a \wedge x \leq b\}$ ein. Als Kürzel führen wir auch die Notation $a..b$ für $\{x \mid x \in \mathbb{Z} \wedge x \geq a \wedge x \leq b\}$ ein.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..10 1..10
``` ```
%% Output %% Output
$\{1,2,3,4,5,6,7,8,9,10\}$ $\{1,2,3,4,5,6,7,8,9,10\}$
{1,2,3,4,5,6,7,8,9,10} {1,2,3,4,5,6,7,8,9,10}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Ein Theorem (Distributivgesetz 1) # Ein Theorem (Distributivgesetz 1)
Für alle Mengen $x$, $y$, $z$ gilt: Für alle Mengen $x$, $y$, $z$ gilt:
* $x \cup (y \cap z) = (x\cup y) \cap (x\cup z)$ * $x \cup (y \cap z) = (x\cup y) \cap (x\cup z)$
<img src="./img/Venn.svg" width="300"> <img src="./img/Venn.svg" width="300">
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2,3,55}∪({2,44,77}∩{2,44,66}) {2,3,55}∪({2,44,77}∩{2,44,66})
``` ```
%% Output %% Output
$\{2,3,44,55\}$ $\{2,3,44,55\}$
{2,3,44,55} {2,3,44,55}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
({2,3,55}∪{2,44,77})∩({2,3,55}∪{2,44,66}) ({2,3,55}∪{2,44,77})∩({2,3,55}∪{2,44,66})
``` ```
%% Output %% Output
$\{2,3,44,55\}$ $\{2,3,44,55\}$
{2,3,44,55} {2,3,44,55}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Beweis von $x \cup (y \cap z) = (x\cup y) \cap (x\cup z)$ ## Beweis von $x \cup (y \cap z) = (x\cup y) \cap (x\cup z)$
Für den Beweis benötigen wir diese Lemmata: Für den Beweis benötigen wir diese Lemmata:
1. $x \cup y = \{a \mid a\in x \vee a\in y\}$ 1. $x \cup y = \{a \mid a\in x \vee a\in y\}$
2. $x \cap y = \{a \mid a\in x \wedge a\in y\}$ 2. $x \cap y = \{a \mid a\in x \wedge a\in y\}$
3. $a \in \{b \mid P(b)\} \equiv P(a)$ 3. $a \in \{b \mid P(b)\} \equiv P(a)$
4. $\phi \vee (\psi \wedge \rho) \equiv (\phi \vee \psi) \wedge (\phi \vee \rho)$ 4. $\phi \vee (\psi \wedge \rho) \equiv (\phi \vee \psi) \wedge (\phi \vee \rho)$
Hier ist ein Äquivalenzbeweis (siehe vorherige Vorlesung): Hier ist ein Äquivalenzbeweis (siehe vorherige Vorlesung):
1. $m=x \cup (y \cap z)$ 1. $m=x \cup (y \cap z)$
2. (Lemma 1) $\Longleftrightarrow$ $m=\{a \mid a\in x \vee a\in (y \cap z)\}$ 2. (Lemma 1) $\Longleftrightarrow$ $m=\{a \mid a\in x \vee a\in (y \cap z)\}$
3. (Lemma 2) $\Longleftrightarrow$ $m=\{a \mid a\in x \vee a\in \{b \mid b\in y \wedge b\in z\} \}$ 3. (Lemma 2) $\Longleftrightarrow$ $m=\{a \mid a\in x \vee a\in \{b \mid b\in y \wedge b\in z\} \}$
4. (Lemma 3) $\Longleftrightarrow$ $m=\{a \mid a\in x \vee (a\in y \wedge a\in z) \}$ 4. (Lemma 3) $\Longleftrightarrow$ $m=\{a \mid a\in x \vee (a\in y \wedge a\in z) \}$
5. (Lemma 4) $\Longleftrightarrow$ $m=\{a \mid (a\in x \vee a\in y) \wedge (a\in x \vee a\in z) \}$ 5. (Lemma 4) $\Longleftrightarrow$ $m=\{a \mid (a\in x \vee a\in y) \wedge (a\in x \vee a\in z) \}$
6. (Lemma 3, $\Leftarrow$) $\Longleftrightarrow$ $m=\{a \mid a\in \{b \mid b\in x \vee b\in y\} \wedge a\in \{b \mid b\in x \vee b\in z\} \}$ 6. (Lemma 3, $\Leftarrow$) $\Longleftrightarrow$ $m=\{a \mid a\in \{b \mid b\in x \vee b\in y\} \wedge a\in \{b \mid b\in x \vee b\in z\} \}$
7. (Lemma 1, $\Leftarrow$) $\Longleftrightarrow$ $m=\{a \mid a\in x \cup y \wedge a\in x \cup z) \}$ 7. (Lemma 1, $\Leftarrow$) $\Longleftrightarrow$ $m=\{a \mid a\in x \cup y \wedge a\in x \cup z) \}$
8. (Lemma 2, $\Leftarrow$) $m=(x\cup y) \cap (x\cup z)$ 8. (Lemma 2, $\Leftarrow$) $m=(x\cup y) \cap (x\cup z)$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Gesetze für $\cap$, $\cup$ und $\setminus$ # Gesetze für $\cap$, $\cup$ und $\setminus$
Für alle Mengen $x$, $y$, $z$ gilt: Für alle Mengen $x$, $y$, $z$ gilt:
* $x \cup y = y \cup x$ (Kommutativ 1) * $x \cup y = y \cup x$ (Kommutativ 1)
* $x \cap y = y \cap x$ (Kommutativ 2) * $x \cap y = y \cap x$ (Kommutativ 2)
* $x \cup (y \cup z) = (x\cup y) \cup z$ (Assoziativ 1) * $x \cup (y \cup z) = (x\cup y) \cup z$ (Assoziativ 1)
* $x \cap (y \cap z) = (x\cap y) \cap z$ (Assoziativ 2) * $x \cap (y \cap z) = (x\cap y) \cap z$ (Assoziativ 2)
* $x \cup (y \cap z) = (x\cup y) \cap (x\cup z)$ (Distributiv 1, siehe oben) * $x \cup (y \cap z) = (x\cup y) \cap (x\cup z)$ (Distributiv 1, siehe oben)
* $x \cap (y \cup z) = (x\cap y) \cup (x\cap z)$ (Distributiv 2) * $x \cap (y \cup z) = (x\cap y) \cup (x\cap z)$ (Distributiv 2)
* $z \setminus (x \cup y) = (z\setminus x) \cap (z\setminus y)$ (De Morgan 1) * $z \setminus (x \cup y) = (z\setminus x) \cap (z\setminus y)$ (De Morgan 1)
* $z \setminus (x \cap y) = (z\setminus x) \cup (z\setminus y)$ (De Morgan 2) * $z \setminus (x \cap y) = (z\setminus x) \cup (z\setminus y)$ (De Morgan 2)
* $x \cup \emptyset = x$ (Leere Menge 1) * $x \cup \emptyset = x$ (Leere Menge 1)
* $x \cap \emptyset = \emptyset$ (Leere Menge 2) * $x \cap \emptyset = \emptyset$ (Leere Menge 2)
* $x \cap (z \setminus x) = \emptyset$ (Leere Menge 3) * $x \cap (z \setminus x) = \emptyset$ (Leere Menge 3)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1..10) \ ({2,4,6,8} ∪ {5,10}) // De Morgan 1 - linke Seite (1..10) \ ({2,4,6,8} ∪ {5,10}) // De Morgan 1 - linke Seite
``` ```
%% Output %% Output
$\{1,3,7,9\}$ $\{1,3,7,9\}$
{1,3,7,9} {1,3,7,9}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1..10) \ {2,4,6,8} (1..10) \ {2,4,6,8}
``` ```
%% Output %% Output
$\{1,3,5,7,9,10\}$ $\{1,3,5,7,9,10\}$
{1,3,5,7,9,10} {1,3,5,7,9,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1..10) \ {5,10} (1..10) \ {5,10}
``` ```
%% Output %% Output
$\{1,2,3,4,6,7,8,9\}$ $\{1,2,3,4,6,7,8,9\}$
{1,2,3,4,6,7,8,9} {1,2,3,4,6,7,8,9}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
((1..10) \ {2,4,6,8}) ∩ ((1..10) \ {5,10}) // De Morgan 1 - rechte Seite ((1..10) \ {2,4,6,8}) ∩ ((1..10) \ {5,10}) // De Morgan 1 - rechte Seite
``` ```
%% Output %% Output
$\{1,3,7,9\}$ $\{1,3,7,9\}$
{1,3,7,9} {1,3,7,9}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Gesetze von De Morgan haben wir auch schon in der Aussagenlogik gesehen. Gesetze von De Morgan haben wir auch schon in der Aussagenlogik gesehen.
Auch hier haben diese die Form wo ein Ausdruck Auch hier haben diese die Form wo ein Ausdruck
* $Op1( x ~ Op2 ~ y)$ * $Op1( x ~ Op2 ~ y)$
umgewandelt wird in einen Ausdruck umgewandelt wird in einen Ausdruck
* $Op1(x) ~ Op2' ~ Op1(y)$ * $Op1(x) ~ Op2' ~ Op1(y)$
wo Op2' der duale Operator von Op2 ist. wo Op2' der duale Operator von Op2 ist.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Hier ein Beispiel für das letzte Gesetz: Hier ein Beispiel für das letzte Gesetz:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2,4} ∩ (ℤ \ {2,4}) {2,4} ∩ (ℤ \ {2,4})
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$ $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Teilmenge # Teilmenge
Eine Menge $x$ ist eine Teilmenge oder Untermenge von $y$ wenn gilt: Eine Menge $x$ ist eine Teilmenge oder Untermenge von $y$ wenn gilt:
* $\forall a. a\in x \Rightarrow a \in y$ * $\forall a. a\in x \Rightarrow a \in y$
Wir benutzen diese Schreibweise $x \subseteq y$. Wir benutzen diese Schreibweise $x \subseteq y$.
In diesem Fall ist $y$ auch eine Obermenge von $x$, geschrieben als $y \supseteq x$. In diesem Fall ist $y$ auch eine Obermenge von $x$, geschrieben als $y \supseteq x$.
Für die echte Teilmenge benutzen wir folgende Schreibweise und Definition: Für die echte Teilmenge benutzen wir folgende Schreibweise und Definition:
* $x \subset y$ $\Leftrightarrow$ $(x \subseteq y \wedge x\neq y)$. * $x \subset y$ $\Leftrightarrow$ $(x \subseteq y \wedge x\neq y)$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x={1,3} ∧ y = 1..5 ∧ ∀a.(a∈x ⇒ a∈y) x={1,3} ∧ y = 1..5 ∧ ∀a.(a∈x ⇒ a∈y)
``` ```
%% Output %% Output
$\newcommand{\upto}{\mathbin{.\mkern1mu.}}\mathit{TRUE}$ $\newcommand{\upto}{\mathbin{.\mkern1mu.}}\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = \{1,3\}$ * $\mathit{x} = \{1,3\}$
* $\mathit{y} = (1 \upto 5)$ * $\mathit{y} = (1 \upto 5)$
TRUE TRUE
Solution: Solution:
x = {1,3} x = {1,3}
y = (1 ‥ 5) y = (1 ‥ 5)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x={1,3} ∧ y = 1..5 ∧ ∀a.(a∈y ⇒ a∈x) x={1,3} ∧ y = 1..5 ∧ ∀a.(a∈y ⇒ a∈x)
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1,3} ⊂ 1..5 {1,3} ⊂ 1..5
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Kardinalität # Kardinalität
Die Anzahl der Elemente einer Menge $x$ schreiben wir als Die Anzahl der Elemente einer Menge $x$ schreiben wir als
* $\mid x\mid$ oder auch als $card(x)$ (B Schreibweise). * $\mid x\mid$ oder auch als $card(x)$ (B Schreibweise).
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({1,2,3}) card({1,2,3})
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({1,1,2,3,2}) card({1,1,2,3,2})
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(∅) card(∅)
``` ```
%% Output %% Output
$0$ $0$
0 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Achtung, die Kardinalität kann auch unendlich sein: je nach Formalismus, ist folgender Ausdruck entweder unendlich oder nicht wohl definiert: $|\{x \mid x \in \mathbb{Z} \wedge x>0\}|$ Achtung, die Kardinalität kann auch unendlich sein: je nach Formalismus, ist folgender Ausdruck entweder unendlich oder nicht wohl definiert: $|\{x \mid x \in \mathbb{Z} \wedge x>0\}|$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({x|x∈ℤ ∧ x>0}) card({x|x∈ℤ ∧ x>0})
``` ```
%% Output %% Output
:eval: NOT-WELL-DEFINED: :eval: NOT-WELL-DEFINED:
card applied to very large set, cardinality not representable in ProB: closure([x],[integer],b(greater(b(identifier(...),integer,[...]),b(value(...),integer,[...])),pred,[nodeid(pos(...)),prob_annotation('DO_NOT_ENUMERATE'(...)),removed_typing])) card applied to very large set, cardinality not representable in ProB: closure([x],[integer],b(greater(b(identifier(...),integer,[...]),b(value(...),integer,[...])),pred,[nodeid(pos(...)),prob_annotation('DO_NOT_ENUMERATE'(...)),removed_typing]))
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# SEND+MORE=MONEY # SEND+MORE=MONEY
Als Übung und Beispiel versuchen wir nun ein Problem zu lösen. Als Übung und Beispiel versuchen wir nun ein Problem zu lösen.
Es handelt sich um ein klassisches arithmetisches Puzzle wo acht unterschiedliche Ziffern gefunden werden sollen die folgende Gleichung erfüllen: Es handelt sich um ein klassisches arithmetisches Puzzle wo acht unterschiedliche Ziffern gefunden werden sollen die folgende Gleichung erfüllen:
| | | | | | | | | | | |
|---|---|---|---|---| |---|---|---|---|---|
| | S | E | N | D | | | S | E | N | D |
| + | M | O | R | E | | + | M | O | R | E |
| |
|= M| O | N | E | Y | |= M| O | N | E | Y |
| | | | | | | | | | | |
Wir können dies nun in Logik, Mengentheorie und Arithmetik modellieren und lösen. Wir können dies nun in Logik, Mengentheorie und Arithmetik modellieren und lösen.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir haben acht Ziffern: Wir haben acht Ziffern:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9 {S,E,N,D,M,O,R,Y} ⊆ 0..9
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 0$ * $\mathit{R} = 0$
* $\mathit{S} = 0$ * $\mathit{S} = 0$
* $\mathit{D} = 0$ * $\mathit{D} = 0$
* $\mathit{E} = 0$ * $\mathit{E} = 0$
* $\mathit{Y} = 0$ * $\mathit{Y} = 0$
* $\mathit{M} = 0$ * $\mathit{M} = 0$
* $\mathit{N} = 0$ * $\mathit{N} = 0$
* $\mathit{O} = 0$ * $\mathit{O} = 0$
TRUE TRUE
Solution: Solution:
R = 0 R = 0
S = 0 S = 0
D = 0 D = 0
E = 0 E = 0
Y = 0 Y = 0
M = 0 M = 0
N = 0 N = 0
O = 0 O = 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
diese Ziffern sind alle unterschiedlich: diese Ziffern sind alle unterschiedlich:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9 ∧ {S,E,N,D,M,O,R,Y} ⊆ 0..9 ∧
card({S,E,N,D,M,O,R,Y}) = 8 card({S,E,N,D,M,O,R,Y}) = 8
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 2$ * $\mathit{R} = 2$
* $\mathit{S} = 0$ * $\mathit{S} = 0$
* $\mathit{D} = 5$ * $\mathit{D} = 5$
* $\mathit{E} = 7$ * $\mathit{E} = 7$
* $\mathit{Y} = 1$ * $\mathit{Y} = 1$
* $\mathit{M} = 4$ * $\mathit{M} = 4$
* $\mathit{N} = 6$ * $\mathit{N} = 6$
* $\mathit{O} = 3$ * $\mathit{O} = 3$
TRUE TRUE
Solution: Solution:
R = 2 R = 2
S = 0 S = 0
D = 5 D = 5
E = 7 E = 7
Y = 1 Y = 1
M = 4 M = 4
N = 6 N = 6
O = 3 O = 3
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
und wobei die zwei führenden Ziffern S und M ungleich 0 sind: und wobei die zwei führenden Ziffern S und M ungleich 0 sind:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9 ∧ card({S,E,N,D,M,O,R,Y}) = 8 ∧ {S,E,N,D,M,O,R,Y} ⊆ 0..9 ∧ card({S,E,N,D,M,O,R,Y}) = 8 ∧
S ≠ 0 ∧ M ≠ 0 S ≠ 0 ∧ M ≠ 0
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 3$ * $\mathit{R} = 3$
* $\mathit{S} = 2$ * $\mathit{S} = 2$
* $\mathit{D} = 5$ * $\mathit{D} = 5$
* $\mathit{E} = 7$ * $\mathit{E} = 7$
* $\mathit{Y} = 0$ * $\mathit{Y} = 0$
* $\mathit{M} = 1$ * $\mathit{M} = 1$
* $\mathit{N} = 6$ * $\mathit{N} = 6$
* $\mathit{O} = 4$ * $\mathit{O} = 4$
TRUE TRUE
Solution: Solution:
R = 3 R = 3
S = 2 S = 2
D = 5 D = 5
E = 7 E = 7
Y = 0 Y = 0
M = 1 M = 1
N = 6 N = 6
O = 4 O = 4
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
und wo die Summe von SEND+MORE MONEY ergibt: und wo die Summe von SEND+MORE MONEY ergibt:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9 ∧ card({S,E,N,D,M,O,R,Y}) = 8 ∧ S ≠ 0 & M ≠ 0 ∧ {S,E,N,D,M,O,R,Y} ⊆ 0..9 ∧ card({S,E,N,D,M,O,R,Y}) = 8 ∧ S ≠ 0 & M ≠ 0 ∧
S*1000 + E*100 + N*10 + D + S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E = M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y M*10000 + O*1000 + N*100 + E*10 + Y
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 8$ * $\mathit{R} = 8$
* $\mathit{S} = 9$ * $\mathit{S} = 9$
* $\mathit{D} = 7$ * $\mathit{D} = 7$
* $\mathit{E} = 5$ * $\mathit{E} = 5$
* $\mathit{Y} = 2$ * $\mathit{Y} = 2$
* $\mathit{M} = 1$ * $\mathit{M} = 1$
* $\mathit{N} = 6$ * $\mathit{N} = 6$
* $\mathit{O} = 0$ * $\mathit{O} = 0$
TRUE TRUE
Solution: Solution:
R = 8 R = 8
S = 9 S = 9
D = 7 D = 7
E = 5 E = 5
Y = 2 Y = 2
M = 1 M = 1
N = 6 N = 6
O = 0 O = 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Aber ist dies die einzige Lösung ? Wir können einfach die Menge aller Lösungen berechnen: Aber ist dies die einzige Lösung ? Wir können einfach die Menge aller Lösungen berechnen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D, M,O,R, Y | {S,E,N,D, M,O,R, Y |
{S,E,N,D, M,O,R, Y} ⊆ 0..9 ∧ S >0 ∧ M >0 ∧ {S,E,N,D, M,O,R, Y} ⊆ 0..9 ∧ S >0 ∧ M >0 ∧
card({S,E,N,D, M,O,R, Y}) = 8 ∧ card({S,E,N,D, M,O,R, Y}) = 8 ∧
S*1000 + E*100 + N*10 + D + S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E = M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y M*10000 + O*1000 + N*100 + E*10 + Y
} }
``` ```
%% Output %% Output
$\{(9\mapsto 5\mapsto 6\mapsto 7\mapsto 1\mapsto 0\mapsto 8\mapsto 2)\}$ $\{(9\mapsto 5\mapsto 6\mapsto 7\mapsto 1\mapsto 0\mapsto 8\mapsto 2)\}$
{(9↦5↦6↦7↦1↦0↦8↦2)} {(9↦5↦6↦7↦1↦0↦8↦2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {S,E,N,D, M,O,R, Y | :table {S,E,N,D, M,O,R, Y |
{S,E,N,D, M,O,R, Y} ⊆ 0..9 ∧ S >0 ∧ M >0 ∧ {S,E,N,D, M,O,R, Y} ⊆ 0..9 ∧ S >0 ∧ M >0 ∧
card({S,E,N,D, M,O,R, Y}) = 8 ∧ card({S,E,N,D, M,O,R, Y}) = 8 ∧
S*1000 + E*100 + N*10 + D + S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E = M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y M*10000 + O*1000 + N*100 + E*10 + Y
} }
``` ```
%% Output %% Output
|S|E|N|D|M|O|R|Y| |S|E|N|D|M|O|R|Y|
|---|---|---|---|---|---|---|---| |---|---|---|---|---|---|---|---|
|9|5|6|7|1|0|8|2| |9|5|6|7|1|0|8|2|
S E N D M O R Y S E N D M O R Y
9 5 6 7 1 0 8 2 9 5 6 7 1 0 8 2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
| | | | | | | | | | | |
|---|---|---|---|---| |---|---|---|---|---|
| | S=9 | E=5 | N=6 | D=7 | | | S=9 | E=5 | N=6 | D=7 |
| + | M=1 | O=0 | R=8 | E=5 | | + | M=1 | O=0 | R=8 | E=5 |
| |
|= M=1| O=0 | N=6 | E=5 | Y=2 | |= M=1| O=0 | N=6 | E=5 | Y=2 |
| | | | | | | | | | | |
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Ein anderes arithmetisches Puzzle ist KISS*KISS=PASSION. Ein anderes arithmetisches Puzzle ist KISS*KISS=PASSION.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {K, I, S, P, A, O, N | :table {K, I, S, P, A, O, N |
{K,P} ⊆ 1..9 ∧ {K,P} ⊆ 1..9 ∧
{I,S,A,O,N} ⊆ 0..9 ∧ {I,S,A,O,N} ⊆ 0..9 ∧
(1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S)
= 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N &
card({K, I, S, P, A, O, N}) = 7} card({K, I, S, P, A, O, N}) = 7}
``` ```
%% Output %% Output
|K|I|S|P|A|O|N| |K|I|S|P|A|O|N|
|---|---|---|---|---|---|---| |---|---|---|---|---|---|---|
|2|0|3|4|1|8|9| |2|0|3|4|1|8|9|
K I S P A O N K I S P A O N
2 0 3 4 1 8 9 2 0 3 4 1 8 9
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Mengen von Mengen # Mengen von Mengen
Mengen können selber auch Mengen beinhalten Mengen können selber auch Mengen beinhalten
Dies sind alles unterschiedliche Mengen: Dies sind alles unterschiedliche Mengen:
* $\{\{2\},\{3,4\}\}$ * $\{\{2\},\{3,4\}\}$
* $\{\{2,3\},\{4\}\}$ * $\{\{2,3\},\{4\}\}$
* $\{\{2,3\},\{3,4\}\}$ * $\{\{2,3\},\{3,4\}\}$
* $\{\{2,3,4\}\}$ * $\{\{2,3,4\}\}$
* $\{2,3,4\}$ * $\{2,3,4\}$
Wir haben zum Beispiel: Wir haben zum Beispiel:
* $|\{\{2,3,4\}\}| = 1$ * $|\{\{2,3,4\}\}| = 1$
* $|\{\{2\},\{3,4\}\}| = 2$ * $|\{\{2\},\{3,4\}\}| = 2$
* $|\{2,3,4\}| = 3$ * $|\{2,3,4\}| = 3$
* $\{2\} \in \{\{2\},\{3,4\}\} $ * $\{2\} \in \{\{2\},\{3,4\}\} $
* $\{2\} \not\in \{\{2,3\},\{4\}\} $ * $\{2\} \not\in \{\{2,3\},\{4\}\} $
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({2,3,4}) card({2,3,4})
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({{2,3,4}}) card({{2,3,4}})
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({{2},{3,4}}) card({{2},{3,4}})
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2} ∈ {{2}, {3,4}} {2} ∈ {{2}, {3,4}}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2} ∈ {{2,3}, {4}} {2} ∈ {{2,3}, {4}}
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Mengen von Mengen und die leere Menge ## Mengen von Mengen und die leere Menge
Achtung: man muss die leere Menge von der Menge die die leere Menge beinhaltet unterscheiden: Achtung: man muss die leere Menge von der Menge die die leere Menge beinhaltet unterscheiden:
* $\emptyset \neq \{\emptyset\}$ * $\emptyset \neq \{\emptyset\}$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∅ = {∅} ∅ = {∅}
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(∅) card(∅)
``` ```
%% Output %% Output
$0$ $0$
0 0
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({∅}) card({∅})
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∅ ∈ {∅} ∅ ∈ {∅}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∅ ∈ ∅ ∅ ∈ ∅
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∅ ∉ ∅ ∅ ∉ ∅
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Potenzmenge # Potenzmenge
Die Menge aller Untermengen einer Menge $A$ schreiben wir als $ℙ(\mathit{A}) $ oder auch als $2^{A}$. Die Menge aller Untermengen einer Menge $A$ schreiben wir als $ℙ(\mathit{A}) $ oder auch als $2^{A}$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ℙ({1,2}) ℙ({1,2})
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{2\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{2\}\}$
{∅,{1},{1,2},{2}} {∅,{1},{1,2},{2}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ℙ(∅) ℙ(∅)
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset\}$
{∅} {∅}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ℙ(1..3) ℙ(1..3)
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{1,3\},\{2\},\{1,2,3\},\{2,3\},\{3\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{1,3\},\{2\},\{1,2,3\},\{2,3\},\{3\}\}$
{∅,{1},{1,2},{1,3},{2},{1,2,3},{2,3},{3}} {∅,{1},{1,2},{1,3},{2},{1,2,3},{2,3},{3}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table ℙ(1..3) :table ℙ(1..3)
``` ```
%% Output %% Output
|Elements| |Elements|
|---| |---|
|∅| |∅|
|{1}| |{1}|
|{1,2}| |{1,2}|
|{1,3}| |{1,3}|
|{2}| |{2}|
|{1,2,3}| |{1,2,3}|
|{2,3}| |{2,3}|
|{3}| |{3}|
Elements Elements
{} {}
{1} {1}
{1,2} {1,2}
{1,3} {1,3}
{2} {2}
{1,2,3} {1,2,3}
{2,3} {2,3}
{3} {3}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table ℙ(ℙ({1})) :table ℙ(ℙ({1}))
``` ```
%% Output %% Output
|Elements| |Elements|
|---| |---|
|∅| |∅|
|{∅}| |{∅}|
|{∅,{1}}| |{∅,{1}}|
|{{1}}| |{{1}}|
Elements Elements
{} {}
{{}} {{}}
{{},{1}} {{},{1}}
{{1}} {{1}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(ℙ(1..3)) card(ℙ(1..3))
``` ```
%% Output %% Output
$8$ $8$
8 8
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(ℙ(1..10)) card(ℙ(1..10))
``` ```
%% Output %% Output
$1024$ $1024$
1024 1024
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(ℙ(1..100)) card(ℙ(1..100))
``` ```
%% Output %% Output
$1267650600228229401496703205376$ $1267650600228229401496703205376$
1267650600228229401496703205376 1267650600228229401496703205376
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(ℙ(ℙ(1..7))) card(ℙ(ℙ(1..7)))
``` ```
%% Output %% Output
$340282366920938463463374607431768211456$ $340282366920938463463374607431768211456$
340282366920938463463374607431768211456 340282366920938463463374607431768211456
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(ℙ(ℙ(ℙ(1..3)))) card(ℙ(ℙ(ℙ(1..3))))
``` ```
%% Output %% Output
$115792089237316195423570985008687907853269984665640564039457584007913129639936$ $115792089237316195423570985008687907853269984665640564039457584007913129639936$
115792089237316195423570985008687907853269984665640564039457584007913129639936 115792089237316195423570985008687907853269984665640564039457584007913129639936
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Relationen in der Mengentheorie # Relationen in der Mengentheorie
* Was ist eine Relation? * Was ist eine Relation?
* Wie kann man Relationen in Mengentheorie und Logik abbilden? * Wie kann man Relationen in Mengentheorie und Logik abbilden?
* https://en.wikipedia.org/wiki/Finitary_relation: * https://en.wikipedia.org/wiki/Finitary_relation:
> In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple. > In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple.
* k-Tupel: $(1,2)$ (k = 2, Paar) * k-Tupel: $(1,2)$ (k = 2, Paar)
* Eine Relation weist k-Tupeln Wahrheitswerte zu: * Eine Relation weist k-Tupeln Wahrheitswerte zu:
* Beispiel: $(1,2) \mapsto \mathit{TRUE}$, $(2,1) \mapsto \mathit{FALSE}$. * Beispiel: $(1,2) \mapsto \mathit{TRUE}$, $(2,1) \mapsto \mathit{FALSE}$.
## Unäre Relationen ## Unäre Relationen
Eine unäre Relation über $x$ entspricht einfach einer Untermenge von $x$: Eine unäre Relation über $x$ entspricht einfach einer Untermenge von $x$:
* die Menge an Werten für die die Relation wahr ist. * die Menge an Werten für die die Relation wahr ist.
Beispiele: Beispiele:
* Relation "Ziffer" über die ganzen Zahlen ist * Relation "Ziffer" über die ganzen Zahlen ist
* $0 .. 9 \subseteq \mathbb{Z}$ * $0 .. 9 \subseteq \mathbb{Z}$
* Relation "Gt0" über die ganzen Zahlen ist * Relation "Gt0" über die ganzen Zahlen ist
* $\{ \mathit{x}|\mathit{x} \in \mathbb{Z} \wedge \mathit{x} > 0\} \subseteq \mathbb{Z}$. * $\{ \mathit{x}|\mathit{x} \in \mathbb{Z} \wedge \mathit{x} > 0\} \subseteq \mathbb{Z}$.
* Relation "Gerade" über die ganzen Zahlen ist * Relation "Gerade" über die ganzen Zahlen ist
* $\{ \mathit{x}|\mathit{x} \in \mathbb{Z} \wedge \mathit{x} \mod 2 = 0\} \subseteq \mathbb{Z}$. * $\{ \mathit{x}|\mathit{x} \in \mathbb{Z} \wedge \mathit{x} \mod 2 = 0\} \subseteq \mathbb{Z}$.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Relationen vs Prädikate ## Relationen vs Prädikate
Eine Relation ist die explizite Darstellung eines Prädikats als Menge: Eine Relation ist die explizite Darstellung eines Prädikats als Menge:
* Prädikate können mit logischen Junktoren und Quantoren verarbeitet werden: * Prädikate können mit logischen Junktoren und Quantoren verarbeitet werden:
* $\exists x. \mathrm{is\_rich}(x)$, $\forall x.(\mathrm{is\_poor}(x) \Rightarrow \neg \mathrm{is\_rich}(x))$ * $\exists x. \mathrm{is\_rich}(x)$, $\forall x.(\mathrm{is\_poor}(x) \Rightarrow \neg \mathrm{is\_rich}(x))$
* Relationen können mit mengentheoretischen Operationen verarbeitet werden: * Relationen können mit mengentheoretischen Operationen verarbeitet werden:
* $\mathrm{rich} \neq \emptyset$, $\mathrm{rich} \cap \mathrm{poor} = \emptyset$. * $\mathrm{rich} \neq \emptyset$, $\mathrm{rich} \cap \mathrm{poor} = \emptyset$.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Kartesisches Produkt und Paare # Kartesisches Produkt und Paare
Das kartesische Produkt $x \times y$ zweier Mengen $x$ und $y$ ist definiert als Das kartesische Produkt $x \times y$ zweier Mengen $x$ und $y$ ist definiert als
* $\{ (a,b) \mid a\in x \wedge b\in y\}$. * $\{ (a,b) \mid a\in x \wedge b\in y\}$.
$(a,b)$ steht hier für ein geordnetes Paar, $(a,b)$ steht hier für ein geordnetes Paar,
d.h. $(1 \mapsto 2) \neq (2 \mapsto 1) $. d.h. $(1 \mapsto 2) \neq (2 \mapsto 1) $.
Wir schreiben manchmal auch $a \mapsto b$ anstatt $(a,b)$. Wir schreiben manchmal auch $a \mapsto b$ anstatt $(a,b)$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1 .. 2) × (4 .. 5) (1 .. 2) × (4 .. 5)
``` ```
%% Output %% Output
$\{(1\mapsto 4),(1\mapsto 5),(2\mapsto 4),(2\mapsto 5)\}$ $\{(1\mapsto 4),(1\mapsto 5),(2\mapsto 4),(2\mapsto 5)\}$
{(1↦4),(1↦5),(2↦4),(2↦5)} {(1↦4),(1↦5),(2↦4),(2↦5)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1 .. 2) × {4} (1 .. 2) × {4}
``` ```
%% Output %% Output
$\{(1\mapsto 4),(2\mapsto 4)\}$ $\{(1\mapsto 4),(2\mapsto 4)\}$
{(1↦4),(2↦4)} {(1↦4),(2↦4)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1 .. 2) × BOOL (1 .. 2) × BOOL
``` ```
%% Output %% Output
$\{(1\mapsto\mathit{FALSE}),(1\mapsto\mathit{TRUE}),(2\mapsto\mathit{FALSE}),(2\mapsto\mathit{TRUE})\}$ $\{(1\mapsto\mathit{FALSE}),(1\mapsto\mathit{TRUE}),(2\mapsto\mathit{FALSE}),(2\mapsto\mathit{TRUE})\}$
{(1↦FALSE),(1↦TRUE),(2↦FALSE),(2↦TRUE)} {(1↦FALSE),(1↦TRUE),(2↦FALSE),(2↦TRUE)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1 .. 3) × (1 .. 3) (1 .. 3) × (1 .. 3)
``` ```
%% Output %% Output
$\{(1\mapsto 1),(1\mapsto 2),(1\mapsto 3),(2\mapsto 1),(2\mapsto 2),(2\mapsto 3),(3\mapsto 1),(3\mapsto 2),(3\mapsto 3)\}$ $\{(1\mapsto 1),(1\mapsto 2),(1\mapsto 3),(2\mapsto 1),(2\mapsto 2),(2\mapsto 3),(3\mapsto 1),(3\mapsto 2),(3\mapsto 3)\}$
{(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3)} {(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card((1..10)×(1..10)) card((1..10)×(1..10))
``` ```
%% Output %% Output
$100$ $100$
100 100
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Das Kartesische Produkt ist nicht kommutativ: Das Kartesische Produkt ist nicht kommutativ:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{2}×{3} {2}×{3}
``` ```
%% Output %% Output
$\{(2\mapsto 3)\}$ $\{(2\mapsto 3)\}$
{(2↦3)} {(2↦3)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{3}×{2} {3}×{2}
``` ```
%% Output %% Output
$\{(3\mapsto 2)\}$ $\{(3\mapsto 2)\}$
{(3↦2)} {(3↦2)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Es gilt: Es gilt:
* $A \times B = \emptyset \equiv (A = \emptyset \vee B=\emptyset)$. * $A \times B = \emptyset \equiv (A = \emptyset \vee B=\emptyset)$.
Das Kartesische Produkt wird auch Kreuzmenge oder Produktmenge genannt. Das Kartesische Produkt wird auch Kreuzmenge oder Produktmenge genannt.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Binäre Relationen # Binäre Relationen
Eine binäre Relation über $x$ und $y$ ist eine Untermenge des kartesischen Produkts $x \times y$ zweier Mengen. Die Mengen $x$ und $y$ können identisch sein. Eine binäre Relation über $x$ und $y$ ist eine Untermenge des kartesischen Produkts $x \times y$ zweier Mengen. Die Mengen $x$ und $y$ können identisch sein.
Beispiel: die Relation "kleiner" über die Ziffern $0..9$: Beispiel: die Relation "kleiner" über die Ziffern $0..9$:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{a,b| (a,b)∈(0..9)×(0..9) ∧ a<b} {a,b| (a,b)∈(0..9)×(0..9) ∧ a<b}
``` ```
%% Output %% Output
$\{(0\mapsto 1),(0\mapsto 2),(0\mapsto 3),(0\mapsto 4),(0\mapsto 5),(0\mapsto 6),(0\mapsto 7),(0\mapsto 8),(0\mapsto 9),(1\mapsto 2),(1\mapsto 3),(1\mapsto 4),(1\mapsto 5),(1\mapsto 6),(1\mapsto 7),(1\mapsto 8),(1\mapsto 9),(2\mapsto 3),(2\mapsto 4),(2\mapsto 5),(2\mapsto 6),(2\mapsto 7),(2\mapsto 8),(2\mapsto 9),(3\mapsto 4),(3\mapsto 5),(3\mapsto 6),(3\mapsto 7),(3\mapsto 8),(3\mapsto 9),(4\mapsto 5),(4\mapsto 6),(4\mapsto 7),(4\mapsto 8),(4\mapsto 9),(5\mapsto 6),(5\mapsto 7),(5\mapsto 8),(5\mapsto 9),(6\mapsto 7),(6\mapsto 8),(6\mapsto 9),(7\mapsto 8),(7\mapsto 9),(8\mapsto 9)\}$ $\{(0\mapsto 1),(0\mapsto 2),(0\mapsto 3),(0\mapsto 4),(0\mapsto 5),(0\mapsto 6),(0\mapsto 7),(0\mapsto 8),(0\mapsto 9),(1\mapsto 2),(1\mapsto 3),(1\mapsto 4),(1\mapsto 5),(1\mapsto 6),(1\mapsto 7),(1\mapsto 8),(1\mapsto 9),(2\mapsto 3),(2\mapsto 4),(2\mapsto 5),(2\mapsto 6),(2\mapsto 7),(2\mapsto 8),(2\mapsto 9),(3\mapsto 4),(3\mapsto 5),(3\mapsto 6),(3\mapsto 7),(3\mapsto 8),(3\mapsto 9),(4\mapsto 5),(4\mapsto 6),(4\mapsto 7),(4\mapsto 8),(4\mapsto 9),(5\mapsto 6),(5\mapsto 7),(5\mapsto 8),(5\mapsto 9),(6\mapsto 7),(6\mapsto 8),(6\mapsto 9),(7\mapsto 8),(7\mapsto 9),(8\mapsto 9)\}$
{(0↦1),(0↦2),(0↦3),(0↦4),(0↦5),(0↦6),(0↦7),(0↦8),(0↦9),(1↦2),(1↦3),(1↦4),(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦3),(2↦4),(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦4),(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦6),(5↦7),(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦8),(7↦9),(8↦9)} {(0↦1),(0↦2),(0↦3),(0↦4),(0↦5),(0↦6),(0↦7),(0↦8),(0↦9),(1↦2),(1↦3),(1↦4),(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦3),(2↦4),(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦4),(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦6),(5↦7),(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦8),(7↦9),(8↦9)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Diese Relation ist eine Untermenge von ℤ×ℤ. Diese Relation ist eine Untermenge von ℤ×ℤ.
Ein anderes Beispiel ist die Relation "halb" über die ganzen Zahlen $1..10$: Ein anderes Beispiel ist die Relation "halb" über die ganzen Zahlen $1..10$:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{a,b| a∈1..10 ∧ b∈1..10 ∧ b*2=a} {a,b| a∈1..10 ∧ b∈1..10 ∧ b*2=a}
``` ```
%% Output %% Output
$\{(2\mapsto 1),(4\mapsto 2),(6\mapsto 3),(8\mapsto 4),(10\mapsto 5)\}$ $\{(2\mapsto 1),(4\mapsto 2),(6\mapsto 3),(8\mapsto 4),(10\mapsto 5)\}$
{(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} {(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Eine binäre Relation kann auch als gerichteter Graph angesehen werden: Eine binäre Relation kann auch als gerichteter Graph angesehen werden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("halb",{a,b| a∈1..10 ∧ b∈1..10 & b*2=a}) :dot expr_as_graph ("halb",{a,b| a∈1..10 ∧ b∈1..10 & b*2=a})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("halb",{a,b| a∈1..10 ∧ b∈1..10 & b*2=a})]> <Dot visualization: expr_as_graph [("halb",{a,b| a∈1..10 ∧ b∈1..10 & b*2=a})]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Typen der Elemente kann abweichen. Die Typen der Elemente kann abweichen.
Zum Beispiel die Relation "durch drei teilbar" über die ganzen Zahlen $1..7$ zum Datentypen $\mathit{STRING}$ Zum Beispiel die Relation "durch drei teilbar" über die ganzen Zahlen $1..7$ zum Datentypen $\mathit{STRING}$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")} {x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")}
``` ```
%% Output %% Output
$\{(1\mapsto\text{"nein"}),(2\mapsto\text{"nein"}),(3\mapsto\text{"ja"}),(4\mapsto\text{"nein"}),(5\mapsto\text{"nein"}),(6\mapsto\text{"ja"}),(7\mapsto\text{"nein"})\}$ $\{(1\mapsto\text{"nein"}),(2\mapsto\text{"nein"}),(3\mapsto\text{"ja"}),(4\mapsto\text{"nein"}),(5\mapsto\text{"nein"}),(6\mapsto\text{"ja"}),(7\mapsto\text{"nein"})\}$
{(1↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")} {(1↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("teilbar",{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")}) :dot expr_as_graph ("teilbar",{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("teilbar",{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")})]> <Dot visualization: expr_as_graph [("teilbar",{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")})]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Das Kartesische Produkt stellt die Relation dar, die immer wahr ist (für die angegebenen Basismengen). Als Graph ist dies der [vollständige Graph](https://de.wikipedia.org/wiki/Vollständiger_Graph) über die Basismengen: Das Kartesische Produkt stellt die Relation dar, die immer wahr ist (für die angegebenen Basismengen). Als Graph ist dies der [vollständige Graph](https://de.wikipedia.org/wiki/Vollständiger_Graph) über die Basismengen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_ENGINE=circo :pref DOT_ENGINE=circo
``` ```
%% Output %% Output
Preference changed: DOT_ENGINE = circo Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("K5",(1..5)×(1..5)) :dot expr_as_graph ("K5",(1..5)×(1..5))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("K5",(1..5)×(1..5))]> <Dot visualization: expr_as_graph [("K5",(1..5)×(1..5))]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_ENGINE=circo :pref DOT_ENGINE=circo
``` ```
%% Output %% Output
Preference changed: DOT_ENGINE = circo Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("K10",(1..10)×(1..10)) :dot expr_as_graph ("K10",(1..10)×(1..10))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("K10",(1..10)×(1..10))]> <Dot visualization: expr_as_graph [("K10",(1..10)×(1..10))]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("K20",(1..20)×(1..20)) :dot expr_as_graph ("K20",(1..20)×(1..20))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("K20",(1..20)×(1..20))]> <Dot visualization: expr_as_graph [("K20",(1..20)×(1..20))]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_ENGINE=dot :pref DOT_ENGINE=dot
``` ```
%% Output %% Output
Preference changed: DOT_ENGINE = dot Preference changed: DOT_ENGINE = dot
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Definitions- und Wertebereich # Definitions- und Wertebereich
Definitionsbereich (Domain in Englisch): Definitionsbereich (Domain in Englisch):
* $\mathrm{dom}(r) = \{a \mid \exists b.((a,b)\in r)\}$ * $\mathrm{dom}(r) = \{a \mid \exists b.((a,b)\in r)\}$
Wertebereich (Bildmenge, Range in Englisch): Wertebereich (Bildmenge, Range in Englisch):
* $\mathrm{ran}(r) = \{b \mid \exists a.((a,b)\in r)\}$ * $\mathrm{ran}(r) = \{b \mid \exists a.((a,b)\in r)\}$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let h {a,b| a∈1..10 ∧ b∈1..10 & b*2=a} :let h {a,b| a∈1..10 ∧ b∈1..10 & b*2=a}
``` ```
%% Output %% Output
$\{(2\mapsto 1),(4\mapsto 2),(6\mapsto 3),(8\mapsto 4),(10\mapsto 5)\}$ $\{(2\mapsto 1),(4\mapsto 2),(6\mapsto 3),(8\mapsto 4),(10\mapsto 5)\}$
{(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} {(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{a| ∃b.((a,b)∈h)} {a| ∃b.((a,b)∈h)}
``` ```
%% Output %% Output
$\{2,4,6,8,10\}$ $\{2,4,6,8,10\}$
{2,4,6,8,10} {2,4,6,8,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{b| ∃a.((a,b)∈h)} {b| ∃a.((a,b)∈h)}
``` ```
%% Output %% Output
$\{1,2,3,4,5\}$ $\{1,2,3,4,5\}$
{1,2,3,4,5} {1,2,3,4,5}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
dom(h) dom(h)
``` ```
%% Output %% Output
$\{2,4,6,8,10\}$ $\{2,4,6,8,10\}$
{2,4,6,8,10} {2,4,6,8,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let h {a,b| a∈1..10 ∧ b∈1..10 & b*2=a} :let h {a,b| a∈1..10 ∧ b∈1..10 & b*2=a}
``` ```
%% Output %% Output
$\{(2\mapsto 1),(4\mapsto 2),(6\mapsto 3),(8\mapsto 4),(10\mapsto 5)\}$ $\{(2\mapsto 1),(4\mapsto 2),(6\mapsto 3),(8\mapsto 4),(10\mapsto 5)\}$
{(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} {(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("h",h) :dot expr_as_graph ("h",h)
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN( <Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN(
("h",h) ("h",h)
)END]> )END]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let d {x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")} :let d {x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")}
``` ```
%% Output %% Output
$\{(1\mapsto\text{"nein"}),(2\mapsto\text{"nein"}),(3\mapsto\text{"ja"}),(4\mapsto\text{"nein"}),(5\mapsto\text{"nein"}),(6\mapsto\text{"ja"}),(7\mapsto\text{"nein"})\}$ $\{(1\mapsto\text{"nein"}),(2\mapsto\text{"nein"}),(3\mapsto\text{"ja"}),(4\mapsto\text{"nein"}),(5\mapsto\text{"nein"}),(6\mapsto\text{"ja"}),(7\mapsto\text{"nein"})\}$
{(1↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")} {(1↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
dom(d) dom(d)
``` ```
%% Output %% Output
$\{1,2,3,4,5,6,7\}$ $\{1,2,3,4,5,6,7\}$
{1,2,3,4,5,6,7} {1,2,3,4,5,6,7}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ran(d) ran(d)
``` ```
%% Output %% Output
$\{\text{"ja"},\text{"nein"}\}$ $\{\text{"ja"},\text{"nein"}\}$
{"ja","nein"} {"ja","nein"}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("d",d) :dot expr_as_graph ("d",d)
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET d,h BE d={(1↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")} & h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN( <Dot visualization: expr_as_graph [LET d,h BE d={(1↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")} & h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN(
("d",d) ("d",d)
)END]> )END]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Relationales Abbild und Umkehrrelation # Relationales Abbild und Umkehrrelation
Abbild: Abbild:
* $r[A] = \{b \mid \exists a.((a,b)\in r \wedge a\in A)\}$ * $r[A] = \{b \mid \exists a.((a,b)\in r \wedge a\in A)\}$
Umkehrrelation: Umkehrrelation:
* $r^{-1} = \{(b,a) \mid (a,b)\in r \}$ * $r^{-1} = \{(b,a) \mid (a,b)\in r \}$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
h[8..10] h[8..10]
``` ```
%% Output %% Output
$\{4,5\}$ $\{4,5\}$
{4,5} {4,5}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
d[{3,6}] d[{3,6}]
``` ```
%% Output %% Output
$\{\text{"ja"}\}$ $\{\text{"ja"}\}$
{"ja"} {"ja"}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
d[{0}] d[{0}]
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$ $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
d⁻¹ d⁻¹
``` ```
%% Output %% Output
$\{(\text{"ja"}\mapsto 3),(\text{"ja"}\mapsto 6),(\text{"nein"}\mapsto 1),(\text{"nein"}\mapsto 2),(\text{"nein"}\mapsto 4),(\text{"nein"}\mapsto 5),(\text{"nein"}\mapsto 7)\}$ $\{(\text{"ja"}\mapsto 3),(\text{"ja"}\mapsto 6),(\text{"nein"}\mapsto 1),(\text{"nein"}\mapsto 2),(\text{"nein"}\mapsto 4),(\text{"nein"}\mapsto 5),(\text{"nein"}\mapsto 7)\}$
{("ja"↦3),("ja"↦6),("nein"↦1),("nein"↦2),("nein"↦4),("nein"↦5),("nein"↦7)} {("ja"↦3),("ja"↦6),("nein"↦1),("nein"↦2),("nein"↦4),("nein"↦5),("nein"↦7)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("d⁻¹",d⁻¹) :dot expr_as_graph ("d⁻¹",d⁻¹)
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET d,h BE d={(1↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")} & h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN( <Dot visualization: expr_as_graph [LET d,h BE d={(1↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")} & h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN(
("d⁻¹",d⁻¹) ("d⁻¹",d⁻¹)
)END]> )END]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann natürlich auch beide Operatoren verknüpfen, zum Beispiel um herauszufinden welche Zahlen durch 3 teilbar sind: Man kann natürlich auch beide Operatoren verknüpfen, zum Beispiel um herauszufinden welche Zahlen durch 3 teilbar sind:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
d⁻¹[{"ja"}] d⁻¹[{"ja"}]
``` ```
%% Output %% Output
$\{3,6\}$ $\{3,6\}$
{3,6} {3,6}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet d :unlet d
``` ```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Binäre Relationen - Verknüpfung # Binäre Relationen - Verknüpfung
Wir können Relationen $r_1$ und $r_2$ mit dem Operator ";" verknüpfen: Wir können Relationen $r_1$ und $r_2$ mit dem Operator ";" verknüpfen:
* $(r_1 ; r_2)$ = $\{(a,c) \mid \exists b. ( (a,b)\in r_1 \wedge (b,c)\in r_2)\}$. * $(r_1 ; r_2)$ = $\{(a,c) \mid \exists b. ( (a,b)\in r_1 \wedge (b,c)\in r_2)\}$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
({1↦2, 2↦3} ; {2↦4, 2↦8}) ({1↦2, 2↦3} ; {2↦4, 2↦8})
``` ```
%% Output %% Output
$\{(1\mapsto 4),(1\mapsto 8)\}$ $\{(1\mapsto 4),(1\mapsto 8)\}$
{(1↦4),(1↦8)} {(1↦4),(1↦8)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann eine Relation auch mit sich selber verknüpfen wenn Werte- und Definitionsbereich kompatibel sind. Man kann eine Relation auch mit sich selber verknüpfen wenn Werte- und Definitionsbereich kompatibel sind.
Zum Beispiel $h^2 = (h;h)$: Zum Beispiel $h^2 = (h;h)$:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(h ; h) (h ; h)
``` ```
%% Output %% Output
$\{(4\mapsto 1),(8\mapsto 2)\}$ $\{(4\mapsto 1),(8\mapsto 2)\}$
{(4↦1),(8↦2)} {(4↦1),(8↦2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("h",h,"hh",(h;h)) :dot expr_as_graph ("h",h,"hh",(h;h))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN( <Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN(
("h",h,"hh",(h;h)) ("h",h,"hh",(h;h))
)END]> )END]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("hh",(h;h)) :dot expr_as_graph ("hh",(h;h))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN( <Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN(
("hh",(h;h)) ("hh",(h;h))
)END]> )END]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("h",(h)) :dot expr_as_graph ("h",(h))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN( <Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN(
("h",(h)) ("h",(h))
)END]> )END]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Transitive Hülle # Transitive Hülle
Gegeben eine Relation $r$ von $A$ nach $A$ Gegeben eine Relation $r$ von $A$ nach $A$
* $r^1 = r$ * $r^1 = r$
* $r^k = (r^{k-1} ; r) = (r ; r^{k-1})$ * $r^k = (r^{k-1} ; r) = (r ; r^{k-1})$
* $r^+ = \bigcup_{i\geq 1} r^i$ * $r^+ = \bigcup_{i\geq 1} r^i$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(h;h) (h;h)
``` ```
%% Output %% Output
$\{(4\mapsto 1),(8\mapsto 2)\}$ $\{(4\mapsto 1),(8\mapsto 2)\}$
{(4↦1),(8↦2)} {(4↦1),(8↦2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(h;h;h) (h;h;h)
``` ```
%% Output %% Output
$\{(8\mapsto 1)\}$ $\{(8\mapsto 1)\}$
{(8↦1)} {(8↦1)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(h;h;h;h) (h;h;h;h)
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$ $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die transitive Hülle wird in B als ```closure1``` geschrieben: Die transitive Hülle wird in B als ```closure1``` geschrieben:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
closure1(h) closure1(h)
``` ```
%% Output %% Output
$\{(2\mapsto 1),(4\mapsto 1),(4\mapsto 2),(6\mapsto 3),(8\mapsto 1),(8\mapsto 2),(8\mapsto 4),(10\mapsto 5)\}$ $\{(2\mapsto 1),(4\mapsto 1),(4\mapsto 2),(6\mapsto 3),(8\mapsto 1),(8\mapsto 2),(8\mapsto 4),(10\mapsto 5)\}$
{(2↦1),(4↦1),(4↦2),(6↦3),(8↦1),(8↦2),(8↦4),(10↦5)} {(2↦1),(4↦1),(4↦2),(6↦3),(8↦1),(8↦2),(8↦4),(10↦5)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("h⁺",closure1(h)) :dot expr_as_graph ("h⁺",closure1(h))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN( <Dot visualization: expr_as_graph [LET h BE h={(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)} IN(
("h⁺",closure1(h)) ("h⁺",closure1(h))
)END]> )END]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet h :unlet h
``` ```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Ein weiteres Beispiel ist folgende abgeänderte strikte Untermengenrelation $\subset$ für $ℙ(1 .. 3) $: Ein weiteres Beispiel ist folgende abgeänderte strikte Untermengenrelation $\subset$ für $ℙ(1 .. 3) $:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let sub1 {x,y|y:ℙ(1..3) & x ⊂ y & card(x)+1=card(y)} :let sub1 {x,y|y:ℙ(1..3) & x ⊂ y & card(x)+1=card(y)}
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\{(\emptyset\mapsto\{1\}),(\emptyset\mapsto\{2\}),(\emptyset\mapsto\{3\}),(\{1\}\mapsto\{1,2\}),(\{1\}\mapsto\{1,3\}),(\{1,2\}\mapsto\{1,2,3\}),(\{1,3\}\mapsto\{1,2,3\}),(\{2\}\mapsto\{1,2\}),(\{2\}\mapsto\{2,3\}),(\{2,3\}\mapsto\{1,2,3\}),(\{3\}\mapsto\{1,3\}),(\{3\}\mapsto\{2,3\})\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\{(\emptyset\mapsto\{1\}),(\emptyset\mapsto\{2\}),(\emptyset\mapsto\{3\}),(\{1\}\mapsto\{1,2\}),(\{1\}\mapsto\{1,3\}),(\{1,2\}\mapsto\{1,2,3\}),(\{1,3\}\mapsto\{1,2,3\}),(\{2\}\mapsto\{1,2\}),(\{2\}\mapsto\{2,3\}),(\{2,3\}\mapsto\{1,2,3\}),(\{3\}\mapsto\{1,3\}),(\{3\}\mapsto\{2,3\})\}$
{(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} {(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_DECOMPOSE_NODES=false :pref DOT_DECOMPOSE_NODES=false
``` ```
%% Output %% Output
Preference changed: DOT_DECOMPOSE_NODES = false Preference changed: DOT_DECOMPOSE_NODES = false
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("sub1",sub1) :dot expr_as_graph ("sub1",sub1)
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET sub1 BE sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN( <Dot visualization: expr_as_graph [LET sub1 BE sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN(
("sub1",sub1) ("sub1",sub1)
)END]> )END]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("sub1",closure1(sub1)) :dot expr_as_graph ("sub1",closure1(sub1))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET sub1 BE sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN( <Dot visualization: expr_as_graph [LET sub1 BE sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN(
("sub1",closure1(sub1)) ("sub1",closure1(sub1))
)END]> )END]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Transitive und Reflexive Hülle # Transitive und Reflexive Hülle
Gegeben eine Relation $r$ von $A$ nach $A$ Gegeben eine Relation $r$ von $A$ nach $A$
* $r^0 = \{(a,a) \mid a\in A\}$ * $r^0 = \{(a,a) \mid a\in A\}$
* $r^1 = r$ * $r^1 = r$
* $r^k = (r^{k-1} ; r) = (r ; r^{k-1})$ * $r^k = (r^{k-1} ; r) = (r ; r^{k-1})$
* $r^* = \bigcup_{i\geq 0} r^i$ * $r^* = \bigcup_{i\geq 0} r^i$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let A {1,2,3} :let A {1,2,3}
``` ```
%% Output %% Output
$\{1,2,3\}$ $\{1,2,3\}$
{1,2,3} {1,2,3}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let r {(1,2), (2,3)} :let r {(1,2), (2,3)}
``` ```
%% Output %% Output
$\{(1\mapsto 2),(2\mapsto 3)\}$ $\{(1\mapsto 2),(2\mapsto 3)\}$
{(1↦2),(2↦3)} {(1↦2),(2↦3)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("r",r) :dot expr_as_graph ("r",r)
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET A,r,sub1 BE A={1,2,3} & r={(1↦2),(2↦3)} & sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN( <Dot visualization: expr_as_graph [LET A,r,sub1 BE A={1,2,3} & r={(1↦2),(2↦3)} & sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN(
("r",r) ("r",r)
)END]> )END]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(r;r) (r;r)
``` ```
%% Output %% Output
$\{(1\mapsto 3)\}$ $\{(1\mapsto 3)\}$
{(1↦3)} {(1↦3)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In B kann man $r^0$ auch als die Identitätsrelation über A beschreiben: In B kann man $r^0$ auch als die Identitätsrelation über A beschreiben:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
id(A) id(A)
``` ```
%% Output %% Output
$\{(1\mapsto 1),(2\mapsto 2),(3\mapsto 3)\}$ $\{(1\mapsto 1),(2\mapsto 2),(3\mapsto 3)\}$
{(1↦1),(2↦2),(3↦3)} {(1↦1),(2↦2),(3↦3)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die transitive und reflexive Hülle ist hier: Die transitive und reflexive Hülle ist hier:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
id(A) \/ r \/ (r;r) \/ (r;r;r) \/ (r;r;r;r) id(A) \/ r \/ (r;r) \/ (r;r;r) \/ (r;r;r;r)
``` ```
%% Output %% Output
$\{(1\mapsto 1),(1\mapsto 2),(1\mapsto 3),(2\mapsto 2),(2\mapsto 3),(3\mapsto 3)\}$ $\{(1\mapsto 1),(1\mapsto 2),(1\mapsto 3),(2\mapsto 2),(2\mapsto 3),(3\mapsto 3)\}$
{(1↦1),(1↦2),(1↦3),(2↦2),(2↦3),(3↦3)} {(1↦1),(1↦2),(1↦3),(2↦2),(2↦3),(3↦3)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("r*",id(A) \/ r \/ (r;r) \/ (r;r;r) \/ (r;r;r;r)) :dot expr_as_graph ("r*",id(A) \/ r \/ (r;r) \/ (r;r;r) \/ (r;r;r;r))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET A,r,sub1 BE A={1,2,3} & r={(1↦2),(2↦3)} & sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN( <Dot visualization: expr_as_graph [LET A,r,sub1 BE A={1,2,3} & r={(1↦2),(2↦3)} & sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN(
("r*",id(A) \/ r \/ (r;r) \/ (r;r;r) \/ (r;r;r;r)) ("r*",id(A) \/ r \/ (r;r) \/ (r;r;r) \/ (r;r;r;r))
)END]> )END]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Als Vergleich dazu sieht die transitive Hülle so aus: Als Vergleich dazu sieht die transitive Hülle so aus:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
closure1(r) closure1(r)
``` ```
%% Output %% Output
$\{(1\mapsto 2),(1\mapsto 3),(2\mapsto 3)\}$ $\{(1\mapsto 2),(1\mapsto 3),(2\mapsto 3)\}$
{(1↦2),(1↦3),(2↦3)} {(1↦2),(1↦3),(2↦3)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("r⁺",closure1(r)) :dot expr_as_graph ("r⁺",closure1(r))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET A,r,sub1 BE A={1,2,3} & r={(1↦2),(2↦3)} & sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN( <Dot visualization: expr_as_graph [LET A,r,sub1 BE A={1,2,3} & r={(1↦2),(2↦3)} & sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN(
("r⁺",closure1(r)) ("r⁺",closure1(r))
)END]> )END]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann die transitive Hülle natürlich mit den anderen Operatoren verknüpfen, zum Beispiel um auszurechnen von welchen Knoten aus man den Knoten 3 erreichen kann: Man kann die transitive Hülle natürlich mit den anderen Operatoren verknüpfen, zum Beispiel um auszurechnen von welchen Knoten aus man den Knoten 3 erreichen kann:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
closure1(r)⁻¹[{3}] closure1(r)⁻¹[{3}]
``` ```
%% Output %% Output
$\{1,2\}$ $\{1,2\}$
{1,2} {1,2}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Anmerkung: die reflexive und transitive Hülle in B wird als ```closure``` geschrieben, ist bei Relationen über Zahlen immer unendlich. Anmerkung: die reflexive und transitive Hülle in B wird als ```closure``` geschrieben, ist bei Relationen über Zahlen immer unendlich.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
closure(r) closure(r)
``` ```
%% Output %% Output
$/*@\mathit{symbolic}*/ \{\mathit{z\_},\mathit{z\_\_}\mid\mathit{z\_} \mapsto \mathit{z\_\_} \in \{(1\mapsto 2),(1\mapsto 3),(2\mapsto 3)\} \lor \mathit{z\_} = \mathit{z\_\_}\}$ $/*@\mathit{symbolic}*/ \{\mathit{z\_},\mathit{z\_\_}\mid\mathit{z\_} \mapsto \mathit{z\_\_} \in \{(1\mapsto 2),(1\mapsto 3),(2\mapsto 3)\} \lor \mathit{z\_} = \mathit{z\_\_}\}$
/*@symbolic*/ {z_,z__∣z_ ↦ z__ ∈ {(1↦2),(1↦3),(2↦3)} ∨ z_ = z__} /*@symbolic*/ {z_,z__∣z_ ↦ z__ ∈ {(1↦2),(1↦3),(2↦3)} ∨ z_ = z__}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
closure(r)⁻¹[{3}] closure(r)⁻¹[{3}]
``` ```
%% Output %% Output
$\{1,2,3\}$ $\{1,2,3\}$
{1,2,3} {1,2,3}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet r :unlet r
``` ```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Funktionen # Funktionen
Was unterscheidet Funktionen von Relationen? Was unterscheidet Funktionen von Relationen?
Wie kann man Funktionen in Mengentheorie und Logik darstellen? Wie kann man Funktionen in Mengentheorie und Logik darstellen?
Eine Funktion kann als Menge an Paaren angesehen werden. Eine Funktion kann als Menge an Paaren angesehen werden.
Zum Beispiel ist die Inkrementfunktion (+1) eine unendliche Mengen an Paaren. Zum Beispiel ist die Inkrementfunktion (+1) eine unendliche Mengen an Paaren.
Die linke Komponente des Paares ist die Eingabe der Funktion, die rechte Komponente die Ausgabe. Die linke Komponente des Paares ist die Eingabe der Funktion, die rechte Komponente die Ausgabe.
Eingeschränkt auf den Bereich 1..10 sieht dies Funktion so aus: Eingeschränkt auf den Bereich 1..10 sieht dies Funktion so aus:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x,y|x:1..10 & y=x+1} {x,y|x:1..10 & y=x+1}
``` ```
%% Output %% Output
$\{(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 10),(10\mapsto 11)\}$ $\{(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 10),(10\mapsto 11)\}$
{(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)} {(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Eine Funktion kann also als Menge von Paaren dargestellt werden. Es sind aber nicht alle Mengen an Paaren auch Funktionen. Zum Beispiel, unsere Relation sub1 von oben ist keine Funktion: Eine Funktion kann also als Menge von Paaren dargestellt werden. Es sind aber nicht alle Mengen an Paaren auch Funktionen. Zum Beispiel, unsere Relation sub1 von oben ist keine Funktion:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("sub1",sub1) :dot expr_as_graph ("sub1",sub1)
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET A,sub1 BE A={1,2,3} & sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN( <Dot visualization: expr_as_graph [LET A,sub1 BE A={1,2,3} & sub1={(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} IN(
("sub1",sub1) ("sub1",sub1)
)END]> )END]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Eingabe ```{1}``` hat zwei mögliche Ausgaben (Nachfolger): ```{1,3}``` und ```{1,2}```. Die Eingabe $\emptyset$ hat drei mögliche Ausgaben: Die Eingabe ```{1}``` hat zwei mögliche Ausgaben (Nachfolger): ```{1,3}``` und ```{1,2}```. Die Eingabe $\emptyset$ hat drei mögliche Ausgaben:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
sub1 sub1
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\{(\emptyset\mapsto\{1\}),(\emptyset\mapsto\{2\}),(\emptyset\mapsto\{3\}),(\{1\}\mapsto\{1,2\}),(\{1\}\mapsto\{1,3\}),(\{1,2\}\mapsto\{1,2,3\}),(\{1,3\}\mapsto\{1,2,3\}),(\{2\}\mapsto\{1,2\}),(\{2\}\mapsto\{2,3\}),(\{2,3\}\mapsto\{1,2,3\}),(\{3\}\mapsto\{1,3\}),(\{3\}\mapsto\{2,3\})\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\{(\emptyset\mapsto\{1\}),(\emptyset\mapsto\{2\}),(\emptyset\mapsto\{3\}),(\{1\}\mapsto\{1,2\}),(\{1\}\mapsto\{1,3\}),(\{1,2\}\mapsto\{1,2,3\}),(\{1,3\}\mapsto\{1,2,3\}),(\{2\}\mapsto\{1,2\}),(\{2\}\mapsto\{2,3\}),(\{2,3\}\mapsto\{1,2,3\}),(\{3\}\mapsto\{1,3\}),(\{3\}\mapsto\{2,3\})\}$
{(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})} {(∅↦{1}),(∅↦{2}),(∅↦{3}),({1}↦{1,2}),({1}↦{1,3}),({1,2}↦{1,2,3}),({1,3}↦{1,2,3}),({2}↦{1,2}),({2}↦{2,3}),({2,3}↦{1,2,3}),({3}↦{1,3}),({3}↦{2,3})}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Eine (totale) Funktion $F$ von $A$ nach $B$ ist Eine (totale) Funktion $F$ von $A$ nach $B$ ist
* eine Relation von $A$ nach $B$ (also eine Untermenge von $A\times B$),so dass * eine Relation von $A$ nach $B$ (also eine Untermenge von $A\times B$),so dass
* $\forall a.( a\in A \Rightarrow \exists b.( (a,b) \in F))$ * $\forall a.( a\in A \Rightarrow \exists b.( (a,b) \in F))$
* $\forall (a,b,c).(((a,b)\in F \wedge (a,c)\in F) \Rightarrow b=c)$ * $\forall (a,b,c).(((a,b)\in F \wedge (a,c)\in F) \Rightarrow b=c)$
Wir schreiben dann $F \in A \rightarrow B$. Wir schreiben dann $F \in A \rightarrow B$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∀(a,b,c).((a,b)∈sub1 & (a,c)∈sub1 ⇒ b=c) ∀(a,b,c).((a,b)∈sub1 & (a,c)∈sub1 ⇒ b=c)
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
sub1 ∈ ℙ(1..3) --> ℙ(1..3) sub1 ∈ ℙ(1..3) --> ℙ(1..3)
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet sub1 :unlet sub1
``` ```
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let i10 {x,y|x:1..10 & y=x+1} :let i10 {x,y|x:1..10 & y=x+1}
``` ```
%% Output %% Output
$\{(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 10),(10\mapsto 11)\}$ $\{(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 10),(10\mapsto 11)\}$
{(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)} {(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∀(a,b,c).((a,b)∈i10 & (a,c)∈i10 ⇒ b=c) ∀(a,b,c).((a,b)∈i10 & (a,c)∈i10 ⇒ b=c)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10 ∈ 1..10 --> 2..11 i10 ∈ 1..10 --> 2..11
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Anmerkung: es wird nicht geprüft ob der komplette Wertebereich abgedeckt wird: Anmerkung: es wird nicht geprüft ob der komplette Wertebereich abgedeckt wird:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10 ∈ 1..10 --> 0..100 i10 ∈ 1..10 --> 0..100
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Es wird aber wohl geprüft ob der Definitionsbereich komplett abgedeckt wird: Es wird aber wohl geprüft ob der Definitionsbereich komplett abgedeckt wird:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10 ∈ 2..10 --> 0..100 i10 ∈ 2..10 --> 0..100
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10 ∈ 0..10 --> 0..100 i10 ∈ 0..10 --> 0..100
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
dom(i10) dom(i10)
``` ```
%% Output %% Output
$\{1,2,3,4,5,6,7,8,9,10\}$ $\{1,2,3,4,5,6,7,8,9,10\}$
{1,2,3,4,5,6,7,8,9,10} {1,2,3,4,5,6,7,8,9,10}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Was kann man mit Funktionen machen? Da Funktionen *nur* besondere Relationen sind, und Relationen *nur* besondere Mengen sind, kann man alle Mengen und Relationsoperatoren anwenden: Was kann man mit Funktionen machen? Da Funktionen *nur* besondere Relationen sind, und Relationen *nur* besondere Mengen sind, kann man alle Mengen und Relationsoperatoren anwenden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(4,z) ∈ i10 (4,z) ∈ i10
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{z} = 5$ * $\mathit{z} = 5$
TRUE TRUE
Solution: Solution:
z = 5 z = 5
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
dom(i10) dom(i10)
``` ```
%% Output %% Output
$\{1,2,3,4,5,6,7,8,9,10\}$ $\{1,2,3,4,5,6,7,8,9,10\}$
{1,2,3,4,5,6,7,8,9,10} {1,2,3,4,5,6,7,8,9,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ran(i10) ran(i10)
``` ```
%% Output %% Output
$\{2,3,4,5,6,7,8,9,10,11\}$ $\{2,3,4,5,6,7,8,9,10,11\}$
{2,3,4,5,6,7,8,9,10,11} {2,3,4,5,6,7,8,9,10,11}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10[{4,5}] i10[{4,5}]
``` ```
%% Output %% Output
$\{5,6\}$ $\{5,6\}$
{5,6} {5,6}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10[{4}] i10[{4}]
``` ```
%% Output %% Output
$\{5\}$ $\{5\}$
{5} {5}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10⁻¹[{4}] i10⁻¹[{4}]
``` ```
%% Output %% Output
$\{3\}$ $\{3\}$
{3} {3}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(i10 ; i10)[{4}] (i10 ; i10)[{4}]
``` ```
%% Output %% Output
$\{6\}$ $\{6\}$
{6} {6}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
closure1(i10)[{4}] closure1(i10)[{4}]
``` ```
%% Output %% Output
$\{5,6,7,8,9,10,11\}$ $\{5,6,7,8,9,10,11\}$
{5,6,7,8,9,10,11} {5,6,7,8,9,10,11}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
closure1(i10~)[{4}] closure1(i10~)[{4}]
``` ```
%% Output %% Output
$\{1,2,3\}$ $\{1,2,3\}$
{1,2,3} {1,2,3}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Anmerkung: um den Wert einer Funktion $F$ für eine Eingabe $x$ zu berechnen, kann man das relationale Bild $F[\{x\}]$ verwenden. Aber: das Ergebnis ist eine Menge! Man kann also nicht direkt zB arithmetische Operatoren anwenden. Dafür wird eine neue Operation für Funktionen eingeführt: die **Funktionsanwendung**: ```F(x)```. Anmerkung: um den Wert einer Funktion $F$ für eine Eingabe $x$ zu berechnen, kann man das relationale Bild $F[\{x\}]$ verwenden. Aber: das Ergebnis ist eine Menge! Man kann also nicht direkt zB arithmetische Operatoren anwenden. Dafür wird eine neue Operation für Funktionen eingeführt: die **Funktionsanwendung**: ```F(x)```.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10(4) i10(4)
``` ```
%% Output %% Output
$5$ $5$
5 5
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10(4) + i10(4) i10(4) + i10(4)
``` ```
%% Output %% Output
$10$ $10$
10 10
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Es ist ein Fehler eine Funktion ausserhalb des Definitionsbereiches anzuwenden. Beim relationalen Bild ist dies erlaubt und man bekommt dort die leere Menge als Ausgabe. Es ist ein Fehler eine Funktion ausserhalb des Definitionsbereiches anzuwenden. Beim relationalen Bild ist dies erlaubt und man bekommt dort die leere Menge als Ausgabe.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10[{100}] i10[{100}]
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$ $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10 i10
``` ```
%% Output %% Output
$\{(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 10),(10\mapsto 11)\}$ $\{(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 10),(10\mapsto 11)\}$
{(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)} {(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
i10(100) i10(100)
``` ```
%% Output %% Output
:eval: NOT-WELL-DEFINED: :eval: NOT-WELL-DEFINED:
function applied outside of domain (#7): Function argument: 100, function value: {} function applied outside of domain (#7): Function argument: 100, function value: {}
### Line: 2, Column: 0 until 8 ### Line: 2, Column: 0 until 8
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Alle möglichen Funktionen über einen Definitionsbereich ergeben wieder eine Menge: Alle möglichen Funktionen über einen Definitionsbereich ergeben wieder eine Menge:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..2 --> 1..2 1..2 --> 1..2
``` ```
%% Output %% Output
$\{\{(1\mapsto 1),(2\mapsto 1)\},\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\},\{(1\mapsto 2),(2\mapsto 2)\}\}$ $\{\{(1\mapsto 1),(2\mapsto 1)\},\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\},\{(1\mapsto 2),(2\mapsto 2)\}\}$
{{(1↦1),(2↦1)},{(1↦1),(2↦2)},{(1↦2),(2↦1)},{(1↦2),(2↦2)}} {{(1↦1),(2↦1)},{(1↦1),(2↦2)},{(1↦2),(2↦1)},{(1↦2),(2↦2)}}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Es gibt auch noch andere Arten an Funktionen: Es gibt auch noch andere Arten an Funktionen:
* partielle Funktionen, `+->` * partielle Funktionen, `+->`
* injektive (umkehrbare) Funktionen `>->` * injektive (umkehrbare) Funktionen `>->`
* surjektive Funktionen die den Wertebereich komplett abdecken `-->>` * surjektive Funktionen die den Wertebereich komplett abdecken `-->>`
* injektive und surjektive Funktionen `>->>`, auch Bijektionen gennant * injektive und surjektive Funktionen `>->>`, auch Bijektionen gennant
(Die Pfeilsymbole sind sehr spezifisch für die B-Sprache. Wir werden diese nicht im Skript verwenden.) (Die Pfeilsymbole sind sehr spezifisch für die B-Sprache. Wir werden diese nicht im Skript verwenden.)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..2 +-> 1..2 1..2 +-> 1..2
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{(1\mapsto 1)\},\{(1\mapsto 1),(2\mapsto 1)\},\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\},\{(1\mapsto 2),(2\mapsto 2)\},\{(2\mapsto 1)\},\{(2\mapsto 2)\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{(1\mapsto 1)\},\{(1\mapsto 1),(2\mapsto 1)\},\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\},\{(1\mapsto 2),(2\mapsto 2)\},\{(2\mapsto 1)\},\{(2\mapsto 2)\}\}$
{∅,{(1↦1)},{(1↦1),(2↦1)},{(1↦1),(2↦2)},{(1↦2)},{(1↦2),(2↦1)},{(1↦2),(2↦2)},{(2↦1)},{(2↦2)}} {∅,{(1↦1)},{(1↦1),(2↦1)},{(1↦1),(2↦2)},{(1↦2)},{(1↦2),(2↦1)},{(1↦2),(2↦2)},{(2↦1)},{(2↦2)}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1..2 --> 1..2) <: (1..2 +-> 1..2) (1..2 --> 1..2) <: (1..2 +-> 1..2)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Folgende fünf Funktionen sind partiell und nicht total: Folgende fünf Funktionen sind partiell und nicht total:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1..2 +-> 1..2) \ (1..2 --> 1..2) (1..2 +-> 1..2) \ (1..2 --> 1..2)
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{(1\mapsto 1)\},\{(1\mapsto 2)\},\{(2\mapsto 1)\},\{(2\mapsto 2)\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{(1\mapsto 1)\},\{(1\mapsto 2)\},\{(2\mapsto 1)\},\{(2\mapsto 2)\}\}$
{∅,{(1↦1)},{(1↦2)},{(2↦1)},{(2↦2)}} {∅,{(1↦1)},{(1↦2)},{(2↦1)},{(2↦2)}}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Das sind die totalen umkehrbaren Funktionen: Das sind die totalen umkehrbaren Funktionen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..2 >-> 1..2 1..2 >-> 1..2
``` ```
%% Output %% Output
$\{\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\}\}$ $\{\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\}\}$
{{(1↦1),(2↦2)},{(1↦2),(2↦1)}} {{(1↦1),(2↦2)},{(1↦2),(2↦1)}}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In diesem Falle sind diese identisch zu den surjektiven Funktionen und den Bijektionen: In diesem Falle sind diese identisch zu den surjektiven Funktionen und den Bijektionen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..2 -->> 1..2 1..2 -->> 1..2
``` ```
%% Output %% Output
$\{\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\}\}$ $\{\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\}\}$
{{(1↦1),(2↦2)},{(1↦2),(2↦1)}} {{(1↦1),(2↦2)},{(1↦2),(2↦1)}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..2 >->> 1..2 1..2 >->> 1..2
``` ```
%% Output %% Output
$\{\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\}\}$ $\{\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\}\}$
{{(1↦1),(2↦2)},{(1↦2),(2↦1)}} {{(1↦1),(2↦2)},{(1↦2),(2↦1)}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet i10 :unlet i10
``` ```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Endliche Folgen # Endliche Folgen
Es gibt verschiedene Schreibweisen für endliche Folgen. Es gibt verschiedene Schreibweisen für endliche Folgen.
Zum Beispiel $[1,2]$ ist eine Folge bestehend aus der Zahl 1 gefolgt von der Zahl 2. Zum Beispiel $[1,2]$ ist eine Folge bestehend aus der Zahl 1 gefolgt von der Zahl 2.
(Anmerkung: Im Skript werden wir eine andere Schreibweise verwenden. Zum Beispiel, $ab$ ist die (Anmerkung: Im Skript werden wir eine andere Schreibweise verwenden. Zum Beispiel, $ab$ ist die
Folge bestehen aus dem Symbol $a$ gefolgt von $b$. Folge bestehen aus dem Symbol $a$ gefolgt von $b$.
Diese Schreibweise ist zwar kompakter, aber nicht immer eindeutig und nicht für eine maschinelle Verarbeitung geeeignet.) Diese Schreibweise ist zwar kompakter, aber nicht immer eindeutig und nicht für eine maschinelle Verarbeitung geeeignet.)
Was unterscheidet Folgen von Mengen? Was unterscheidet Folgen von Mengen?
Wie kann man Folgen in Mengentheorie und Logik darstellen? Wie kann man Folgen in Mengentheorie und Logik darstellen?
## Endliche Folgen vs Mengen ## Endliche Folgen vs Mengen
Die Reihenfolge der Elemente ist wichtig: Die Reihenfolge der Elemente ist wichtig:
* $[1,2] \neq [2,1] $, während * $[1,2] \neq [2,1] $, während
* $\{1,2\} = \{2,1\} $ * $\{1,2\} = \{2,1\} $
Elemente können mehrfach auftauchen: Elemente können mehrfach auftauchen:
* $[1,1] \neq [1] $, während * $[1,1] \neq [1] $, während
* $\{1,1\} = \{1\} $ * $\{1,1\} = \{1\} $
Wie kann man Folgen in Mengentheorie und Logik darstellen? Wie kann man Folgen in Mengentheorie und Logik darstellen?
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Endliche Folgen mathematisch gesehen ## Endliche Folgen mathematisch gesehen
Eine (endliche) Folge $G$ von $A$ Elementen der Länge $n$ ist Eine (endliche) Folge $G$ von $A$ Elementen der Länge $n$ ist
* eine (totale) Funktion von $1..n$ nach $A$. * eine (totale) Funktion von $1..n$ nach $A$.
Da eine totale Funktion eine Menge an Paare ist, haben wir zum Beispiel: Da eine totale Funktion eine Menge an Paare ist, haben wir zum Beispiel:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let G [22,22,33] :let G [22,22,33]
``` ```
%% Output %% Output
$\{(1\mapsto 22),(2\mapsto 22),(3\mapsto 33)\}$ $\{(1\mapsto 22),(2\mapsto 22),(3\mapsto 33)\}$
{(1↦22),(2↦22),(3↦33)} {(1↦22),(2↦22),(3↦33)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
G G
``` ```
%% Output %% Output
$\{(1\mapsto 22),(2\mapsto 22),(3\mapsto 33)\}$ $\{(1\mapsto 22),(2\mapsto 22),(3\mapsto 33)\}$
{(1↦22),(2↦22),(3↦33)} {(1↦22),(2↦22),(3↦33)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("G",G) :dot expr_as_graph ("G",G)
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [LET A,G BE A={1,2,3} & G={(1↦22),(2↦22),(3↦33)} IN( <Dot visualization: expr_as_graph [LET A,G BE A={1,2,3} & G={(1↦22),(2↦22),(3↦33)} IN(
("G",G) ("G",G)
)END]> )END]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Es gilt also Es gilt also
* $G = [22,22,33] = \{(1\mapsto 22),(2\mapsto 22),(3\mapsto 33)\}$ * $G = [22,22,33] = \{(1\mapsto 22),(2\mapsto 22),(3\mapsto 33)\}$
Wir schreiben $\mathit{G} \in \mathrm{seq}(\mathbb{Z})$ Wir schreiben $\mathit{G} \in \mathrm{seq}(\mathbb{Z})$
oder aber auch $G \in \mathbb{Z}^*$ (mehr dazu später im Skript) oder aber auch $G \in \mathbb{Z}^*$ (mehr dazu später im Skript)
Das n-te Element einer Folge $G$ ist einfach $G(n)$: Das n-te Element einer Folge $G$ ist einfach $G(n)$:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
G(2) G(2)
``` ```
%% Output %% Output
$22$ $22$
22 22
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Länge einer Folge (```size``` in B) ist einfach die Kardinalität der unterliegenden Relation: Die Länge einer Folge (```size``` in B) ist einfach die Kardinalität der unterliegenden Relation:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
size(G) size(G)
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(G) card(G)
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir können alle anderen Menge und Relationsoperatoren auf Folgen anwenden: Wir können alle anderen Menge und Relationsoperatoren auf Folgen anwenden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
dom(G) dom(G)
``` ```
%% Output %% Output
$\{1,2,3\}$ $\{1,2,3\}$
{1,2,3} {1,2,3}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ran(G) ran(G)
``` ```
%% Output %% Output
$\{22,33\}$ $\{22,33\}$
{22,33} {22,33}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
G⁻¹[{22}] G⁻¹[{22}]
``` ```
%% Output %% Output
$\{1,2\}$ $\{1,2\}$
{1,2} {1,2}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet G :unlet G
``` ```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Zusammenfassung Mengentheorie # Zusammenfassung Mengentheorie
* Mengen, Notationen (per Prädikat) * Mengen, Notationen (per Prädikat)
* Potenzmenge, Menge von Mengen, $\phi \neq \{\phi\}$ * Potenzmenge, Menge von Mengen, $\phi \neq \{\phi\}$
* kartesisches Produkt, Relationen als Menge von Paaren/Tupeln * kartesisches Produkt, Relationen als Menge von Paaren/Tupeln
* Definitionsbereich, Wertebereich, Abbild, Umkehrrelation * Definitionsbereich, Wertebereich, Abbild, Umkehrrelation
* Transitive Hülle * Transitive Hülle
* Funktionen * Funktionen
* Endliche Folgen als Funktion von $\mathbb{Z}$ nach Wertebereich * Endliche Folgen als Funktion von $\mathbb{Z}$ nach Wertebereich
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Lernziele von Kapitel 0 # Lernziele von Kapitel 0
* logische Formeln verstehen und schreiben können * logische Formeln verstehen und schreiben können
* logische Beweise verstehen: Wahrheitstabelle, Widerspruch, Deduktiver Beweis, Äuivalenzbeweis * logische Beweise verstehen: Wahrheitstabelle, Widerspruch, Deduktiver Beweis, Äuivalenzbeweis
* Mengenausdrücke verstehen und nach Logik übersetzen können * Mengenausdrücke verstehen und nach Logik übersetzen können
* Problemstellungen nach Logik und Mengentheorie übersetzen können * Problemstellungen nach Logik und Mengentheorie übersetzen können
* Relationen, Funktionen und Folgen in Mengendarstellung bearbeiten können * Relationen, Funktionen und Folgen in Mengendarstellung bearbeiten können
......
This diff is collapsed.