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
  • master
1 result

Target

Select target project
  • general/stups/prob-teaching-notebooks
1 result
Select Git revision
  • master
1 result
Show changes
Commits on Source (2)
  • dgelessus's avatar
    Update URLs · c8e3c165
    dgelessus authored
    c8e3c165
  • dgelessus's avatar
    Force use of old Jupyter Notebook interface · bea76b55
    dgelessus authored 
    In JupyterLab, it's much harder to trust an entire notebook, whereas in
the old interface, the user just needs to click on "Not Trusted".
Linking to a directory of notebooks also works better with the old
interface - in JupyterLab, the sidebar is automatically hidden, which
makes it very unclear that the user is supposed to select a notebook.
    bea76b55
Show whitespace changes
Inline Side-by-side
README.md
View file @ bea76b55
[![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/master)
[![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)
# Various Notebooks for Teaching
These notebooks are made for the [ProB Jupyter kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel).
[ProB](https://www3.hhu.de/stups/prob) is a validation tool for formal methods, in particular for the B method.
[ProB](https://prob.hhu.de/w/) is a validation tool for formal methods, in particular for the B method.
At its heart is a constraint solver for logic, set theory and arithmetic.
These notebooks were developed by the [STUPS group](https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen.html) of the [University of Düsseldorf](https://www.uni-duesseldorf.de).
These notebooks were developed by the [STUPS group](https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen.html) of the [University of Düsseldorf](https://www.hhu.de).
To view the formatted output of ProB you may have to click in the upper right corner on "Not Trusted". Once a notebook is trusted, JavaScript is enabled and can render formulas, tables and figures.
\ No newline at end of file
binder/postBuild
View file @ bea76b55
......@@ -13,8 +13,8 @@ then
# (Note: doesn't work for past snapshot versions.)
DOWNLOAD_URL="https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/${JAR_NAME}?job=test"
else
# Release version - download from www3.
DOWNLOAD_URL="https://www3.hhu.de/stups/downloads/prob2-jupyter/${JAR_NAME}"
# Release version - download from regular server.
DOWNLOAD_URL="https://stups.hhu-hosting.de/downloads/prob2-jupyter/${JAR_NAME}"
fi
wget --output-document="${JAR_NAME}" "${DOWNLOAD_URL}"
......
info4/kapitel-0/Logik.ipynb
View file @ bea76b55
%% Cell type:markdown id: tags:
# Theoretische Informatik - Vorlesung 0 - Teil 1 Logik
* April 2020
* Michael Leuschel
* Lehrstuhl Softwaretechnik und Programmiersprachen
* Heinrich-Heine Universität Düsseldorf
Grundlagen der Logik und Mengentheorie sind nicht im Skript.
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.
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:
## Was ist ein Notebook?
* Dokument mit Text und ausführbaren Code-Abschnitten
* Code kann interaktiv ausgeführt werden
* Ergebnisse erscheinen im Notebook unter dem jeweiligem Code
* Ähnlich wie eine REPL (read-eval-print-loop), mit einigen Unterschieden:
* Ausgaben können formatierten Text und Grafiken enthalten
* Speicherbar als Datei
* Code kann später neu ausgeführt werden
* Weitergabe an andere Nutzer möglich
* Implementierungen: Mathematica, Maple, Jupyter, u. a.
%% Cell type:markdown id: tags:
## Jupyter Notebook
* Browserbasierte Notebook-Oberfläche
* Open Source und plattformübergreifend
* Stammt aus der Python-Community, in Python implementiert
* ACM System Software Award 2017
* Jupyter-Notebooks verschiedene Programmiersprachen verwenden
* Ein sprachspezifischer **Kernel** stellt die Sprache dem Jupyter Frontend zur Verfügung
%% Cell type:markdown id: tags:
## [ProB](https://www3.hhu.de/stups/prob) Kernel
## [ProB](https://prob.hhu.de/w/) Kernel
![ProB](img/prob_logo.png)
* [ProB](https://www3.hhu.de/stups/prob) 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
* Entwicklung am STUPS Lehrstuhl
* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.
* 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
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):
[![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/master)
[![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.
%% Cell type:markdown id: tags:
# Was ist Logik?
Quelle [Wikipedia](https://de.wikipedia.org/wiki/Logik):
* 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
* 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.
%% Cell type:markdown id: tags:
# Warum Logik studieren?
* Hardware: logische Schaltkreise
* Wissensdarstellung und intelligentes Denken: Künstliche Intelligenz, deklarative Darstellung von Wissen, semantisches Web, ...
* Überlegungen über Programme: Verifikation, statische Programmanalyse, Programmoptimierung,...
* Universale Vorrichtung zur Berechnung: Datenbanken, logische Programmierung, ...
* 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
* 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.```
%% Cell type:markdown id: tags:
# Welche Logik studieren?
* Aussagenlogik
* Prädikatenlogik der ersten Stufe (FOL - First Order Logic)
* Logik höherer Stufe (HOL - Higher Order Logic)
* eine temporale Logik
* eine mehrwertige Logik oder gar Fuzzy Logik
* Relevanzlogik, lineare Logik
* eine nichtmonotone Logik
Wir werden die klassische, zweiwertige, monotone **Aussagenlogik**
und **Prädikatenlogik** studieren (zusammen mit Mengentheorie).
%% Cell type:markdown id: tags:
# Aussagenlogik
Eine Aussage ist endweder wahr (TRUE) oder falsch (FALSE).
Hier sind vier Aussagen:
1. Siegfried ist ein Ritter
2. Alle Ritter sagen die Wahrheit
3. Siegfried sagt "Ich habe 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.
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.
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:
%% Cell type:code id: tags:
``` prob
2>1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
1+1 = 2
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2<1
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
# Junktoren und Formeln
Jede Aussage ist auch eine Formel der Aussagenlogik.
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:
%% Cell type:code id: tags:
``` prob
¬(2<1)
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
¬(1+1=2)
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
In diesen Notebooks muss der Inhalt der Negation immer geklammert werden. Im Skript ist das nicht immer nötig.
%% Cell type:markdown id: tags:
Die Konjunktion ```F ∧ G``` von zwei Formeln ist wahr gdw beide Formeln wahr sind:
%% Cell type:code id: tags:
``` prob
2>1 ∧ 1>0
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2>1 ∧ 1>2
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
Die Disjunktion ```F ∨ G``` von zwei Formeln ist wahr gdw mindestes eine der beiden Formeln wahr sind:
%% Cell type:code id: tags:
``` prob
1>1 ∨ 1>2
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
2>1 ∨ 3>1
```
%% Output
$\mathit{TRUE}$
TRUE
%% 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:
%% Cell type:code id: tags:
``` prob
2>1 ⇒ 3>1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2<1 ⇒ 1+1 = 5
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2>1 ⇒ 1+1=5
```
%% Output
$\mathit{FALSE}$
FALSE
%% 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:
%% Cell type:code id: tags:
``` prob
1=2 ⇔ 2=1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
1=3 ⇔ 1=1024
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
1=1 ⇔ 2=3
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
## Prioritäten
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)$.
Eine Formel kann man immer als einen Baum sehen
%% Cell type:code id: tags:
``` prob
:pref OPTIMIZE_AST=FALSE
```
%% Output
Preference changed: OPTIMIZE_AST = FALSE
%% Cell type:code id: tags:
``` prob
:dot formula_tree (2>3 ⇒ 4>1) ⇔ ¬(5<1)
```
%% Output
<Dot visualization: formula_tree [(2>3 => 4>1) <=> not(5<1)]>
%% Cell type:markdown id: tags:
# Wahrheitstabellen
Die Bedeutung der Junktoren der Aussagenlogik kann man in folgender Wahrheitstabelle zusammenfassen:
<img src="./img/wahrheitstabelle.png" width="600">
Wie berechnet man damit den Wahrheitswert einer Formel wie $(p \vee (\neg p \wedge q))$?
%% Cell type:markdown id: tags:
## Interpretationen
Man braucht erst die Wahrheitswerte für die atomaren Aussagen $p$ und $q$.
Diese Information nennt man eine <b>Interpretation</b> für die Formel.
Die Formel oben hat 4 Interpretationen, da $p$ und $q$ jeweils wahr oder falsch sein können.
Mit einer Interpretation kann man nun
* den Wahrheitswert aller (atomaren) Aussagen berechnen
* und mit der Wahrheitstabelle dann den Wert von immer grösseren Unterformeln berechnen.
Beispiel:
Sei $i$ = $\{p\mapsto TRUE,q\mapsto FALSE\}$ eine Interpretation für die Formel $(p \vee (\neg p \wedge q))$.
* Schritt 1: alle Aussagen berechnen: $~(TRUE \vee (\neg TRUE \wedge FALSE)$
* Schritt 2: $\neg TRUE = FALSE$: $~(TRUE \vee (FALSE \wedge FALSE)$
* Schritt 3: $FALSE \wedge FALSE = FALSE$: $~(TRUE \vee FALSE)$
* Schritt 3: $TRUE \vee FALSE = TRUE$: $~TRUE$
Unter der Interpretation $i$ ist die Formel $(p \vee (\neg p \wedge q)$ wahr.
%% Cell type:markdown id: tags:
## Modelle
Man nennt so eine Interpretation ein <b>Modell</b> für die Formel.
* eine Interpretation $i$ so dass $i(\phi)={\color{olive}{TRUE}}$ ist ein <b>Modell</b> für $\phi$
* eine Formel $\phi$ die mindestens ein Modell hat heißt <b>erfüllbar</b>
* eine Formel $\phi$ wo alle Interpretationen auch Modelle sind wird eine <b>Tautologie</b> genannt
* eine Formel ohne Modell heißt <b>unerfüllbar</b> oder ein Widerspruch
Die Interpretation $i'$ = $\{p\mapsto FALSE,q\mapsto FALSE\}$ ist kein Modell von $(p \vee (\neg p \wedge q))$.
Die Formel ist also keine Tautologie, aber erfüllbar.
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.
%% Cell type:markdown id: tags:
# Äquivalenz von Formeln
Zwei Formeln sind <b>äquivalent</b> gdw sie die selben Modelle haben.
$(p \vee (\neg p \wedge q))$ ist zum Beispiel äquivalent zu $p \vee q$.
Hier stellen wir die Interpretationen und Modelle tabellarisch dar:
%% Cell type:code id: tags:
``` prob
:table {p,q,F1,F2| p:BOOL & q:BOOL &
F1=bool(p=TRUE ∨ (¬(p=TRUE) ∧ q=TRUE)) & // p ∨ (¬p ∧ q)
F2=bool(p=TRUE ∨ q=TRUE) // p ∨ q
}
```
%% Output
|p|q|F1|F2|
|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
p q F1 F2
FALSE FALSE FALSE FALSE
FALSE TRUE TRUE TRUE
TRUE FALSE TRUE TRUE
TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags:
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.
$\equiv$ ist eine Relation zwischen logischen Formeln.
$\equiv$ ist transitiv und kommutativ.
%% Cell type:markdown id: tags:
# Wichtige Äquivalenzen
Für alle Formeln $\phi, \psi$ der Aussagenlogik gilt:
* $\phi \wedge \psi \equiv \psi \wedge \phi$ (Kommutativität)
* $\phi \vee \psi \equiv \psi \vee \phi$ (Kommutativität)
Mit diesen Regeln kann man $\Rightarrow$ und $\Leftrightarrow$ umwandeln:
* $\phi \Rightarrow \psi \equiv (\neg \phi) \vee \psi$
* $\phi \Leftrightarrow \psi \equiv (\phi \Rightarrow \psi) \wedge (\psi \Rightarrow \phi)$
Mit diesen Regeln kann man die Negation zu den atomaren Aussagen verschieben:
* $\neg \neg \phi \equiv \phi$
* $\neg(\phi \wedge \psi) \equiv (\neg \phi) \vee (\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:
%% Cell type:code id: tags:
``` prob
: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) &
NODER = bool(¬(ODER=TRUE)) &
NUND=bool((np=TRUE) ∧ (nq=TRUE))}
```
%% Output
|p|q|ODER|NODER|NUND|np|nq|
|---|---|---|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
p q ODER NODER NUND np nq
FALSE FALSE FALSE TRUE TRUE TRUE TRUE
FALSE TRUE TRUE FALSE FALSE TRUE FALSE
TRUE FALSE TRUE FALSE FALSE FALSE TRUE
TRUE TRUE TRUE FALSE FALSE FALSE FALSE
%% Cell type:markdown id: tags:
## Kontraposition
$\neg \psi \Rightarrow \neg \phi$ ist die Kontraposition von $\phi \Rightarrow \psi$.
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$
%% Cell type:code id: tags:
``` prob
: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) &
KONT=bool((nq=TRUE) => (np=TRUE))}
```
%% Output
|p|q|IMPL|KONT|np|nq|
|---|---|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
p q IMPL KONT np nq
FALSE FALSE TRUE TRUE TRUE TRUE
FALSE TRUE TRUE TRUE TRUE FALSE
TRUE FALSE FALSE FALSE FALSE TRUE
TRUE TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags:
Es gilt also:
$\phi \Rightarrow \psi$ $\equiv$ $\neg \psi \Rightarrow \neg \phi$ .
%% Cell type:markdown id: tags:
# Logisches Schließen
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$
* 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 beiden Formeln sind nicht äquivalent.
%% Cell type:code id: tags:
``` prob
:table {p,q,F1,F2| p:BOOL & q:BOOL & F1=bool(p=TRUE ⇔ q=TRUE) & F2=bool(p=TRUE ⇒ q=TRUE)}
```
%% Output
|p|q|F1|F2|
|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
p q F1 F2
FALSE FALSE TRUE TRUE
FALSE TRUE FALSE TRUE
TRUE FALSE FALSE FALSE
TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags:
# Wichtige logische Schlussfolgerungen
Für alle Formeln $\phi, \psi$ gilt:
* $\phi \wedge \psi \models \phi$
* $(\phi \Rightarrow \psi) \wedge \phi \models \psi$ (Modus Ponens)
* $(\phi \Rightarrow \psi) \wedge \neg\psi \models \neg\phi$ (Modus Tollens)
Beispiel: $\phi$ = "Es regnet", $\psi$ = "Die Straße wird nass".
* $(\phi \Leftrightarrow \psi) \wedge \psi \models \phi$
* $(\phi \Leftrightarrow \psi) \wedge \neg\psi \models \neg\phi$
Achtung $\phi \wedge \neg \phi \models \psi$ für beliebiges $\psi$ !
Also:
* $1>2 \models 1+1=100$
%% Cell type:markdown id: tags:
# Smullyan - Einfaches Puzzle
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
* Schurken die immer lügen.
Hier ist ein Puzzle aus einem seiner Bücher:
* X sagt: ```Y ist ein Ritter```
* Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```
Können wir bestimmen ob X und Y Ritter oder Schurken sind?
%% Cell type:markdown id: tags:
## Lösen des Puzzles
Schritt 1: was sind die Aussagen?
* $X$: die Person X ist ein Ritter
* $Y$: die Person Y ist ein Ritter
Schritt 2: Übersetzung der Informationen in Aussagenlogik
* $\mathit{X} \Leftrightarrow \mathit{Y}$ ist die Übersetzung von:
* X sagt: ```Y ist ein Ritter```
* $\mathit{Y} \Leftrightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von:
* Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```
Schritt 3: Bestimmung der Modelle:
%% Cell type:code id: tags:
``` prob
:table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇔ y=TRUE) &
S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE)}
```
%% Output
|x|y|S1|S2|Puzzle|
|---|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
x y S1 S2 Puzzle
FALSE FALSE TRUE TRUE TRUE
FALSE TRUE FALSE TRUE FALSE
TRUE FALSE FALSE FALSE FALSE
TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags:
Unser Puzzle hat nur ein einziges Modell und beide Personen sind also Schurken.
Ein typische fehlerhafte Übersetzung des Puzzles ist diese:
* $\mathit{X} \Rightarrow \mathit{Y}$ ist die Übersetzung von:
* X sagt: ```Y ist ein Ritter```
* $\mathit{Y} \Rightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von:
* Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```
%% Cell type:code id: tags:
``` prob
:table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇒ y=TRUE) &
S2=bool(y=TRUE ⇒ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE)}
```
%% Output
|x|y|S1|S2|Puzzle|
|---|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
x y S1 S2 Puzzle
FALSE FALSE TRUE TRUE TRUE
FALSE TRUE TRUE TRUE TRUE
TRUE FALSE FALSE TRUE FALSE
TRUE TRUE TRUE FALSE FALSE
%% 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.
%% Cell type:markdown id: tags:
# Beweis durch Widerspruch
* Theorem: $\phi \models \psi$ genau dann wenn $\phi \wedge \neg \psi$ kein Modell hat
Beweis (ist ein Äquivalenzbeweis auf Metaebene):
* $\phi \models \psi$
* $\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$ 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)
%% Cell type:markdown id: tags:
Anwendung auf unser Puzzle:
* 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)
* Wir haben $\phi \models \psi$ und
* $\phi \wedge \neg \psi$ ist ein Widerspruch:
%% Cell type:code id: tags:
``` prob
:table {x,y,S1,S2,Puzzle,WS | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇔ y=TRUE) &
S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE) &
WS=bool(Puzzle=TRUE & not( not(x=TRUE) & not(y=TRUE)))}
```
%% Output
|x|y|S1|S2|Puzzle|WS|
|---|---|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
x y S1 S2 Puzzle WS
FALSE FALSE TRUE TRUE TRUE FALSE
FALSE TRUE FALSE TRUE FALSE FALSE
TRUE FALSE FALSE FALSE FALSE FALSE
TRUE TRUE TRUE FALSE FALSE FALSE
%% Cell type:markdown id: tags:
Widerspruchsbeweise werden wir oft im Verlauf der Vorlesung verwenden.
Es gibt zwei andere Arten von Beweisen: Äquivalenzbeweise und Deduktionsbeweise.
# Äquivalenzbeweis
Hier schreiben wir die Schritte des Beweises oft in folgender Form auf:
* $\phi_1$
* $\Longleftrightarrow$ $\phi_2$
* ...
* $\Longleftrightarrow$ $\phi_k$
wobei immer gilt $\phi_i \equiv \phi_{i+1}$.
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$.
Wir haben sowohl $\phi_1 \models \phi_k$ als auch $\phi_k \models \phi_1$.
%% Cell type:markdown id: tags:
Als kleines Beispiel beweisen wir, dass $\neg b \Rightarrow a \equiv a \vee b$:
* $\neg b \Rightarrow a$
* $\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$ $a \vee b$ (Kommutativität von $\vee$)
Anmerkung: im Skript verwenden wir $\Longleftrightarrow$ für Äquivalenzbeweise; die "präzise" logische Schreibweise wäre $\equiv$.
%% Cell type:markdown id: tags:
# Deduktiver Beweis
Hier schreiben wir die Schritte des Beweises oft in folgender Form auf:
* $\phi_1$
* $\phi_2$
* ...
* $\phi_k$
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$.
Aber im Gegensatz zum Äquivalenzbeweis gilt hier generell nicht $\phi_k \models \phi_1$!
Dieser Beweis kann nicht umgekehrt werden.
%% Cell type:markdown id: tags:
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''
* B sagt: ``1+1=3''
* $\phi_1$ = $A \Leftrightarrow B$ $\wedge$ $B \Leftrightarrow FALSE$
* $\neg B$ (nach der zweiten Aussage $B \Leftrightarrow FALSE$ muss B 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.
%% Cell type:markdown id: tags:
# Aristoteles: Anfänge der Logik
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?
(In die Aussagenlogik sind alle vier Aussagen unabhängig.)
1. Alle Menschen sind sterblich.
2. Einige Menschen sind sterblich.
3. Alle Menschen sind unsterblich.
4. Einige Menschen sind unsterblich.
%% Cell type:markdown id: tags:
# Prädikatenlogik
Im Vergleich zur Aussagenlogik mit den Wahrheitswerten und Aussagen, gibt es in der Prädikatenlogik:
* Objekte
* <b>Konstanten</b> und <b>Variablen</b> die Objekte darstellen,
* <b>Funktionen</b> die Objekte auf Objekte abbilden,
* <b>Prädikate</b> die Objekte oder Objekt-kombinationen auf einen Wahrheitswert abbilden,
* <b>Quantoren</b> mit denen man Variablen einführt und Aussagen über alle Objekte machen kann, oder die Existenz eines Objekts zusichert
%% Cell type:markdown id: tags:
Erläuterung:
* ```2+2 < 5``` ist eine Aussage
* ```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.
* ```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 <b>Prädikat</b>, 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
Weitere Beispiele:
* ```<``` ist ein <b>binäres Prädikat</b>, für jede Kombination an Werten können wir bestimmen ob das Prädikat wahr oder falsch ist:
%% Cell type:code id: tags:
``` prob
:table {x,y,res | x:1..2 & y:1..3 & res=bool(x<y)}
```
%% Output
|x|y|res|
|---|---|---|
|$1$|$1$|$\mathit{FALSE}$|
|$1$|$2$|$\mathit{TRUE}$|
|$1$|$3$|$\mathit{TRUE}$|
|$2$|$1$|$\mathit{FALSE}$|
|$2$|$2$|$\mathit{FALSE}$|
|$2$|$3$|$\mathit{TRUE}$|
x y res
1 1 FALSE
1 2 TRUE
1 3 TRUE
2 1 FALSE
2 2 FALSE
2 3 TRUE
%% Cell type:markdown id: tags:
# Freie Variablen
Die Formel ```x<5``` besteht formal gesehen aus:
* einer logischen Variable $x$,
* 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.)
Innerhalb von ```x<5``` ist $x$ eine freie Variable.
In einer <b>geschlossenen</b> Formel der Prädikatenlogik müssen alle Variablen durch Quantoren gebunden werden.
%% Cell type:markdown id: tags:
# Quantoren
In der Prädikatenlogik gibt es zwei Quantoren:
* den <b>Existenzquantor</b> $\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
* den <b>Allquantor</b> $\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
* $\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.
Mit der Standardinterpretation von $<$ und $5$ ist diese Formel falsch. Ein Gegenbeispiel ist $x=5$.
%% Cell type:code id: tags:
``` prob
∃x.(x<5)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 0$
TRUE
Solution:
x = 0
%% Cell type:markdown id: tags:
In diesem Jupyter Notebook werden automatisch Existenzquantoren für alle offenen Variablen eingefügt:
%% Cell type:code id: tags:
``` prob
x<5
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 0$
TRUE
Solution:
x = 0
%% Cell type:code id: tags:
``` prob
x+20 = 30
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 10$
TRUE
Solution:
x = 10
%% Cell type:code id: tags:
``` prob
x*x = 10000
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = -100$
TRUE
Solution:
x = −100
%% Cell type:markdown id: tags:
# Logische Äquivalenz, Schlussfolgerung
Diese beiden Definitionen übernehmen wir wortwörtlich aus der Aussagenlogik:
* Zwei Formeln $\phi$ und $\psi$ sind <b>äquivalent</b> gdw sie die selben Modelle haben.
* Wir schreiben dies als $\phi \equiv \psi$.
* Eine Formel $\psi$ ist eine <b>logische Schlussfolgerung</b> von $\phi$, wenn alle Modelle von $\phi$ auch Modelle von $\psi$ sind.
* Wir schreiben dies als $\phi \models \psi$.
%% Cell type:markdown id: tags:
Das Konzept der Modelle ist aber in Prädikatenlogik komplizierter:
* eine Menge an Objekten muss ausgewählt 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.
* (manchmal sind bestimmte Symbole vordefiniert, wie $<$, $+$ oder $5$)
Dies ist nicht Inhalt dieser Vorlesung.
%% Cell type:markdown id: tags:
# Quantoren: Einige Gesetze der Prädikatenlogik
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. (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$
Diese Gesetze erlauben es einem Quantoren zu vertauschen:
* $\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))$
* $\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))$
%% Cell type:markdown id: tags:
Aber Achtung:
* $\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)$
%% Cell type:markdown id: tags:
# Werkzeuge für Logik
* 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
* Beweiser: Atelier-B, Rodin, Isabelle, Coq, Vampire,...
* Model-Finder, Constraint Solver: ProB, Alloy, IDP, ...
* Programmiersprache: Prolog
Einige Anwendungen dieser Werkzeuge:
* Hardware Verifikation
* schwere Probleme lösen (Eclipse/Linux Abhängigkeiten,...)
* https://wiki.eclipse.org/Equinox_P2_Resolution
* Software Verifikation, Fehler finden (NullPointer Exception, Overflows), Windows Driver Verification (SLAM2,...)
* 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/
* Stellwerkprüfung (Prover Technologies, ...)
* Datenvalidierung (ProB bei Siemens, Alstom, Thales; Paris L1)
* Software Entwicklung (AtelierB, Paris L14, L1, ....: seit 1999 kein einziger Bug !)
%% Cell type:markdown id: tags:
# Andere Logiken
* Aussagenlogik und Prädikatenlogik sind klassische zweiwertige Logiken
* sie sind <b>monoton</b> wenn $\phi \models \psi$ dann gilt für alle $\rho$: $\phi \wedge \rho \models \psi$
* Aussagenlogik ist entscheidbar
* 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
* (Anmerkung: Wir werden später in der Vorlesung das Konzept der Entscheidbarkeit formal beschreiben)
* reine Prädikatenlogik ist nicht ausreichend um Arithmetik zu axiomatisieren
* Gödelscher Unvollständigkeitssatz https://de.wikipedia.org/wiki/Gödelscher_Unvollständigkeitssatz
Nicht-klassische Logiken:
* es gibt Intuitionistische Logik: Beweis durch Widerspruch dort nicht erlaubt
* es gibt dreiwertige Logiken ( $2/0=1 \wedge 1=2$ )
* es gibt die Fuzzy Logik, modale Logiken, temporale Logiken,...
* nicht-monotone Logiken
%% Cell type:markdown id: tags:
# Zusammenfassung Logik
* Formeln der Aussagenlogik und Prädikatenlogik
* Interpretation, Modell, Äquivalenz ($\equiv$), logisches Schließen ($\models$)
* Deduktiver Beweis, Äquivalenzbeweis
* Beweis durch Widerspruch
* Äquivalenzen (Kommutativität, de Morgan, ...)
* Ziel: logische Formeln verstehen und erstellen können
* Nächste Vorlesung: Grundlagen der Mengentheorie
%% Cell type:markdown id: tags:
# Anhang mit Erläuterungen
## Unterschied zwischen $\equiv$ und $\Leftrightarrow$
* $\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
* $\equiv$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen
* Mit $\equiv$ trifft man mathematische Aussagen über zwei Formeln.
Es gilt aber folgendes Theorem:
Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik.
Dann gilt:
* $\phi \equiv \psi$ gdw die Formel $\phi \Leftrightarrow \psi$ eine Tautologie ist.
%% 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:
%% Cell type:code id: tags:
``` prob
:table {p,q,ODER,IMPL,EQUIV| p:BOOL & q:BOOL &
ODER=bool(p=TRUE ∨ ¬(q=TRUE)) & // 𝑝∨¬𝑞
IMPL = bool(q=TRUE ⇒ p=TRUE) & // 𝑞⇒p
EQUIV=bool((ODER=TRUE) ⇔ (IMPL=TRUE))}
```
%% Output
|p|q|ODER|IMPL|EQUIV|
|---|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
p q ODER IMPL EQUIV
FALSE FALSE TRUE TRUE TRUE
FALSE TRUE FALSE FALSE TRUE
TRUE FALSE TRUE TRUE TRUE
TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags:
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)$!
%% Cell type:code id: tags:
``` prob
:table {p,q,ODER,UND,EQUIV| p:BOOL & q:BOOL &
ODER=bool(p=TRUE ∨ q=TRUE) & // 𝑝∨𝑞
UND = bool(p=TRUE & q=TRUE) & // p&q
EQUIV=bool((ODER=TRUE) ⇔ (UND=TRUE))}
```
%% Output
|p|q|ODER|UND|EQUIV|
|---|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
p q ODER UND EQUIV
FALSE FALSE FALSE FALSE TRUE
FALSE TRUE TRUE FALSE FALSE
TRUE FALSE TRUE FALSE FALSE
TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags:
## Unterschied zwischen $\models$ und $\Rightarrow$
Das Gleiche gilt für diese beiden Symbole:
* $\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
* $\models$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen
* Mit $\models$ trifft man mathematische Aussagen über zwei Formeln.
Es gilt aber folgendes Theorem:
Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik.
Dann gilt:
* $\phi \models \psi$ gdw die Formel $\phi \Rightarrow \psi$ eine Tautologie ist.
%% Cell type:code id: tags:
``` prob
```
......
info4/kapitel-0/Mengentheorie.ipynb
View file @ bea76b55
%% Cell type:markdown id: tags:
# Theoretische Informatik - Vorlesung 0 - Teil 2 Mengentheorie
* April 2020
* Michael Leuschel
* Lehrstuhl Softwaretechnik und Programmiersprachen
* Heinrich-Heine Universität Düsseldorf
Grundlagen der Logik und Mengentheorie sind nicht im Skript.
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.
Auswertung der Formeln erfolgt mit dem [Jupyter Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) für [ProB](https://www3.hhu.de/stups/prob)
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.
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/master?filepath=info4%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:
# Mengen
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))
* _"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:
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.
Fundamental sind diese beiden Symbole:
* wenn $a$ ein Objekt ist und $x$ eine Menge, dann
* 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.
$\in$ und $\not\in$ sind Prädikate, verbunden durch die Eigenschaft:
* $\forall(a,x).(a\not\in x \Leftrightarrow \neg(a \in x))$
%% Cell type:markdown id: tags:
## Die leere Menge und Gleichheit
Eine besondere Menge ist die leere Menge $\emptyset$.
Sie hat keine Elemente:
* $z = \emptyset \Leftrightarrow \forall(a).(a\not\in z)$
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))$
%% Cell type:code id: tags:
``` prob
∅ = {1}
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
{1} = {1,2}
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
{1,2} = {2,1}
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
# Notationen für Mengen: endliche Enumeration
* explizite Auflistung aller Elemente $\{a_1,\ldots,a_n\}$
* die Reihenfolge spielt keine Rolle:
%% Cell type:code id: tags:
``` prob
{2,5,3} = {2,3,5}
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Dies ist im Unterschied zu Tupeln und Listen oder Folgen, die oft mit runden und eckigen Klammern geschriben werden:
%% Cell type:code id: tags:
``` prob
(TRUE,5,3) = (TRUE,3,5) // Vergleich von zwei Tripeln
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
[2,5,3] = [2,3,5] // Vergleich von zwei Folgen/Listen
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
* Elemente können in der Enumeration mehrfach auftauchen:
%% Cell type:code id: tags:
``` prob
{2,5,3,2,5} = {2,3,5}
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
# Vereinigung, Schnitt, Differenz
Drei wichtige Operationen auf Mengen sind wie folgt.
Vereinigung von Mengen $\cup$ :
* $z = x\cup y \Leftrightarrow \forall(a).(a\in z \Leftrightarrow (a\in x \vee a \in y))$
Schnitt von Mengen $\cap$:
* $z = x\cap y \Leftrightarrow \forall(a).(a\in z \Leftrightarrow (a\in x \wedge a \in y))$
Differenz von Mengen $\setminus$:
* $z = x \setminus y \Leftrightarrow \forall(a).(a\in z \Leftrightarrow (a\in x \wedge a \not\in y))$
%% Cell type:code id: tags:
``` prob
{2,3,5} ∪ {5,7}
```
%% Output
$\{2,3,5,7\}$
{2,3,5,7}
%% Cell type:code id: tags:
``` prob
{2,3,5}∩{5,7}
```
%% Output
$\{5\}$
{5}
%% Cell type:code id: tags:
``` prob
{2,3,5}−{5,7}
```
%% Output
$\{2,3\}$
{2,3}
%% Cell type:markdown id: tags:
# Notationen für Mengen: per Prädikat
Man kann die Elemente einer Menge auch durch ein Prädikat beschreiben:$\{a \mid P(a)\}$.
Es gilt:
* $z = \{a \mid P(a)\} \Leftrightarrow \forall(a).(a\in z \Leftrightarrow P(a))$
%% Cell type:code id: tags:
``` prob
{a | a>1 & a<6 & a≠4}
```
%% Output
$\{2,3,5\}$
{2,3,5}
%% Cell type:markdown id: tags:
Man kann mit dieser Schreibweise auch unendliche Mengen darstellen:
%% Cell type:code id: tags:
``` prob
{a | a>10}
```
%% Output
$\{\mathit{a}\mid \mathit{a} > 10\}$
{a∣a > 10}
%% Cell type:code id: tags:
``` prob
{a | a mod 2 = 0} ∩ {2,3,5}
```
%% Output
$\{2\}$
{2}
%% Cell type:markdown id: tags:
Man kann mit dieser Schreibweise auch die drei Mengenoperationen definieren:
* $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 \setminus y = \{a \mid a\in x \wedge a\not\in y\}$
%% Cell type:code id: tags:
``` prob
x = {2,3} & y = {2,5} & xy = {a| a∈x ∨ a∈y}
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xy} = \{2,3,5\}$
* $\mathit{x} = \{2,3\}$
* $\mathit{y} = \{2,5\}$
TRUE
Solution:
xy = {2,3,5}
x = {2,3}
y = {2,5}
%% Cell type:code id: tags:
``` prob
x = {2,3} & y = {2,5} & xy = {a| a∈x ∧ a∈y}
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xy} = \{2\}$
* $\mathit{x} = \{2,3\}$
* $\mathit{y} = \{2,5\}$
TRUE
Solution:
xy = {2}
x = {2,3}
y = {2,5}
%% Cell type:code id: tags:
``` prob
x = {2,3} & y = {2,5} & xy = {a| a∈x ∧ a∉y}
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{xy} = \{3\}$
* $\mathit{x} = \{2,3\}$
* $\mathit{y} = \{2,5\}$
TRUE
Solution:
xy = {3}
x = {2,3}
y = {2,5}
%% Cell type:markdown id: tags:
Als Kürzel führen wir auch die Notation $a..b$ für $\{x \mid x \geq a \wedge x \leq b\}$ ein.
%% Cell type:code id: tags:
``` prob
1..10
```
%% Output
$\{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:
# Ein Theorem (Distributivgesetz 1)
Für alle Mengen $x$, $y$, $z$ gilt:
* $x \cup (y \cap z) = (x\cup y) \cap (x\cup z)$
<img src="./img/Venn.svg" width="300">
%% Cell type:code id: tags:
``` prob
{2,3,55}∪({2,44,77}∩{2,44,66})
```
%% Output
$\{2,3,44,55\}$
{2,3,44,55}
%% Cell type:code id: tags:
``` prob
({2,3,55}∪{2,44,77})∩({2,3,55}∪{2,44,66})
```
%% Output
$\{2,3,44,55\}$
{2,3,44,55}
%% Cell type:markdown id: tags:
## Beweis von $x \cup (y \cap z) = (x\cup y) \cap (x\cup z)$
Für den Beweis benötigen wir diese Lemmata:
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\}$
3. $a \in \{b \mid P(b)\} \equiv P(a)$
4. $\phi \vee (\psi \wedge \rho) \equiv (\phi \vee \psi) \wedge (\phi \vee \rho)$
Hier ist ein Äquivalenzbeweis (siehe vorherige Vorlesung):
1. $m=x \cup (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\} \}$
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) \}$
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) \}$
8. (Lemma 2, $\Leftarrow$) $m=(x\cup y) \cap (x\cup z)$
%% Cell type:markdown id: tags:
# Gesetze für $\cap$, $\cup$ und $\setminus$
Für alle Mengen $x$, $y$, $z$ gilt:
* $x \cup y = y \cup x$ (Kommutativ 1)
* $x \cap y = y \cap x$ (Kommutativ 2)
* $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 \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)
* $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)
* $x \cup \emptyset = x$ (Leere Menge 1)
* $x \cap \emptyset = \emptyset$ (Leere Menge 2)
* $x \cap (z \setminus x) = \emptyset$ (Leere Menge 3)
%% Cell type:code id: tags:
``` prob
(1..10) \ ({2,4,6,8} ∪ {5,10}) // De Morgan 1 - linke Seite
```
%% Output
$\{1,3,7,9\}$
{1,3,7,9}
%% Cell type:code id: tags:
``` prob
(1..10) \ {2,4,6,8}
```
%% Output
$\{1,3,5,7,9,10\}$
{1,3,5,7,9,10}
%% Cell type:code id: tags:
``` prob
(1..10) \ {5,10}
```
%% Output
$\{1,2,3,4,6,7,8,9\}$
{1,2,3,4,6,7,8,9}
%% Cell type:code id: tags:
``` prob
((1..10) \ {2,4,6,8}) ∩ ((1..10) \ {5,10}) // De Morgan 1 - rechte Seite
```
%% Output
$\{1,3,7,9\}$
{1,3,7,9}
%% Cell type:markdown id: tags:
Gesetze von De Morgan haben wir auch schon in der Aussagenlogik gesehen.
Auch hier haben diese die Form wo ein Ausdruck
* $Op1( x ~ Op2 ~ y)$
umgewandelt wird in einen Ausdruck
* $Op1(x) ~ Op2' ~ Op1(y)$
wo Op2' der duale Operator von Op2 ist.
%% Cell type:markdown id: tags:
Hier ein Beispiel für das letzte Gesetz:
%% Cell type:code id: tags:
``` prob
{2,4} ∩ (ℤ \ {2,4})
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
∅
%% Cell type:markdown id: tags:
# Teilmenge
Eine Menge $x$ ist eine Teilmenge oder Untermenge von $y$ wenn gilt:
* $\forall a. a\in x \Rightarrow a \in y$
Wir benutzen diese Schreibweise $x \subseteq y$.
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:
* $x \subset y$ $\Leftrightarrow$ $(x \subseteq y \wedge x\neq y)$.
%% Cell type:code id: tags:
``` prob
x={1,3} ∧ y = 1..5 ∧ ∀a.(a∈x ⇒ a∈y)
```
%% Output
$\newcommand{\upto}{\mathbin{.\mkern1mu.}}\mathit{TRUE}$
**Solution:**
* $\mathit{x} = \{1,3\}$
* $\mathit{y} = (1 \upto 5)$
TRUE
Solution:
x = {1,3}
y = (1 ‥ 5)
%% Cell type:code id: tags:
``` prob
x={1,3} ∧ y = 1..5 ∧ ∀a.(a∈y ⇒ a∈x)
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
{1,3} ⊂ 1..5
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
# Kardinalität
Die Anzahl der Elemente einer Menge $x$ schreiben wir als
* $\mid x\mid$ oder auch als $card(x)$ (B Schreibweise).
%% Cell type:code id: tags:
``` prob
card({1,2,3})
```
%% Output
$3$
3
%% Cell type:code id: tags:
``` prob
card({1,1,2,3,2})
```
%% Output
$3$
3
%% Cell type:code id: tags:
``` prob
card(∅)
```
%% Output
$0$
0
%% 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: $\mid \{x \mid x>0\} \mid$
%% Cell type:code id: tags:
``` prob
card({x|x>0})
```
%% Output
: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(...))]))
%% Cell type:markdown id: tags:
# SEND+MORE=MONEY
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:
| | | | | |
|---|---|---|---|---|
| | S | E | N | D |
| + | M | O | R | E |
|
|= M| O | N | E | Y |
| | | | | |
Wir können dies nun in Logik, Mengentheorie und Arithmetik modellieren und lösen.
%% Cell type:markdown id: tags:
Wir haben acht Ziffern:
%% Cell type:code id: tags:
``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 0$
* $\mathit{S} = 0$
* $\mathit{D} = 0$
* $\mathit{E} = 0$
* $\mathit{Y} = 0$
* $\mathit{M} = 0$
* $\mathit{N} = 0$
* $\mathit{O} = 0$
TRUE
Solution:
R = 0
S = 0
D = 0
E = 0
Y = 0
M = 0
N = 0
O = 0
%% Cell type:markdown id: tags:
diese Ziffern sind alle unterschiedlich:
%% Cell type:code id: tags:
``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9 ∧
card({S,E,N,D,M,O,R,Y}) = 8
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 2$
* $\mathit{S} = 0$
* $\mathit{D} = 5$
* $\mathit{E} = 7$
* $\mathit{Y} = 1$
* $\mathit{M} = 4$
* $\mathit{N} = 6$
* $\mathit{O} = 3$
TRUE
Solution:
R = 2
S = 0
D = 5
E = 7
Y = 1
M = 4
N = 6
O = 3
%% Cell type:markdown id: tags:
und wobei die zwei führenden Ziffern S und M ungleich 0 sind:
%% Cell type:code id: tags:
``` 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
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 3$
* $\mathit{S} = 2$
* $\mathit{D} = 5$
* $\mathit{E} = 7$
* $\mathit{Y} = 0$
* $\mathit{M} = 1$
* $\mathit{N} = 6$
* $\mathit{O} = 4$
TRUE
Solution:
R = 3
S = 2
D = 5
E = 7
Y = 0
M = 1
N = 6
O = 4
%% Cell type:markdown id: tags:
und wo die Summe von SEND+MORE MONEY ergibt:
%% Cell type:code id: tags:
``` 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*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 8$
* $\mathit{S} = 9$
* $\mathit{D} = 7$
* $\mathit{E} = 5$
* $\mathit{Y} = 2$
* $\mathit{M} = 1$
* $\mathit{N} = 6$
* $\mathit{O} = 0$
TRUE
Solution:
R = 8
S = 9
D = 7
E = 5
Y = 2
M = 1
N = 6
O = 0
%% Cell type:markdown id: tags:
Aber ist dies die einzige Lösung ? Wir können einfach die Menge aller Lösungen berechnen:
%% Cell type:code id: tags:
``` prob
{S,E,N,D, M,O,R, Y |
{S,E,N,D, M,O,R, Y} ⊆ 0..9 ∧ S >0 ∧ M >0 ∧
card({S,E,N,D, M,O,R, Y}) = 8 ∧
S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y }
```
%% Output
$\{(9\mapsto 5\mapsto 6\mapsto 7\mapsto 1\mapsto 0\mapsto 8\mapsto 2)\}$
{(9↦5↦6↦7↦1↦0↦8↦2)}
%% Cell type:code id: tags:
``` prob
:table {S,E,N,D, M,O,R, Y |
{S,E,N,D, M,O,R, Y} ⊆ 0..9 ∧ S >0 ∧ M >0 ∧
card({S,E,N,D, M,O,R, Y}) = 8 ∧
S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y }
```
%% Output
|S|E|N|D|M|O|R|Y|
|---|---|---|---|---|---|---|---|
|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|
S E N D M O R Y
9 5 6 7 1 0 8 2
%% Cell type:markdown id: tags:
| | | | | |
|---|---|---|---|---|
| | S=9 | E=5 | N=6 | D=7 |
| + | M=1 | O=0 | R=8 | E=5 |
|
|= M=1| O=0 | N=6 | E=5 | Y=2 |
| | | | | |
%% Cell type:markdown id: tags:
Ein anderes arithmetisches Puzzle ist KISS*KISS=PASSION.
%% Cell type:code id: tags:
``` prob
:table {K, I, S, P, A, O, N |
{K,P} ⊆ 1..9 ∧
{I,S,A,O,N} ⊆ 0..9 ∧
(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 &
card({K, I, S, P, A, O, N}) = 7}
```
%% Output
|K|I|S|P|A|O|N|
|---|---|---|---|---|---|---|
|$2$|$0$|$3$|$4$|$1$|$8$|$9$|
K I S P A O N
2 0 3 4 1 8 9
%% Cell type:markdown id: tags:
# Mengen von Mengen
Mengen können selber auch Mengen beinhalten
Dies sind alles unterschiedliche Mengen:
* $\{\{2\},\{3,4\}\}$
* $\{\{2,3\},\{4\}\}$
* $\{\{2,3\},\{3,4\}\}$
* $\{\{2,3,4\}\}$
* $\{2,3,4\}$
Wir haben zum Beispiel:
* $\mathit{card}(\{\{2,3,4\}\}) = 1$
* $\mathit{card}(\{\{2\},\{3,4\}\}) = 2$
* $\mathit{card}(\{2,3,4\}) = 3$
* $\{2\} \in \{\{2\},\{3,4\}\} $
* $\{2\} \not\in \{\{2,3\},\{4\}\} $
%% Cell type:code id: tags:
``` prob
card({2,3,4})
```
%% Output
$3$
3
%% Cell type:code id: tags:
``` prob
card({{2,3,4}})
```
%% Output
$1$
1
%% Cell type:code id: tags:
``` prob
card({{2},{3,4}})
```
%% Output
$2$
2
%% Cell type:code id: tags:
``` prob
{2} ∈ {{2}, {3,4}}
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
{2} ∈ {{2,3}, {4}}
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
## Mengen von Mengen und die leere Menge
Achtung: man muss die leere Menge von der Menge die die leere Menge beinhaltet unterscheiden:
* $\emptyset \neq \{\emptyset\}$
%% Cell type:code id: tags:
``` prob
∅ = {∅}
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
card(∅)
```
%% Output
$0$
0
%% Cell type:code id: tags:
``` prob
card({∅})
```
%% Output
$1$
1
%% Cell type:code id: tags:
``` prob
∅ ∈ {∅}
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
∅ ∈ ∅
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
∅ ∉ ∅
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
# Potenzmenge
Die Menge aller Untermengen einer Menge $A$ schreiben wir als $ℙ(\mathit{A}) $ oder auch als $2^{A}$.
%% Cell type:code id: tags:
``` prob
ℙ({1,2})
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{2\}\}$
{∅,{1},{1,2},{2}}
%% Cell type:code id: tags:
``` prob
ℙ(∅)
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset\}$
{∅}
%% Cell type:code id: tags:
``` prob
ℙ(1..3)
```
%% Output
$\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}}
%% Cell type:code id: tags:
``` prob
:table ℙ(1..3)
```
%% Output
|Elements|
|---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|
|$\{1\}$|
|$\{1,2\}$|
|$\{1,3\}$|
|$\{2\}$|
|$\{1,2,3\}$|
|$\{2,3\}$|
|$\{3\}$|
Elements
{}
{1}
{1,2}
{1,3}
{2}
{1,2,3}
{2,3}
{3}
%% Cell type:code id: tags:
``` prob
:table ℙ(ℙ({1}))
```
%% Output
|Elements|
|---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|
|$\{\emptyset\}$|
|$\{\emptyset,\{1\}\}$|
|$\{\{1\}\}$|
Elements
{}
{{}}
{{},{1}}
{{1}}
%% Cell type:code id: tags:
``` prob
card(ℙ(1..3))
```
%% Output
$8$
8
%% Cell type:code id: tags:
``` prob
card(ℙ(1..10))
```
%% Output
$1024$
1024
%% Cell type:code id: tags:
``` prob
card(ℙ(1..100))
```
%% Output
$1267650600228229401496703205376$
1267650600228229401496703205376
%% Cell type:code id: tags:
``` prob
card(ℙ(ℙ(1..7)))
```
%% Output
$340282366920938463463374607431768211456$
340282366920938463463374607431768211456
%% Cell type:code id: tags:
``` prob
card(ℙ(ℙ(ℙ(1..3))))
```
%% Output
$115792089237316195423570985008687907853269984665640564039457584007913129639936$
115792089237316195423570985008687907853269984665640564039457584007913129639936
%% Cell type:markdown id: tags:
# Relationen in der Mengentheorie
* Was ist eine Relation?
* Wie kann man Relationen in Mengentheorie und Logik abbilden?
* 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._
* k-Tupel: $(1,2)$ (k=2, Paar)
* Eine Relation weist k-Tupeln Wahrheitswerte zu:
* Beispiel: $(1,2) \mapsto TRUE$, $(2,1) \mapsto FALSE$.
## Unäre Relationen
Eine unäre Relation über $x$ entspricht einfach einer Untermenge von $x$:
* die Menge an Werten für die die Relation wahr ist.
Beispiele:
* Relation ``Ziffer'' über die ganzen Zahlen ist
* $0 .. 9 \subseteq$ ℤ
* Relation ``Gt0'' über die ganzen Zahlen ist
* $\{ \mathit{x}|\mathit{x} \in $ℤ $\wedge \mathit{x} > 0\} \subseteq$ ℤ.
* Relation ``Gerade'' über die ganzen Zahlen ist
* $\{ \mathit{x}|\mathit{x} \in $ ℤ $\wedge \mathit{x} \mod 2 = 0\} \subseteq$ ℤ.
%% Cell type:markdown id: tags:
## Relationen vs Prädikate
Eine Relation ist die explizite Darstellung eines Prädikats als Menge:
* Prädikate können mit logischen Junktoren und Quantoren verarbeitet werden:
* $\exists x. is\_rich(x)$, $\forall x.(is\_poor(x) \Rightarrow \neg is\_rich(x))$
* Relationen können mit mengentheoretischen Operationen verarbeitet werden:
* $rich \neq \emptyset$, $rich \cap poor = \emptyset$.
%% Cell type:markdown id: tags:
# Kartesisches Produkt und Paare
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)$ steht hier für ein geordnetes Paar,
d.h. $(1 \mapsto 2) \neq (2 \mapsto 1) $.
Wir schreiben manchmal auch $a \mapsto b$ anstatt $(a,b)$.
%% Cell type:code id: tags:
``` prob
(1 .. 2) × (4 .. 5)
```
%% Output
$\{(1\mapsto 4),(1\mapsto 5),(2\mapsto 4),(2\mapsto 5)\}$
{(1↦4),(1↦5),(2↦4),(2↦5)}
%% Cell type:code id: tags:
``` prob
(1 .. 2) × {4}
```
%% Output
$\{(1\mapsto 4),(2\mapsto 4)\}$
{(1↦4),(2↦4)}
%% Cell type:code id: tags:
``` prob
(1 .. 2) × BOOL
```
%% Output
$\{(1\mapsto \mathit{FALSE}),(1\mapsto \mathit{TRUE}),(2\mapsto \mathit{FALSE}),(2\mapsto \mathit{TRUE})\}$
{(1↦FALSE),(1↦TRUE),(2↦FALSE),(2↦TRUE)}
%% Cell type:code id: tags:
``` prob
(1 .. 3) × (1 .. 3)
```
%% 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↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3)}
%% Cell type:code id: tags:
``` prob
card((1..10)×(1..10))
```
%% Output
$100$
100
%% Cell type:markdown id: tags:
Das Kartesische Produkt ist nicht kommutativ:
%% Cell type:code id: tags:
``` prob
{2}×{3}
```
%% Output
$\{(2\mapsto 3)\}$
{(2↦3)}
%% Cell type:code id: tags:
``` prob
{3}×{2}
```
%% Output
$\{(3\mapsto 2)\}$
{(3↦2)}
%% Cell type:markdown id: tags:
Es gilt:
* $A \times B = \emptyset \equiv (A = \emptyset \vee B=\emptyset)$.
Das Kartesische Produkt wird auch Kreuzmenge oder Produktmenge genannt.
%% Cell type:markdown id: tags:
# 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.
Beispiel: die Relation ``kleiner'' über die Ziffern $0..9$:
%% Cell type:code id: tags:
``` prob
{a,b| (a,b)∈(0..9)×(0..9) ∧ a<b}
```
%% 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↦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:
Diese Relation ist eine Untermenge von ℤ×ℤ.
Ein anderes Beispiel ist die Relation ``halb'' über die ganzen Zahlen $1..10$:
%% Cell type:code id: tags:
``` prob
{a,b| a∈1..10 ∧ b∈1..10 ∧ b*2=a}
```
%% Output
$\{(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)}
%% Cell type:markdown id: tags:
Eine binäre Relation kann auch als gerichteter Graph angesehen werden:
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("halb",{a,b| a∈1..10 ∧ b∈1..10 & b*2=a})
```
%% Output
<Dot visualization: expr_as_graph [("halb",{a,b|a:1..10 & b:1..10 & b*2=a})]>
%% Cell type:markdown id: tags:
Die Typen der Elemente kann abweichen.
Zum Beispiel die Relation ``durch drei teilbar'' über die ganzen Zahlen $1..7$ zum Datentypen $STRING$
%% Cell type:code id: tags:
``` prob
{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")}
```
%% 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↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("teilbar",{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")})
```
%% Output
<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:
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:
``` prob
:pref DOT_ENGINE=circo
```
%% Output
Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("K5",(1..5)×(1..5))
```
%% Output
<Dot visualization: expr_as_graph [("K5",(1..5)*(1..5))]>
%% Cell type:code id: tags:
``` prob
:pref DOT_ENGINE=circo
```
%% Output
Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("K10",(1..10)×(1..10))
```
%% Output
<Dot visualization: expr_as_graph [("K10",(1..10)*(1..10))]>
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("K20",(1..20)×(1..20))
```
%% Output
<Dot visualization: expr_as_graph [("K20",(1..20)*(1..20))]>
%% Cell type:code id: tags:
``` prob
:pref DOT_ENGINE=dot
```
%% Output
Preference changed: DOT_ENGINE = dot
%% Cell type:markdown id: tags:
# Definitions- und Wertebereich
Definitionsbereich (Domain in Englisch):
* $dom(r) = \{a \mid \exists b.((a,b)\in r)\}$
Wertebereich (Bildmenge, Range in Englisch):
* $ran(r) = \{b \mid \exists a.((a,b)\in r)\}$
%% Cell type:code id: tags:
``` prob
:let h {a,b| a∈1..10 ∧ b∈1..10 & b*2=a}
```
%% Output
$\{(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)}
%% Cell type:code id: tags:
``` prob
{a| ∃b.((a,b)∈h)}
```
%% Output
$\{2,4,6,8,10\}$
{2,4,6,8,10}
%% Cell type:code id: tags:
``` prob
{b| ∃a.((a,b)∈h)}
```
%% Output
$\{1,2,3,4,5\}$
{1,2,3,4,5}
%% Cell type:code id: tags:
``` prob
dom(h)
```
%% Output
$\{2,4,6,8,10\}$
{2,4,6,8,10}
%% Cell type:code id: tags:
``` prob
:let h {a,b| a∈1..10 ∧ b∈1..10 & b*2=a}
```
%% Output
$\{(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)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("h",h)
```
%% Output
<Dot visualization: expr_as_graph [hh={(2,1),(4,2),(6,3),(8,4),(10,5)}("h",h)]>
%% Cell type:code id: tags:
``` prob
:let d {x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")}
```
%% 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↦"nein"),(2↦"nein"),(3↦"ja"),(4↦"nein"),(5↦"nein"),(6↦"ja"),(7↦"nein")}
%% Cell type:code id: tags:
``` prob
dom(d)
```
%% Output
$\{1,2,3,4,5,6,7\}$
{1,2,3,4,5,6,7}
%% Cell type:code id: tags:
``` prob
ran(d)
```
%% Output
$\{\text{"ja"},\text{"nein"}\}$
{"ja","nein"}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("d",d)
```
%% Output
<Dot visualization: expr_as_graph [dhd={(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)}("d",d)]>
%% Cell type:markdown id: tags:
# Relationales Abbild und Umkehrrelation
Abbild:
* $r[A] = \{b \mid \exists a.((a,b)\in r \wedge a\in A)\}$
Umkehrrelation:
* $r^{-1} = \{(b,a) \mid (a,b)\in r \}$
Im Notebook muss für die Umkehrrelation leider Tilde (~) verwendet werden:
%% Cell type:code id: tags:
``` prob
h[8..10]
```
%% Output
$\{4,5\}$
{4,5}
%% Cell type:code id: tags:
``` prob
d[{3,6}]
```
%% Output
$\{\text{"ja"}\}$
{"ja"}
%% Cell type:code id: tags:
``` prob
d[{0}]
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
∅
%% Cell type:code id: tags:
``` prob
d~
```
%% 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)\}$
{("ja"↦3),("ja"↦6),("nein"↦1),("nein"↦2),("nein"↦4),("nein"↦5),("nein"↦7)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("d~",d~)
```
%% Output
<Dot visualization: expr_as_graph [dhd={(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)}("d~",d~)]>
%% Cell type:markdown id: tags:
Man kann natürlich auch beide Operatoren verknüpfen, zum Beispiel um herauszufinden welche Zahlen durch 3 teilbar sind:
%% Cell type:code id: tags:
``` prob
d~[{"ja"}]
```
%% Output
$\{3,6\}$
{3,6}
%% Cell type:code id: tags:
``` prob
:unlet d
```
%% Cell type:markdown id: tags:
# Binäre Relationen - Verknüpfung
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)\}$.
%% Cell type:code id: tags:
``` prob
({1↦2, 2↦3} ; {2↦4, 2↦8})
```
%% Output
$\{(1\mapsto 4),(1\mapsto 8)\}$
{(1↦4),(1↦8)}
%% Cell type:markdown id: tags:
Man kann eine Relation auch mit sich selber verknüpfen wenn Werte- und Definitionsbereich kompatibel sind.
Zum Beispiel $h^2 = (h;h)$:
%% Cell type:code id: tags:
``` prob
(h ; h)
```
%% Output
$\{(4\mapsto 1),(8\mapsto 2)\}$
{(4↦1),(8↦2)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("h",h,"hh",(h;h))
```
%% Output
<Dot visualization: expr_as_graph [hh={(2,1),(4,2),(6,3),(8,4),(10,5)}("h",h)]>
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("hh",(h;h))
```
%% Output
<Dot visualization: expr_as_graph [hh={(2,1),(4,2),(6,3),(8,4),(10,5)}("hh",(h;h))]>
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("h",(h))
```
%% Output
<Dot visualization: expr_as_graph [hh={(2,1),(4,2),(6,3),(8,4),(10,5)}("h",h)]>
%% Cell type:markdown id: tags:
# Transitive Hülle
Gegeben eine Relation $r$ von $A$ nach $A$
* $r^1 = r$
* $r^k = (r^{k-1} ; r) = (r ; r^{k-1})$
* $r^+$ = $\bigcup_{i\geq 1} r^i$
%% Cell type:code id: tags:
``` prob
(h;h)
```
%% Output
$\{(4\mapsto 1),(8\mapsto 2)\}$
{(4↦1),(8↦2)}
%% Cell type:code id: tags:
``` prob
(h;h;h)
```
%% Output
$\{(8\mapsto 1)\}$
{(8↦1)}
%% Cell type:code id: tags:
``` prob
(h;h;h;h)
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
∅
%% Cell type:markdown id: tags:
Die transitive Hülle wird in B als ```closure1``` geschrieben:
%% Cell type:code id: tags:
``` prob
closure1(h)
```
%% 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↦1),(4↦1),(4↦2),(6↦3),(8↦1),(8↦2),(8↦4),(10↦5)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("h+",closure1(h))
```
%% Output
<Dot visualization: expr_as_graph [hh={(2,1),(4,2),(6,3),(8,4),(10,5)}("h+",closure1(h))]>
%% Cell type:code id: tags:
``` prob
:unlet h
```
%% Cell type:markdown id: tags:
Ein weiteres Beispiel ist folgende abgeänderte strikte Untermengenrelation $\subset$ für $ℙ(1 .. 3) $:
%% Cell type:code id: tags:
``` prob
:let sub1 {x,y|y:ℙ(1..3) & x ⊂ y & card(x)+1=card(y)}
```
%% 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\})\}$
{(∅↦{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:
``` prob
:pref DOT_DECOMPOSE_NODES=false
```
%% Output
Preference changed: DOT_DECOMPOSE_NODES = false
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("sub1",sub1)
```
%% Output
<Dot visualization: expr_as_graph [sub1sub1={({},{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})}("sub1",sub1)]>
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("sub1",closure1(sub1))
```
%% Output
<Dot visualization: expr_as_graph [sub1sub1={({},{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})}("sub1",closure1(sub1))]>
%% Cell type:markdown id: tags:
# Transitive und Reflexive Hülle
Gegeben eine Relation $r$ von $A$ nach $A$
* $r^0 = \{(a,a) \mid a\in A\}$
* $r^1 = r$
* $r^k = (r^{k-1} ; r) = (r ; r^{k-1})$
* $r^*$ = $\bigcup_{i\geq 0} r^i$
%% Cell type:code id: tags:
``` prob
:let A {1,2,3}
```
%% Output
$\{1,2,3\}$
{1,2,3}
%% Cell type:code id: tags:
``` prob
:let r {(1,2), (2,3)}
```
%% Output
$\{(1\mapsto 2),(2\mapsto 3)\}$
{(1↦2),(2↦3)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("r",r)
```
%% Output
<Dot visualization: expr_as_graph [Arsub1A={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})}("r",r)]>
%% Cell type:code id: tags:
``` prob
(r;r)
```
%% Output
$\{(1\mapsto 3)\}$
{(1↦3)}
%% Cell type:markdown id: tags:
In B kann man $r^0$ auch als die Identitätsrelation über A beschreiben:
%% Cell type:code id: tags:
``` prob
id(A)
```
%% Output
$\{(1\mapsto 1),(2\mapsto 2),(3\mapsto 3)\}$
{(1↦1),(2↦2),(3↦3)}
%% Cell type:markdown id: tags:
Die transitive und reflexive Hülle ist hier:
%% Cell type:code id: tags:
``` prob
id(A) \/ r \/ (r;r) \/ (r;r;r) \/ (r;r;r;r)
```
%% Output
$\{(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)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("r*",id(A) \/ r \/ (r;r) \/ (r;r;r) \/ (r;r;r;r))
```
%% Output
<Dot visualization: expr_as_graph [Arsub1A={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})}("r*",id(A)\/r\/(r;r)\/((r;r);r)\/(((r;r);r);r))]>
%% Cell type:markdown id: tags:
Als Vergleich dazu sieht die transitive Hülle so aus:
%% Cell type:code id: tags:
``` prob
closure1(r)
```
%% Output
$\{(1\mapsto 2),(1\mapsto 3),(2\mapsto 3)\}$
{(1↦2),(1↦3),(2↦3)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("r+",closure1(r))
```
%% Output
<Dot visualization: expr_as_graph [Arsub1A={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})}("r+",closure1(r))]>
%% 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:
%% Cell type:code id: tags:
``` prob
closure1(r)~[{3}]
```
%% Output
$\{1,2\}$
{1,2}
%% 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.
%% Cell type:code id: tags:
``` prob
closure(r)
```
%% Output
$/*@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__}
%% Cell type:code id: tags:
``` prob
closure(r)~[{3}]
```
%% Output
$\{1,2,3\}$
{1,2,3}
%% Cell type:code id: tags:
``` prob
:unlet r
```
%% Cell type:markdown id: tags:
# Funktionen
Was unterscheidet Funktionen von Relationen?
Wie kann man Funktionen in Mengentheorie und Logik darstellen?
Eine Funktion kann als Menge an Paaren angesehen werden.
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.
Eingeschränkt auf den Bereich 1..10 sieht dies Funktion so aus:
%% Cell type:code id: tags:
``` prob
{x,y|x:1..10 & y=x+1}
```
%% 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↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)}
%% 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:
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("sub1",sub1)
```
%% Output
<Dot visualization: expr_as_graph [Asub1A={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})}("sub1",sub1)]>
%% 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:
%% Cell type:code id: tags:
``` prob
sub1
```
%% 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\})\}$
{(∅↦{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:
Eine (totale) Funktion $F$ von $A$ nach $B$ ist
* 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,b,c).(((a,b)\in F \wedge (a,c)\in F) \Rightarrow b=c)$
Wir schreiben dann $F \in A \rightarrow B$.
%% Cell type:code id: tags:
``` prob
∀(a,b,c).((a,b)∈sub1 & (a,c)∈sub1 ⇒ b=c)
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
sub1 ∈ ℙ(1..3) --> ℙ(1..3)
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
:unlet sub1
```
%% Cell type:code id: tags:
``` prob
:let i10 {x,y|x:1..10 & y=x+1}
```
%% 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↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)}
%% Cell type:code id: tags:
``` prob
∀(a,b,c).((a,b)∈i10 & (a,c)∈i10 ⇒ b=c)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{A} = \{1,2,3\}$
* $\mathit{i10} = \{(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)\}$
TRUE
Solution:
A = {1,2,3}
i10 = {(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:
``` prob
i10 ∈ 1..10 --> 2..11
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{A} = \{1,2,3\}$
* $\mathit{i10} = \{(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)\}$
TRUE
Solution:
A = {1,2,3}
i10 = {(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:
Anmerkung: es wird nicht geprüft ob der komplette Wertebereich abgedeckt wird:
%% Cell type:code id: tags:
``` prob
i10 ∈ 1..10 --> 0..100
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{A} = \{1,2,3\}$
* $\mathit{i10} = \{(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)\}$
TRUE
Solution:
A = {1,2,3}
i10 = {(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:
Es wird aber wohl geprüft ob der Definitionsbereich komplett abgedeckt wird:
%% Cell type:code id: tags:
``` prob
i10 ∈ 2..10 --> 0..100
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
i10 ∈ 0..10 --> 0..100
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
dom(i10)
```
%% Output
$\{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:
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:
``` prob
(4,z) ∈ i10
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{A} = \{1,2,3\}$
* $\mathit{i10} = \{(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)\}$
* $\mathit{z} = 5$
TRUE
Solution:
A = {1,2,3}
i10 = {(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)}
z = 5
%% Cell type:code id: tags:
``` prob
dom(i10)
```
%% Output
$\{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:
``` prob
ran(i10)
```
%% Output
$\{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:
``` prob
i10[{4,5}]
```
%% Output
$\{5,6\}$
{5,6}
%% Cell type:code id: tags:
``` prob
i10[{4}]
```
%% Output
$\{5\}$
{5}
%% Cell type:code id: tags:
``` prob
i10~[{4}]
```
%% Output
$\{3\}$
{3}
%% Cell type:code id: tags:
``` prob
(i10 ; i10)[{4}]
```
%% Output
$\{6\}$
{6}
%% Cell type:code id: tags:
``` prob
closure1(i10)[{4}]
```
%% Output
$\{5,6,7,8,9,10,11\}$
{5,6,7,8,9,10,11}
%% Cell type:code id: tags:
``` prob
closure1(i10~)[{4}]
```
%% Output
$\{1,2,3\}$
{1,2,3}
%% 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)```.
%% Cell type:code id: tags:
``` prob
i10(4)
```
%% Output
$5$
5
%% Cell type:code id: tags:
``` prob
i10(4) + i10(4)
```
%% Output
$10$
10
%% 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.
%% Cell type:code id: tags:
``` prob
i10[{100}]
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
∅
%% Cell type:code id: tags:
``` prob
i10
```
%% 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↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10),(10↦11)}
%% Cell type:code id: tags:
``` prob
i10(100)
```
%% Output
:eval: NOT-WELL-DEFINED:
function applied outside of domain (#7): Function argument: 100, function value: {}
### Line: 2, Column: 0 until 8
%% Cell type:markdown id: tags:
Alle möglichen Funktionen über einen Definitionsbereich ergeben wieder eine Menge:
%% Cell type:code id: tags:
``` prob
1..2 --> 1..2
```
%% 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↦1),(2↦1)},{(1↦1),(2↦2)},{(1↦2),(2↦1)},{(1↦2),(2↦2)}}
%% Cell type:markdown id: tags:
Es gibt auch noch andere Arten an Funktionen:
* partielle Funktionen, +->
* injektive (umkehrbare) Funktionen >->
* surjektive Funktionen die den Wertebereich komplett abdecken -->>
* injektive und surjektive Funktionen >->>, auch Bijektionen gennant
(Die Pfeilsymbole sind sehr spezifisch für die B Sprache. Wir werden diese nicht im Skript verwenden.)
%% Cell type:code id: tags:
``` prob
1..2 +-> 1..2
```
%% 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)\}\}$
{∅,{(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:
``` prob
(1..2 --> 1..2) <: (1..2 +-> 1..2)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{A} = \{1,2,3\}$
* $\mathit{i10} = \{(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)\}$
TRUE
Solution:
A = {1,2,3}
i10 = {(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:
Folgende fünf Funktionen sind partiell und nicht total:
%% Cell type:code id: tags:
``` prob
(1..2 +-> 1..2) \ (1..2 --> 1..2)
```
%% Output
$\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)}}
%% Cell type:markdown id: tags:
Das sind die totalen umkehrbaren Funktionen:
%% Cell type:code id: tags:
``` prob
1..2 >-> 1..2
```
%% Output
$\{\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\}\}$
{{(1↦1),(2↦2)},{(1↦2),(2↦1)}}
%% Cell type:markdown id: tags:
In diesem Falle sind diese identisch zu den surjektiven Funktionen und den Bijektionen:
%% Cell type:code id: tags:
``` prob
1..2 -->> 1..2
```
%% Output
$\{\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\}\}$
{{(1↦1),(2↦2)},{(1↦2),(2↦1)}}
%% Cell type:code id: tags:
``` prob
1..2 >->> 1..2
```
%% Output
$\{\{(1\mapsto 1),(2\mapsto 2)\},\{(1\mapsto 2),(2\mapsto 1)\}\}$
{{(1↦1),(2↦2)},{(1↦2),(2↦1)}}
%% Cell type:code id: tags:
``` prob
:unlet i10
```
%% Cell type:markdown id: tags:
# 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.
(Anmerkung: Im Skript werden wir eine andere Schreibweise verwenden. Zum Beispiel, $ab$ ist die
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.)
Was unterscheidet Folgen von Mengen?
Wie kann man Folgen in Mengentheorie und Logik darstellen?
## Endliche Folgen vs Mengen
Die Reihenfolge der Elemente ist wichtig:
* $[1,2] \neq [2,1] $, während
* $\{1,2\} = \{2,1\} $
Elemente können mehrfach auftauchen:
* $[1,1] \neq [1] $, während
* $\{1,1\} = \{1\} $
Wie kann man Folgen in Mengentheorie und Logik darstellen?
%% Cell type:markdown id: tags:
## Endliche Folgen mathematisch gesehen
Eine (endliche) Folge $G$ von $A$ Elementen der Länge $n$ ist
* eine (totale) Funktion von $1..n$ nach $A$.
Da eine totale Funktion eine Menge an Paare ist, haben wir zum Beispiel:
%% Cell type:code id: tags:
``` prob
:let G [22,22,33]
```
%% Output
$\{(1\mapsto 22),(2\mapsto 22),(3\mapsto 33)\}$
{(1↦22),(2↦22),(3↦33)}
%% Cell type:code id: tags:
``` prob
G
```
%% Output
$\{(1\mapsto 22),(2\mapsto 22),(3\mapsto 33)\}$
{(1↦22),(2↦22),(3↦33)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("G",G)
```
%% Output
<Dot visualization: expr_as_graph [AGA={1,2,3} & G={(1,22),(2,22),(3,33)}("G",G)]>
%% Cell type:markdown id: tags:
Es gilt also
* $G = [22,22,33] = \{(1\mapsto 22),(2\mapsto 22),(3\mapsto 33)\}$
Wir schreiben $\mathit{G} \in \mathit{seq}$(ℤ)
oder aber auch $G \in ℤ^*$ (mehr dazu später im Skript)
Das n-te Element einer Folge $G$ ist einfach $G(n)$:
%% Cell type:code id: tags:
``` prob
G(2)
```
%% Output
$22$
22
%% Cell type:markdown id: tags:
Die Länge einer Folge (```size``` in B) ist einfach die Kardinalität der unterliegenden Relation:
%% Cell type:code id: tags:
``` prob
size(G)
```
%% Output
$3$
3
%% Cell type:code id: tags:
``` prob
card(G)
```
%% Output
$3$
3
%% Cell type:markdown id: tags:
Wir können alle anderen Menge und Relationsoperatoren auf Folgen anwenden:
%% Cell type:code id: tags:
``` prob
dom(G)
```
%% Output
$\{1,2,3\}$
{1,2,3}
%% Cell type:code id: tags:
``` prob
ran(G)
```
%% Output
$\{22,33\}$
{22,33}
%% Cell type:code id: tags:
``` prob
G~[{22}]
```
%% Output
$\{1,2\}$
{1,2}
%% Cell type:code id: tags:
``` prob
:unlet G
```
%% Cell type:markdown id: tags:
# Zusammenfassung Mengentheorie
* Mengen, Notationen (per Prädikat)
* Potenzmenge, Menge von Mengen, $\phi \neq \{ \phi\}$
* kartesisches Produkt, Relationen als Menge von Paaren/Tupeln
* Definitionsbereich, Wertebereich, Abbild, Umkehrrelation
* Transitive Hülle
* Funktionen
* Endliche Folgen als Funktion von $ℤ$ nach Wertebereich
%% Cell type:markdown id: tags:
# Lernziele von Kapitel 0
* logische Formeln verstehen und schreiben können
* logische Beweise verstehen: Wahrheitstabelle, Widerspruch, Deduktiver Beweis, Äuivalenzbeweis
* Mengenausdrücke verstehen und nach Logik übbersetzen können
* Problemstellungen nach Logik und Mengentheorie übersetzen können
* Relationen, Funktionen und Folgen in Mengendarstellung bearbeiten können
%% Cell type:code id: tags:
``` prob
```
......