# 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](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):
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)$.
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:
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)
* 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:
* 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 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](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):
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)$.
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:
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)
* 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:
* 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.
# 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):
* _"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$.
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:
> 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.
* $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$:
: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:
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.
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:
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.
* 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
...
...
%% 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):
* _"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$.
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:
> 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.
* $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$:
: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:
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.
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:
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.