# Theoretische Informatik - Vorlesung 0 - Teil 1 Logik
* April 2023
* April 2020
* Michael Leuschel
* Lehrstuhl Softwaretechnik und Programmiersprachen
* Heinrich-Heine Universität Düsseldorf
Grundlagen der Logik und Mengentheorie sind nicht im Skript.
Hier definieren wir einige Grundlagen und Notationen, die im Skript verwendet werden.
Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich.
Die Folien für diese Grundlagen sind als Jupyter Notebooks erstellt worden und im [GitLab der Informatik](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) erhältlich.
%% Cell type:markdown id: tags:
## Was ist ein Notebook?
* Dokument mit Text und ausführbaren Code-Abschnitten
* Code kann interaktiv ausgeführt werden
* Ergebnisse erscheinen im Notebook unter dem jeweiligem Code
* Ähnlich wie eine REPL (read-eval-print-loop), mit einigen Unterschieden:
* Ausgaben können formatierten Text und Grafiken enthalten
* Speicherbar als Datei
* Code kann später neu ausgeführt werden
* Weitergabe an andere Nutzer möglich
* Implementierungen: Mathematica, Maple, Jupyter, u. a.
%% Cell type:markdown id: tags:
## Jupyter Notebook
* Browserbasierte Notebook-Oberfläche
* Open Source und plattformübergreifend
* Stammt aus der Python-Community, in Python implementiert
* ACM System Software Award 2017
* Jupyter-Notebooks verschiedene Programmiersprachen verwenden
* Ein sprachspezifischer **Kernel** stellt die Sprache dem Jupyter Frontend zur Verfügung
%% Cell type:markdown id: tags:
## [ProB](https://prob.hhu.de/w/) Kernel

*[ProB](https://prob.hhu.de/w/) ist ein Werkzeug zur Animation, Verifikation und Visualisierung formaler Spezifikationen
* Unterstützt B-Spezifikationen für sicherheitskritsche Anwendungen
* Entwicklung am STUPS Lehrstuhl
* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.
* Eignet sich aber auch für mathematische Ausführungen
* Der [ProB-Jupyter-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) stellt die B-Sprache und die mathematischen Grundlagen für Jupyter Notebooks zur Verfügung
Um diese Notebooks zu starten kann man entweder selber Jupyter und den [ProB-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren.
Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger):
Damit Jupyter formattierte Ausgabe für Formeln und Tabellen zulässt muss rechts oben in der Menuleiste auf "Not Trusted" drücken. Wenn das Notebook als "Trusted" markiert ist wird JavaScript aktiviert und die Ausgabe wird besser ausgegeben.
%% Cell type:markdown id: tags:
# Was ist Logik?
Quelle [Wikipedia](https://de.wikipedia.org/wiki/Logik):
* vernünftiges Schlussfolgern, Denklehre
* In der Logik wird die Struktur von Argumenten im Hinblick auf ihre Gültigkeit untersucht, unabhängig vom Inhalt der Aussagen
* Traditionell ist die Logik ein Teil der Philosophie.
* Seit dem 20. Jahrhundert versteht man unter Logik überwiegend symbolische Logik, die auch als grundlegende Strukturwissenschaft, z. B. innerhalb der Mathematik und der theoretischen Informatik, behandelt wird.
%% Cell type:markdown id: tags:
# Warum Logik studieren?
* Hardware: logische Schaltkreise
* Wissensdarstellung und intelligentes Denken: Künstliche Intelligenz, deklarative Darstellung von Wissen, semantisches Web, ...
* Überlegungen über Programme: Verifikation, statische Programmanalyse, Programmoptimierung,...
* Universale Vorrichtung zur Berechnung: Datenbanken, logische Programmierung, ...
* Grundlage der Mathematik und auch der theoretischen Informatik
* Halpern et al. On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.cmu.edu/~rwh/papers/unreasonable/basl.pdf
* Zitat aus diesem Artikel:
> The effectiveness of logic in computer science is not by any means limited to the areas mentioned in here. As a matter of fact, it spans a wide spectrum of areas, from artificial intelligence to software engineering. Overall, logic provides computer science with both a unifying foundational framework and a powerful tool for modeling and reasoning about aspects of computation.
%% Cell type:markdown id: tags:
# Welche Logik studieren?
* Aussagenlogik
* Prädikatenlogik der ersten Stufe (FOL - First Order Logic)
* Logik höherer Stufe (HOL - Higher Order Logic)
* eine temporale Logik
* eine mehrwertige Logik oder gar Fuzzy Logik
* Relevanzlogik, lineare Logik
* eine nichtmonotone Logik
Wir werden die klassische, zweiwertige, monotone **Aussagenlogik**
und **Prädikatenlogik** studieren (zusammen mit Mengentheorie).
%% Cell type:markdown id: tags:
# Aussagenlogik
Eine Aussage ist endweder wahr ($\mathit{TRUE}$) oder falsch ($\mathit{FALSE}$).
Hier sind vier Aussagen:
1. Siegfried ist ein Ritter
2. Alle Ritter sagen die Wahrheit
3. Siegfried sagt "Ich habe den Drachen getötet"
4. Siegfried hat den Drachen getötet.
Die Logik interessiert sich weniger ob Aussagen wahr oder falsch sind, sondern mehr um Zusammenhänge zwischen möglichen Wahrheitswerten verschiedener Aussagen und Formeln.
Zum Beispiel, wenn wir die Aussagen 1,2 und 3 als wahr annehmen, dann müssen wir auch die Aussage 4 als wahr annehmen.
Einige Aussagen haben manchmal vordefinierte Wahrheitswerte.
Wir zum Beispiel benutzen Arithmetik und Mengetheorie in unseren logischen Formeln, ohne diese selber in Logik zu formalisieren.
Hier sind ein paar Aussagen in Arithmetik:
%% Cell type:code id: tags:
``` prob
2>1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
1+1 = 2
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2<1
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
# Junktoren und Formeln
Jede Aussage ist auch eine Formel der Aussagenlogik.
Mit den Junktoren kann man Aussagen und Formeln zu grösseren Formeln der Aussagenlogik kombinieren.
Die Negation `¬(F)` einer Formel F ist auch eine Formel. Die negierte Formel ist wahr genau dann wenn (gdw) die ursprünglihe Formel falsch ist:
%% Cell type:code id: tags:
``` prob
¬(2<1)
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
¬(1+1=2)
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
In diesen Notebooks muss der Inhalt der Negation immer geklammert werden. Im Skript ist das nicht immer nötig.
%% Cell type:markdown id: tags:
Die Konjunktion `F ∧ G` von zwei Formeln ist wahr gdw beide Formeln wahr sind:
%% Cell type:code id: tags:
``` prob
2>1 ∧ 1>0
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2>1 ∧ 1>2
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
Die Disjunktion `F ∨ G` von zwei Formeln ist wahr gdw mindestes eine der beiden Formeln wahr sind:
%% Cell type:code id: tags:
``` prob
1>1 ∨ 1>2
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
2>1 ∨ 3>1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Die Implikation `F ⇒ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder die erste Formel F falsch ist:
%% Cell type:code id: tags:
``` prob
2>1 ⇒ 3>1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2<1 ⇒ 1+1 = 5
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2>1 ⇒ 1+1=5
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
Die Äquivalenz `F ⇔ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder beide Formeln falsch sind:
%% Cell type:code id: tags:
``` prob
1=2 ⇔ 2=1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
1=3 ⇔ 1=1024
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
1=1 ⇔ 2=3
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
## Prioritäten
Anmerkung: Wir nehmen an, dass $\neg$ am stärksten bindet, dann kommen $\wedge$, $\vee$, $\Rightarrow$ und schließlich ⇔.
Die Formel $(p \vee (\neg p \wedge q))$ steht also für $(p \vee (\neg(p) \wedge q)$.
Wir schreiben diesen Tatbestand als $(p \vee (\neg p \wedge q)) \equiv p \vee q$.
Kleine Anmerkung: das Werkzeug im Jupyter Notebook akzeptiert keine aussagenlogische Variablen sondern nur Bool'sche Datenvariablen. Anstatt $p$ muss man `p=TRUE` schreiben und anstatt $p \vee q$ muss man `p=TRUE ∨ q=TRUE` schreiben. Mit `bool(P)` konvertiert man den Wahrheitswert einer Formel in einen Bool'schen Datenwert um.
$\equiv$ ist eine Relation zwischen logischen Formeln.
$\equiv$ ist transitiv und kommutativ.
%% Cell type:markdown id: tags:
# Wichtige Äquivalenzen
Für alle Formeln $\phi, \psi$ der Aussagenlogik gilt:
Achtung $\phi \wedge \neg \phi \models \psi$ für beliebiges $\psi$!
Also:
* $1>2 \models 1+1=100$
%% Cell type:markdown id: tags:
# Smullyan - Einfaches Puzzle
Raymond Smullyan beschreibt in seinen Büchern eine Insel auf der es (nur) zwei Arten von Personen gibt:
* Ritter, die immer die Wahrheit sagen, und
* Schurken, die immer lügen.
Hier ist ein Puzzle aus einem seiner Bücher:
* X sagt: "Y ist ein Ritter"
* Y sagt: "X und ich sind von einem unterschiedlichen Typ"
Können wir bestimmen ob X und Y Ritter oder Schurken sind?
%% Cell type:markdown id: tags:
## Lösen des Puzzles
Schritt 1: was sind die Aussagen?
* $X$: die Person X ist ein Ritter
* $Y$: die Person Y ist ein Ritter
Schritt 2: Übersetzung der Informationen in Aussagenlogik
* $\mathit{X} \Leftrightarrow \mathit{Y}$ ist die Übersetzung von:
* X sagt: "Y ist ein Ritter"
* $\mathit{Y} \Leftrightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von:
* Y sagt: "X und ich sind von einem unterschiedlichen Typ"
Schritt 3: Bestimmung der Modelle:
%% Cell type:code id: tags:
``` prob
:table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇔ y=TRUE) &
S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE)}
```
%% Output
|x|y|S1|S2|Puzzle|
|---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE|
|FALSE|TRUE|FALSE|TRUE|FALSE|
|TRUE|FALSE|FALSE|FALSE|FALSE|
|TRUE|TRUE|TRUE|FALSE|FALSE|
x y S1 S2 Puzzle
FALSE FALSE TRUE TRUE TRUE
FALSE TRUE FALSE TRUE FALSE
TRUE FALSE FALSE FALSE FALSE
TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags:
Unser Puzzle hat nur ein einziges Modell und beide Personen sind also Schurken.
Ein typische fehlerhafte Übersetzung des Puzzles ist diese:
* $\mathit{X} \Rightarrow \mathit{Y}$ ist die Übersetzung von:
* X sagt: "Y ist ein Ritter"
* $\mathit{Y} \Rightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von:
* Y sagt: "X und ich sind von einem unterschiedlichen Typ"
%% Cell type:code id: tags:
``` prob
:table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇒ y=TRUE) &
S2=bool(y=TRUE ⇒ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE)}
```
%% Output
|x|y|S1|S2|Puzzle|
|---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE|
|FALSE|TRUE|TRUE|TRUE|TRUE|
|TRUE|FALSE|FALSE|TRUE|FALSE|
|TRUE|TRUE|TRUE|FALSE|FALSE|
x y S1 S2 Puzzle
FALSE FALSE TRUE TRUE TRUE
FALSE TRUE TRUE TRUE TRUE
TRUE FALSE FALSE TRUE FALSE
TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags:
Diese Übersetzung erlaubt zwei Modelle, und auch eine fehlerhafte "Lösung" mit X als Schurken und Y als Ritter. Diese Lösung ist falsch, da X und Y die Wahrheit sagen, aber nur Y ein Ritter ist.
%% Cell type:markdown id: tags:
# Beweis durch Widerspruch
* Theorem: $\phi \models \psi$ genau dann wenn $\phi \wedge \neg \psi$ kein Modell hat
Beweis (ist ein Äquivalenzbeweis auf Metaebene):
* $\phi \models \psi$
* $\Longleftrightarrow$ alle Modelle von $\phi$ sind auch Modelle von $\psi$ (per Definition von $\models$)
* $\Longleftrightarrow$ in allen Modellen von $\phi$ hat $\neg \psi$ den Wahrheitswert falsch (per Definition von $\neg$)
* $\Longleftrightarrow$ alle Modelle von $\phi$ sind kein Modell von $\phi \wedge \neg \psi$ (per Definition von $\wedge$)
* $\Longleftrightarrow$ $\phi \wedge \neg \psi$ hat kein Modell (da auch kein Modell von $\neg \phi$ ein Modell von $\phi \wedge \neg \psi$ sein kann)
* dem binären Prädikatensymbol $<$, hier in Infix-Notation, mit zwei Argumenten: $x$ und $5$. (In Präfix-Notation würde man $<(x,5)$ schreiben.)
Innerhalb von `x<5` ist $x$ eine freie Variable.
In einer **geschlossenen** Formel der Prädikatenlogik müssen alle Variablen durch Quantoren gebunden werden.
%% Cell type:markdown id: tags:
# Quantoren
In der Prädikatenlogik gibt es zwei Quantoren:
* den **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
* 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
* $\exists x. x<5$ ist eine geschlossene Formel (aka eine Aussage). Mit der Standardinterpretation von $<$ und $5$ ist diese Formel wahr; eine Lösung ist $x=4$.
* $\forall x. x<5$ ist auch eine geschlossene Formel.
Mit der Standardinterpretation von $<$ und $5$ ist diese Formel falsch. Ein Gegenbeispiel ist $x=5$.
%% Cell type:code id: tags:
``` prob
∃x.(x<5)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 0$
TRUE
Solution:
x = 0
%% Cell type:markdown id: tags:
In diesem Jupyter Notebook werden automatisch Existenzquantoren für alle offenen Variablen eingefügt:
%% Cell type:code id: tags:
``` prob
x<5
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 0$
TRUE
Solution:
x = 0
%% Cell type:code id: tags:
``` prob
x+20 = 30
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 10$
TRUE
Solution:
x = 10
%% Cell type:code id: tags:
``` prob
x*x = 10000
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = -100$
TRUE
Solution:
x = −100
%% Cell type:markdown id: tags:
# Logische Äquivalenz, Schlussfolgerung
Diese beiden Definitionen übernehmen wir wortwörtlich aus der Aussagenlogik:
* Zwei Formeln $\phi$ und $\psi$ sind **äquivalent** gdw sie die selben Modelle haben.
* 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.
* Wir schreiben dies als $\phi \models \psi$.
%% Cell type:markdown id: tags:
Das Konzept der Modelle ist aber in Prädikatenlogik komplizierter:
* eine Menge an Objekten muss ausgewählt werden
* die Konstanten und Funktionen müssen den Objekten zugeordnet werden
* die Prädikate müssen Objekte auf Wahrheitswerte abbilden; Aussagen sind ein Spezialfall von Prädikaten.
* (manchmal sind bestimmte Symbole vordefiniert, wie $<$, $+$ oder $5$)
Dies ist nicht Inhalt dieser Vorlesung.
%% Cell type:markdown id: tags:
# Quantoren: Einige Gesetze der Prädikatenlogik
Mit diesen beiden Gesetzen kann man die Negation zu den atomaren Aussagen und Prädikaten verschieben:
* Ziel: logische Formeln verstehen und erstellen können
* Nächste Vorlesung: Grundlagen der Mengentheorie
%% Cell type:markdown id: tags:
# Anhang mit Erläuterungen
## Unterschied zwischen $\equiv$ und $\Leftrightarrow$
* $\Leftrightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen
* wenn $\phi$ und $\psi$ Formeln der Aussagenlogik sind, dann ist $\phi \Leftrightarrow \psi$ also auch eine Formel der Aussagenlogik
* $\equiv$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen
* Mit $\equiv$ trifft man mathematische Aussagen über zwei Formeln.
Es gilt aber folgendes Theorem:
Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik.
Dann gilt:
* $\phi \equiv \psi$ gdw die Formel $\phi \Leftrightarrow \psi$ eine Tautologie ist.
%% Cell type:markdown id: tags:
Zum Beispiel haben wir $p \vee \neg q \equiv q \Rightarrow p$ und in der Tat is die Formel $(p \vee \neg q) \Leftrightarrow (q \Rightarrow p)$ eine Tautologie:
%% Cell type:code id: tags:
``` prob
:table {p,q,ODER,IMPL,EQUIV| p:BOOL & q:BOOL &
ODER = bool(p=TRUE ∨ ¬(q=TRUE)) & // 𝑝∨¬𝑞
IMPL = bool(q=TRUE ⇒ p=TRUE) & // 𝑞⇒p
EQUIV = bool((ODER=TRUE) ⇔ (IMPL=TRUE))}
```
%% Output
|p|q|ODER|IMPL|EQUIV|
|---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE|
|FALSE|TRUE|FALSE|FALSE|TRUE|
|TRUE|FALSE|TRUE|TRUE|TRUE|
|TRUE|TRUE|TRUE|TRUE|TRUE|
p q ODER IMPL EQUIV
FALSE FALSE TRUE TRUE TRUE
FALSE TRUE FALSE FALSE TRUE
TRUE FALSE TRUE TRUE TRUE
TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags:
Die Formel $(p \vee q) \Leftrightarrow (p \wedge q)$ hingegen ist eine erfüllbare Formel, aber keine Tautologie.
Es gilt also $(p \vee q) \not\equiv (p \wedge q)$!
%% Cell type:code id: tags:
``` prob
:table {p,q,ODER,UND,EQUIV| p:BOOL & q:BOOL &
ODER = bool(p=TRUE ∨ q=TRUE) & // 𝑝∨𝑞
UND = bool(p=TRUE & q=TRUE) & // p&q
EQUIV = bool((ODER=TRUE) ⇔ (UND=TRUE))}
```
%% Output
|p|q|ODER|UND|EQUIV|
|---|---|---|---|---|
|FALSE|FALSE|FALSE|FALSE|TRUE|
|FALSE|TRUE|TRUE|FALSE|FALSE|
|TRUE|FALSE|TRUE|FALSE|FALSE|
|TRUE|TRUE|TRUE|TRUE|TRUE|
p q ODER UND EQUIV
FALSE FALSE FALSE FALSE TRUE
FALSE TRUE TRUE FALSE FALSE
TRUE FALSE TRUE FALSE FALSE
TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags:
## Unterschied zwischen $\models$ und $\Rightarrow$
Das Gleiche gilt für diese beiden Symbole:
* $\Rightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen
* wenn $\phi$ und $\psi$ Formeln der Aussagenlogik sind, dann ist $\phi \Rightarrow \psi$ also auch eine Formel der Aussagenlogik
* $\models$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen
* Mit $\models$ trifft man mathematische Aussagen über zwei Formeln.
Es gilt aber folgendes Theorem:
Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik.
Dann gilt:
* $\phi \models \psi$ gdw die Formel $\phi \Rightarrow \psi$ eine Tautologie ist.
...
...
%% Cell type:markdown id: tags:
# Theoretische Informatik - Vorlesung 0 - Teil 1 Logik
* April 2023
* April 2020
* Michael Leuschel
* Lehrstuhl Softwaretechnik und Programmiersprachen
* Heinrich-Heine Universität Düsseldorf
Grundlagen der Logik und Mengentheorie sind nicht im Skript.
Hier definieren wir einige Grundlagen und Notationen, die im Skript verwendet werden.
Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich.
Die Folien für diese Grundlagen sind als Jupyter Notebooks erstellt worden und im [GitLab der Informatik](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) erhältlich.
%% Cell type:markdown id: tags:
## Was ist ein Notebook?
* Dokument mit Text und ausführbaren Code-Abschnitten
* Code kann interaktiv ausgeführt werden
* Ergebnisse erscheinen im Notebook unter dem jeweiligem Code
* Ähnlich wie eine REPL (read-eval-print-loop), mit einigen Unterschieden:
* Ausgaben können formatierten Text und Grafiken enthalten
* Speicherbar als Datei
* Code kann später neu ausgeführt werden
* Weitergabe an andere Nutzer möglich
* Implementierungen: Mathematica, Maple, Jupyter, u. a.
%% Cell type:markdown id: tags:
## Jupyter Notebook
* Browserbasierte Notebook-Oberfläche
* Open Source und plattformübergreifend
* Stammt aus der Python-Community, in Python implementiert
* ACM System Software Award 2017
* Jupyter-Notebooks verschiedene Programmiersprachen verwenden
* Ein sprachspezifischer **Kernel** stellt die Sprache dem Jupyter Frontend zur Verfügung
%% Cell type:markdown id: tags:
## [ProB](https://prob.hhu.de/w/) Kernel

*[ProB](https://prob.hhu.de/w/) ist ein Werkzeug zur Animation, Verifikation und Visualisierung formaler Spezifikationen
* Unterstützt B-Spezifikationen für sicherheitskritsche Anwendungen
* Entwicklung am STUPS Lehrstuhl
* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.
* Eignet sich aber auch für mathematische Ausführungen
* Der [ProB-Jupyter-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) stellt die B-Sprache und die mathematischen Grundlagen für Jupyter Notebooks zur Verfügung
Um diese Notebooks zu starten kann man entweder selber Jupyter und den [ProB-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren.
Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger):
Damit Jupyter formattierte Ausgabe für Formeln und Tabellen zulässt muss rechts oben in der Menuleiste auf "Not Trusted" drücken. Wenn das Notebook als "Trusted" markiert ist wird JavaScript aktiviert und die Ausgabe wird besser ausgegeben.
%% Cell type:markdown id: tags:
# Was ist Logik?
Quelle [Wikipedia](https://de.wikipedia.org/wiki/Logik):
* vernünftiges Schlussfolgern, Denklehre
* In der Logik wird die Struktur von Argumenten im Hinblick auf ihre Gültigkeit untersucht, unabhängig vom Inhalt der Aussagen
* Traditionell ist die Logik ein Teil der Philosophie.
* Seit dem 20. Jahrhundert versteht man unter Logik überwiegend symbolische Logik, die auch als grundlegende Strukturwissenschaft, z. B. innerhalb der Mathematik und der theoretischen Informatik, behandelt wird.
%% Cell type:markdown id: tags:
# Warum Logik studieren?
* Hardware: logische Schaltkreise
* Wissensdarstellung und intelligentes Denken: Künstliche Intelligenz, deklarative Darstellung von Wissen, semantisches Web, ...
* Überlegungen über Programme: Verifikation, statische Programmanalyse, Programmoptimierung,...
* Universale Vorrichtung zur Berechnung: Datenbanken, logische Programmierung, ...
* Grundlage der Mathematik und auch der theoretischen Informatik
* Halpern et al. On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.cmu.edu/~rwh/papers/unreasonable/basl.pdf
* Zitat aus diesem Artikel:
> The effectiveness of logic in computer science is not by any means limited to the areas mentioned in here. As a matter of fact, it spans a wide spectrum of areas, from artificial intelligence to software engineering. Overall, logic provides computer science with both a unifying foundational framework and a powerful tool for modeling and reasoning about aspects of computation.
%% Cell type:markdown id: tags:
# Welche Logik studieren?
* Aussagenlogik
* Prädikatenlogik der ersten Stufe (FOL - First Order Logic)
* Logik höherer Stufe (HOL - Higher Order Logic)
* eine temporale Logik
* eine mehrwertige Logik oder gar Fuzzy Logik
* Relevanzlogik, lineare Logik
* eine nichtmonotone Logik
Wir werden die klassische, zweiwertige, monotone **Aussagenlogik**
und **Prädikatenlogik** studieren (zusammen mit Mengentheorie).
%% Cell type:markdown id: tags:
# Aussagenlogik
Eine Aussage ist endweder wahr ($\mathit{TRUE}$) oder falsch ($\mathit{FALSE}$).
Hier sind vier Aussagen:
1. Siegfried ist ein Ritter
2. Alle Ritter sagen die Wahrheit
3. Siegfried sagt "Ich habe den Drachen getötet"
4. Siegfried hat den Drachen getötet.
Die Logik interessiert sich weniger ob Aussagen wahr oder falsch sind, sondern mehr um Zusammenhänge zwischen möglichen Wahrheitswerten verschiedener Aussagen und Formeln.
Zum Beispiel, wenn wir die Aussagen 1,2 und 3 als wahr annehmen, dann müssen wir auch die Aussage 4 als wahr annehmen.
Einige Aussagen haben manchmal vordefinierte Wahrheitswerte.
Wir zum Beispiel benutzen Arithmetik und Mengetheorie in unseren logischen Formeln, ohne diese selber in Logik zu formalisieren.
Hier sind ein paar Aussagen in Arithmetik:
%% Cell type:code id: tags:
``` prob
2>1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
1+1 = 2
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2<1
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
# Junktoren und Formeln
Jede Aussage ist auch eine Formel der Aussagenlogik.
Mit den Junktoren kann man Aussagen und Formeln zu grösseren Formeln der Aussagenlogik kombinieren.
Die Negation `¬(F)` einer Formel F ist auch eine Formel. Die negierte Formel ist wahr genau dann wenn (gdw) die ursprünglihe Formel falsch ist:
%% Cell type:code id: tags:
``` prob
¬(2<1)
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
¬(1+1=2)
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
In diesen Notebooks muss der Inhalt der Negation immer geklammert werden. Im Skript ist das nicht immer nötig.
%% Cell type:markdown id: tags:
Die Konjunktion `F ∧ G` von zwei Formeln ist wahr gdw beide Formeln wahr sind:
%% Cell type:code id: tags:
``` prob
2>1 ∧ 1>0
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2>1 ∧ 1>2
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
Die Disjunktion `F ∨ G` von zwei Formeln ist wahr gdw mindestes eine der beiden Formeln wahr sind:
%% Cell type:code id: tags:
``` prob
1>1 ∨ 1>2
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
2>1 ∨ 3>1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Die Implikation `F ⇒ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder die erste Formel F falsch ist:
%% Cell type:code id: tags:
``` prob
2>1 ⇒ 3>1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2<1 ⇒ 1+1 = 5
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
2>1 ⇒ 1+1=5
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
Die Äquivalenz `F ⇔ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder beide Formeln falsch sind:
%% Cell type:code id: tags:
``` prob
1=2 ⇔ 2=1
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
1=3 ⇔ 1=1024
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
1=1 ⇔ 2=3
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
## Prioritäten
Anmerkung: Wir nehmen an, dass $\neg$ am stärksten bindet, dann kommen $\wedge$, $\vee$, $\Rightarrow$ und schließlich ⇔.
Die Formel $(p \vee (\neg p \wedge q))$ steht also für $(p \vee (\neg(p) \wedge q)$.
Wir schreiben diesen Tatbestand als $(p \vee (\neg p \wedge q)) \equiv p \vee q$.
Kleine Anmerkung: das Werkzeug im Jupyter Notebook akzeptiert keine aussagenlogische Variablen sondern nur Bool'sche Datenvariablen. Anstatt $p$ muss man `p=TRUE` schreiben und anstatt $p \vee q$ muss man `p=TRUE ∨ q=TRUE` schreiben. Mit `bool(P)` konvertiert man den Wahrheitswert einer Formel in einen Bool'schen Datenwert um.
$\equiv$ ist eine Relation zwischen logischen Formeln.
$\equiv$ ist transitiv und kommutativ.
%% Cell type:markdown id: tags:
# Wichtige Äquivalenzen
Für alle Formeln $\phi, \psi$ der Aussagenlogik gilt:
Achtung $\phi \wedge \neg \phi \models \psi$ für beliebiges $\psi$!
Also:
* $1>2 \models 1+1=100$
%% Cell type:markdown id: tags:
# Smullyan - Einfaches Puzzle
Raymond Smullyan beschreibt in seinen Büchern eine Insel auf der es (nur) zwei Arten von Personen gibt:
* Ritter, die immer die Wahrheit sagen, und
* Schurken, die immer lügen.
Hier ist ein Puzzle aus einem seiner Bücher:
* X sagt: "Y ist ein Ritter"
* Y sagt: "X und ich sind von einem unterschiedlichen Typ"
Können wir bestimmen ob X und Y Ritter oder Schurken sind?
%% Cell type:markdown id: tags:
## Lösen des Puzzles
Schritt 1: was sind die Aussagen?
* $X$: die Person X ist ein Ritter
* $Y$: die Person Y ist ein Ritter
Schritt 2: Übersetzung der Informationen in Aussagenlogik
* $\mathit{X} \Leftrightarrow \mathit{Y}$ ist die Übersetzung von:
* X sagt: "Y ist ein Ritter"
* $\mathit{Y} \Leftrightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von:
* Y sagt: "X und ich sind von einem unterschiedlichen Typ"
Schritt 3: Bestimmung der Modelle:
%% Cell type:code id: tags:
``` prob
:table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇔ y=TRUE) &
S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE)}
```
%% Output
|x|y|S1|S2|Puzzle|
|---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE|
|FALSE|TRUE|FALSE|TRUE|FALSE|
|TRUE|FALSE|FALSE|FALSE|FALSE|
|TRUE|TRUE|TRUE|FALSE|FALSE|
x y S1 S2 Puzzle
FALSE FALSE TRUE TRUE TRUE
FALSE TRUE FALSE TRUE FALSE
TRUE FALSE FALSE FALSE FALSE
TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags:
Unser Puzzle hat nur ein einziges Modell und beide Personen sind also Schurken.
Ein typische fehlerhafte Übersetzung des Puzzles ist diese:
* $\mathit{X} \Rightarrow \mathit{Y}$ ist die Übersetzung von:
* X sagt: "Y ist ein Ritter"
* $\mathit{Y} \Rightarrow (\mathit{X} \Leftrightarrow \neg (\mathit{Y}))$ ist die Übersetzung von:
* Y sagt: "X und ich sind von einem unterschiedlichen Typ"
%% Cell type:code id: tags:
``` prob
:table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
S1=bool(x=TRUE ⇒ y=TRUE) &
S2=bool(y=TRUE ⇒ (x=TRUE ⇔ ¬(y=TRUE))) &
Puzzle=bool(S1=TRUE & S2=TRUE)}
```
%% Output
|x|y|S1|S2|Puzzle|
|---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE|
|FALSE|TRUE|TRUE|TRUE|TRUE|
|TRUE|FALSE|FALSE|TRUE|FALSE|
|TRUE|TRUE|TRUE|FALSE|FALSE|
x y S1 S2 Puzzle
FALSE FALSE TRUE TRUE TRUE
FALSE TRUE TRUE TRUE TRUE
TRUE FALSE FALSE TRUE FALSE
TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags:
Diese Übersetzung erlaubt zwei Modelle, und auch eine fehlerhafte "Lösung" mit X als Schurken und Y als Ritter. Diese Lösung ist falsch, da X und Y die Wahrheit sagen, aber nur Y ein Ritter ist.
%% Cell type:markdown id: tags:
# Beweis durch Widerspruch
* Theorem: $\phi \models \psi$ genau dann wenn $\phi \wedge \neg \psi$ kein Modell hat
Beweis (ist ein Äquivalenzbeweis auf Metaebene):
* $\phi \models \psi$
* $\Longleftrightarrow$ alle Modelle von $\phi$ sind auch Modelle von $\psi$ (per Definition von $\models$)
* $\Longleftrightarrow$ in allen Modellen von $\phi$ hat $\neg \psi$ den Wahrheitswert falsch (per Definition von $\neg$)
* $\Longleftrightarrow$ alle Modelle von $\phi$ sind kein Modell von $\phi \wedge \neg \psi$ (per Definition von $\wedge$)
* $\Longleftrightarrow$ $\phi \wedge \neg \psi$ hat kein Modell (da auch kein Modell von $\neg \phi$ ein Modell von $\phi \wedge \neg \psi$ sein kann)
* dem binären Prädikatensymbol $<$, hier in Infix-Notation, mit zwei Argumenten: $x$ und $5$. (In Präfix-Notation würde man $<(x,5)$ schreiben.)
Innerhalb von `x<5` ist $x$ eine freie Variable.
In einer **geschlossenen** Formel der Prädikatenlogik müssen alle Variablen durch Quantoren gebunden werden.
%% Cell type:markdown id: tags:
# Quantoren
In der Prädikatenlogik gibt es zwei Quantoren:
* den **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
* 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
* $\exists x. x<5$ ist eine geschlossene Formel (aka eine Aussage). Mit der Standardinterpretation von $<$ und $5$ ist diese Formel wahr; eine Lösung ist $x=4$.
* $\forall x. x<5$ ist auch eine geschlossene Formel.
Mit der Standardinterpretation von $<$ und $5$ ist diese Formel falsch. Ein Gegenbeispiel ist $x=5$.
%% Cell type:code id: tags:
``` prob
∃x.(x<5)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 0$
TRUE
Solution:
x = 0
%% Cell type:markdown id: tags:
In diesem Jupyter Notebook werden automatisch Existenzquantoren für alle offenen Variablen eingefügt:
%% Cell type:code id: tags:
``` prob
x<5
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 0$
TRUE
Solution:
x = 0
%% Cell type:code id: tags:
``` prob
x+20 = 30
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 10$
TRUE
Solution:
x = 10
%% Cell type:code id: tags:
``` prob
x*x = 10000
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = -100$
TRUE
Solution:
x = −100
%% Cell type:markdown id: tags:
# Logische Äquivalenz, Schlussfolgerung
Diese beiden Definitionen übernehmen wir wortwörtlich aus der Aussagenlogik:
* Zwei Formeln $\phi$ und $\psi$ sind **äquivalent** gdw sie die selben Modelle haben.
* 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.
* Wir schreiben dies als $\phi \models \psi$.
%% Cell type:markdown id: tags:
Das Konzept der Modelle ist aber in Prädikatenlogik komplizierter:
* eine Menge an Objekten muss ausgewählt werden
* die Konstanten und Funktionen müssen den Objekten zugeordnet werden
* die Prädikate müssen Objekte auf Wahrheitswerte abbilden; Aussagen sind ein Spezialfall von Prädikaten.
* (manchmal sind bestimmte Symbole vordefiniert, wie $<$, $+$ oder $5$)
Dies ist nicht Inhalt dieser Vorlesung.
%% Cell type:markdown id: tags:
# Quantoren: Einige Gesetze der Prädikatenlogik
Mit diesen beiden Gesetzen kann man die Negation zu den atomaren Aussagen und Prädikaten verschieben:
* Ziel: logische Formeln verstehen und erstellen können
* Nächste Vorlesung: Grundlagen der Mengentheorie
%% Cell type:markdown id: tags:
# Anhang mit Erläuterungen
## Unterschied zwischen $\equiv$ und $\Leftrightarrow$
* $\Leftrightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen
* wenn $\phi$ und $\psi$ Formeln der Aussagenlogik sind, dann ist $\phi \Leftrightarrow \psi$ also auch eine Formel der Aussagenlogik
* $\equiv$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen
* Mit $\equiv$ trifft man mathematische Aussagen über zwei Formeln.
Es gilt aber folgendes Theorem:
Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik.
Dann gilt:
* $\phi \equiv \psi$ gdw die Formel $\phi \Leftrightarrow \psi$ eine Tautologie ist.
%% Cell type:markdown id: tags:
Zum Beispiel haben wir $p \vee \neg q \equiv q \Rightarrow p$ und in der Tat is die Formel $(p \vee \neg q) \Leftrightarrow (q \Rightarrow p)$ eine Tautologie:
%% Cell type:code id: tags:
``` prob
:table {p,q,ODER,IMPL,EQUIV| p:BOOL & q:BOOL &
ODER = bool(p=TRUE ∨ ¬(q=TRUE)) & // 𝑝∨¬𝑞
IMPL = bool(q=TRUE ⇒ p=TRUE) & // 𝑞⇒p
EQUIV = bool((ODER=TRUE) ⇔ (IMPL=TRUE))}
```
%% Output
|p|q|ODER|IMPL|EQUIV|
|---|---|---|---|---|
|FALSE|FALSE|TRUE|TRUE|TRUE|
|FALSE|TRUE|FALSE|FALSE|TRUE|
|TRUE|FALSE|TRUE|TRUE|TRUE|
|TRUE|TRUE|TRUE|TRUE|TRUE|
p q ODER IMPL EQUIV
FALSE FALSE TRUE TRUE TRUE
FALSE TRUE FALSE FALSE TRUE
TRUE FALSE TRUE TRUE TRUE
TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags:
Die Formel $(p \vee q) \Leftrightarrow (p \wedge q)$ hingegen ist eine erfüllbare Formel, aber keine Tautologie.
Es gilt also $(p \vee q) \not\equiv (p \wedge q)$!
%% Cell type:code id: tags:
``` prob
:table {p,q,ODER,UND,EQUIV| p:BOOL & q:BOOL &
ODER = bool(p=TRUE ∨ q=TRUE) & // 𝑝∨𝑞
UND = bool(p=TRUE & q=TRUE) & // p&q
EQUIV = bool((ODER=TRUE) ⇔ (UND=TRUE))}
```
%% Output
|p|q|ODER|UND|EQUIV|
|---|---|---|---|---|
|FALSE|FALSE|FALSE|FALSE|TRUE|
|FALSE|TRUE|TRUE|FALSE|FALSE|
|TRUE|FALSE|TRUE|FALSE|FALSE|
|TRUE|TRUE|TRUE|TRUE|TRUE|
p q ODER UND EQUIV
FALSE FALSE FALSE FALSE TRUE
FALSE TRUE TRUE FALSE FALSE
TRUE FALSE TRUE FALSE FALSE
TRUE TRUE TRUE TRUE TRUE
%% Cell type:markdown id: tags:
## Unterschied zwischen $\models$ und $\Rightarrow$
Das Gleiche gilt für diese beiden Symbole:
* $\Rightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen
* wenn $\phi$ und $\psi$ Formeln der Aussagenlogik sind, dann ist $\phi \Rightarrow \psi$ also auch eine Formel der Aussagenlogik
* $\models$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen
* Mit $\models$ trifft man mathematische Aussagen über zwei Formeln.
Es gilt aber folgendes Theorem:
Seien $\phi$ und $\psi$ beliebige Formeln der Aussagenlogik.
Dann gilt:
* $\phi \models \psi$ gdw die Formel $\phi \Rightarrow \psi$ eine Tautologie ist.
# Theoretische Informatik - Vorlesung 0 - Teil 2 Mengentheorie
* April 2023
* April 2020
* Michael Leuschel
* Lehrstuhl Softwaretechnik und Programmiersprachen
* Heinrich-Heine Universität Düsseldorf
Grundlagen der Logik und Mengentheorie sind nicht im Skript.
Hier definieren wir einige Grundlagen und Notationen die im Skript verwendet werden.
Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich.
Auswertung der Formeln erfolgt mit dem [Jupyter Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) für [ProB](https://prob.hhu.de/w/)
Um dieses Notebook zu starten kann man entweder selber Jupyter und den [ProB-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren.
Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger):
* _"Unter einer ‚Menge‘ verstehen wir jede Zusammenfassung M von bestimmten wohlunterschiedenen Objekten m unserer Anschauung oder unseres Denkens (welche die ‚Elemente‘ von M genannt werden) zu einem Ganzen."_ Georg Cantor (siehe [Textstelle als Bild in Wikipedia](https://de.wikipedia.org/wiki/Datei:Textstelle_mit_der_Mengendefinition_von_Georg_Cantor.png))
* _"The ability to regard any collection of objects as a single entity (i.e., as a set)."_ (Keith Devlin. Joy of Sets. Springer-Verlag.)
%% Cell type:markdown id: tags:
In der Regel gibt es eine Domäne an "Objekten" mit denen man Mengen bauen kann.
Was genau diese Objekte sind interessiert uns in der Mengentheorie nicht.
Fundamental sind diese beiden Symbole:
* wenn $a$ ein Objekt ist und $x$ eine Menge, dann
* ist $a \in x$ wahr, wenn $a$ ein Element von $x$ ist
* ist $a \not\in x$ wahr, wenn $a$ **kein** Element von $x$ ist.
$\in$ und $\not\in$ sind Prädikate, verbunden durch die Eigenschaft:
* $\forall(a,x).(a\not\in x \Leftrightarrow \neg(a \in x))$
%% Cell type:markdown id: tags:
## Die leere Menge und Gleichheit
Eine besondere Menge ist die leere Menge $\emptyset$.
Die Anzahl der Elemente einer Menge $x$ schreiben wir als
* $\mid x\mid$ oder auch als $card(x)$ (B Schreibweise).
%% Cell type:code id: tags:
``` prob
card({1,2,3})
```
%% Output
$3$
3
%% Cell type:code id: tags:
``` prob
card({1,1,2,3,2})
```
%% Output
$3$
3
%% Cell type:code id: tags:
``` prob
card(∅)
```
%% Output
$0$
0
%% Cell type:markdown id: tags:
Achtung, die Kardinalität kann auch unendlich sein: je nach Formalismus, ist folgender Ausdruck entweder unendlich oder nicht wohl definiert: $|\{x \mid x \in \mathbb{Z} \wedge x>0\}|$
%% Cell type:code id: tags:
``` prob
card({x|x∈ℤ ∧ x>0})
```
%% Output
:eval: NOT-WELL-DEFINED:
card applied to very large set, cardinality not representable in ProB: closure([x],[integer],b(greater(b(identifier(...),integer,[...]),b(value(...),integer,[...])),pred,[nodeid(pos(...)),prob_annotation('DO_NOT_ENUMERATE'(...)),removed_typing]))
%% Cell type:markdown id: tags:
# SEND+MORE=MONEY
Als Übung und Beispiel versuchen wir nun ein Problem zu lösen.
Es handelt sich um ein klassisches arithmetisches Puzzle wo acht unterschiedliche Ziffern gefunden werden sollen die folgende Gleichung erfüllen:
| | | | | |
|---|---|---|---|---|
| | S | E | N | D |
| + | M | O | R | E |
|
|= M| O | N | E | Y |
| | | | | |
Wir können dies nun in Logik, Mengentheorie und Arithmetik modellieren und lösen.
%% Cell type:markdown id: tags:
Wir haben acht Ziffern:
%% Cell type:code id: tags:
``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 0$
* $\mathit{S} = 0$
* $\mathit{D} = 0$
* $\mathit{E} = 0$
* $\mathit{Y} = 0$
* $\mathit{M} = 0$
* $\mathit{N} = 0$
* $\mathit{O} = 0$
TRUE
Solution:
R = 0
S = 0
D = 0
E = 0
Y = 0
M = 0
N = 0
O = 0
%% Cell type:markdown id: tags:
diese Ziffern sind alle unterschiedlich:
%% Cell type:code id: tags:
``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9 ∧
card({S,E,N,D,M,O,R,Y}) = 8
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 2$
* $\mathit{S} = 0$
* $\mathit{D} = 5$
* $\mathit{E} = 7$
* $\mathit{Y} = 1$
* $\mathit{M} = 4$
* $\mathit{N} = 6$
* $\mathit{O} = 3$
TRUE
Solution:
R = 2
S = 0
D = 5
E = 7
Y = 1
M = 4
N = 6
O = 3
%% Cell type:markdown id: tags:
und wobei die zwei führenden Ziffern S und M ungleich 0 sind:
> 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)$.
Das Kartesische Produkt wird auch Kreuzmenge oder Produktmenge genannt.
%% Cell type:markdown id: tags:
# Binäre Relationen
Eine binäre Relation über $x$ und $y$ ist eine Untermenge des kartesischen Produkts $x \times y$ zweier Mengen. Die Mengen $x$ und $y$ können identisch sein.
Beispiel: die Relation "kleiner" über die Ziffern $0..9$:
:dot expr_as_graph ("teilbar",{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")})
```
%% Output
<Dot visualization: expr_as_graph [("teilbar",{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")})]>
%% Cell type:markdown id: tags:
Das Kartesische Produkt stellt die Relation dar, die immer wahr ist (für die angegebenen Basismengen). Als Graph ist dies der [vollständige Graph](https://de.wikipedia.org/wiki/Vollständiger_Graph) über die Basismengen:
Man kann die transitive Hülle natürlich mit den anderen Operatoren verknüpfen, zum Beispiel um auszurechnen von welchen Knoten aus man den Knoten 3 erreichen kann:
%% Cell type:code id: tags:
``` prob
closure1(r)⁻¹[{3}]
```
%% Output
$\{1,2\}$
{1,2}
%% Cell type:markdown id: tags:
Anmerkung: die reflexive und transitive Hülle in B wird als ```closure``` geschrieben, ist bei Relationen über Zahlen immer unendlich.
Eine Funktion kann also als Menge von Paaren dargestellt werden. Es sind aber nicht alle Mengen an Paaren auch Funktionen. Zum Beispiel, unsere Relation sub1 von oben ist keine Funktion:
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("sub1",sub1)
```
%% Output
<Dot visualization: expr_as_graph [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)
)END]>
%% 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:
Anmerkung: es wird nicht geprüft ob der komplette Wertebereich abgedeckt wird:
%% Cell type:code id: tags:
``` prob
i10 ∈ 1..10 --> 0..100
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Es wird aber wohl geprüft ob der Definitionsbereich komplett abgedeckt wird:
%% Cell type:code id: tags:
``` prob
i10 ∈ 2..10 --> 0..100
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
i10 ∈ 0..10 --> 0..100
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
dom(i10)
```
%% Output
$\{1,2,3,4,5,6,7,8,9,10\}$
{1,2,3,4,5,6,7,8,9,10}
%% Cell type:markdown id: tags:
Was kann man mit Funktionen machen? Da Funktionen *nur* besondere Relationen sind, und Relationen *nur* besondere Mengen sind, kann man alle Mengen und Relationsoperatoren anwenden:
%% Cell type:code id: tags:
``` prob
(4,z) ∈ i10
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{z} = 5$
TRUE
Solution:
z = 5
%% Cell type:code id: tags:
``` prob
dom(i10)
```
%% Output
$\{1,2,3,4,5,6,7,8,9,10\}$
{1,2,3,4,5,6,7,8,9,10}
%% Cell type:code id: tags:
``` prob
ran(i10)
```
%% Output
$\{2,3,4,5,6,7,8,9,10,11\}$
{2,3,4,5,6,7,8,9,10,11}
%% Cell type:code id: tags:
``` prob
i10[{4,5}]
```
%% Output
$\{5,6\}$
{5,6}
%% Cell type:code id: tags:
``` prob
i10[{4}]
```
%% Output
$\{5\}$
{5}
%% Cell type:code id: tags:
``` prob
i10⁻¹[{4}]
```
%% Output
$\{3\}$
{3}
%% Cell type:code id: tags:
``` prob
(i10 ; i10)[{4}]
```
%% Output
$\{6\}$
{6}
%% Cell type:code id: tags:
``` prob
closure1(i10)[{4}]
```
%% Output
$\{5,6,7,8,9,10,11\}$
{5,6,7,8,9,10,11}
%% Cell type:code id: tags:
``` prob
closure1(i10~)[{4}]
```
%% Output
$\{1,2,3\}$
{1,2,3}
%% Cell type:markdown id: tags:
Anmerkung: um den Wert einer Funktion $F$ für eine Eingabe $x$ zu berechnen, kann man das relationale Bild $F[\{x\}]$ verwenden. Aber: das Ergebnis ist eine Menge! Man kann also nicht direkt zB arithmetische Operatoren anwenden. Dafür wird eine neue Operation für Funktionen eingeführt: die **Funktionsanwendung**: ```F(x)```.
%% Cell type:code id: tags:
``` prob
i10(4)
```
%% Output
$5$
5
%% Cell type:code id: tags:
``` prob
i10(4) + i10(4)
```
%% Output
$10$
10
%% Cell type:markdown id: tags:
Es ist ein Fehler eine Funktion ausserhalb des Definitionsbereiches anzuwenden. Beim relationalen Bild ist dies erlaubt und man bekommt dort die leere Menge als Ausgabe.
* Mengenausdrücke verstehen und nach Logik übersetzen können
* Problemstellungen nach Logik und Mengentheorie übersetzen können
* Relationen, Funktionen und Folgen in Mengendarstellung bearbeiten können
...
...
%% Cell type:markdown id: tags:
# Theoretische Informatik - Vorlesung 0 - Teil 2 Mengentheorie
* April 2023
* April 2020
* Michael Leuschel
* Lehrstuhl Softwaretechnik und Programmiersprachen
* Heinrich-Heine Universität Düsseldorf
Grundlagen der Logik und Mengentheorie sind nicht im Skript.
Hier definieren wir einige Grundlagen und Notationen die im Skript verwendet werden.
Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich.
Auswertung der Formeln erfolgt mit dem [Jupyter Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) für [ProB](https://prob.hhu.de/w/)
Um dieses Notebook zu starten kann man entweder selber Jupyter und den [ProB-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren.
Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger):
* _"Unter einer ‚Menge‘ verstehen wir jede Zusammenfassung M von bestimmten wohlunterschiedenen Objekten m unserer Anschauung oder unseres Denkens (welche die ‚Elemente‘ von M genannt werden) zu einem Ganzen."_ Georg Cantor (siehe [Textstelle als Bild in Wikipedia](https://de.wikipedia.org/wiki/Datei:Textstelle_mit_der_Mengendefinition_von_Georg_Cantor.png))
* _"The ability to regard any collection of objects as a single entity (i.e., as a set)."_ (Keith Devlin. Joy of Sets. Springer-Verlag.)
%% Cell type:markdown id: tags:
In der Regel gibt es eine Domäne an "Objekten" mit denen man Mengen bauen kann.
Was genau diese Objekte sind interessiert uns in der Mengentheorie nicht.
Fundamental sind diese beiden Symbole:
* wenn $a$ ein Objekt ist und $x$ eine Menge, dann
* ist $a \in x$ wahr, wenn $a$ ein Element von $x$ ist
* ist $a \not\in x$ wahr, wenn $a$ **kein** Element von $x$ ist.
$\in$ und $\not\in$ sind Prädikate, verbunden durch die Eigenschaft:
* $\forall(a,x).(a\not\in x \Leftrightarrow \neg(a \in x))$
%% Cell type:markdown id: tags:
## Die leere Menge und Gleichheit
Eine besondere Menge ist die leere Menge $\emptyset$.
Die Anzahl der Elemente einer Menge $x$ schreiben wir als
* $\mid x\mid$ oder auch als $card(x)$ (B Schreibweise).
%% Cell type:code id: tags:
``` prob
card({1,2,3})
```
%% Output
$3$
3
%% Cell type:code id: tags:
``` prob
card({1,1,2,3,2})
```
%% Output
$3$
3
%% Cell type:code id: tags:
``` prob
card(∅)
```
%% Output
$0$
0
%% Cell type:markdown id: tags:
Achtung, die Kardinalität kann auch unendlich sein: je nach Formalismus, ist folgender Ausdruck entweder unendlich oder nicht wohl definiert: $|\{x \mid x \in \mathbb{Z} \wedge x>0\}|$
%% Cell type:code id: tags:
``` prob
card({x|x∈ℤ ∧ x>0})
```
%% Output
:eval: NOT-WELL-DEFINED:
card applied to very large set, cardinality not representable in ProB: closure([x],[integer],b(greater(b(identifier(...),integer,[...]),b(value(...),integer,[...])),pred,[nodeid(pos(...)),prob_annotation('DO_NOT_ENUMERATE'(...)),removed_typing]))
%% Cell type:markdown id: tags:
# SEND+MORE=MONEY
Als Übung und Beispiel versuchen wir nun ein Problem zu lösen.
Es handelt sich um ein klassisches arithmetisches Puzzle wo acht unterschiedliche Ziffern gefunden werden sollen die folgende Gleichung erfüllen:
| | | | | |
|---|---|---|---|---|
| | S | E | N | D |
| + | M | O | R | E |
|
|= M| O | N | E | Y |
| | | | | |
Wir können dies nun in Logik, Mengentheorie und Arithmetik modellieren und lösen.
%% Cell type:markdown id: tags:
Wir haben acht Ziffern:
%% Cell type:code id: tags:
``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 0$
* $\mathit{S} = 0$
* $\mathit{D} = 0$
* $\mathit{E} = 0$
* $\mathit{Y} = 0$
* $\mathit{M} = 0$
* $\mathit{N} = 0$
* $\mathit{O} = 0$
TRUE
Solution:
R = 0
S = 0
D = 0
E = 0
Y = 0
M = 0
N = 0
O = 0
%% Cell type:markdown id: tags:
diese Ziffern sind alle unterschiedlich:
%% Cell type:code id: tags:
``` prob
{S,E,N,D,M,O,R,Y} ⊆ 0..9 ∧
card({S,E,N,D,M,O,R,Y}) = 8
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 2$
* $\mathit{S} = 0$
* $\mathit{D} = 5$
* $\mathit{E} = 7$
* $\mathit{Y} = 1$
* $\mathit{M} = 4$
* $\mathit{N} = 6$
* $\mathit{O} = 3$
TRUE
Solution:
R = 2
S = 0
D = 5
E = 7
Y = 1
M = 4
N = 6
O = 3
%% Cell type:markdown id: tags:
und wobei die zwei führenden Ziffern S und M ungleich 0 sind:
> 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)$.
Das Kartesische Produkt wird auch Kreuzmenge oder Produktmenge genannt.
%% Cell type:markdown id: tags:
# Binäre Relationen
Eine binäre Relation über $x$ und $y$ ist eine Untermenge des kartesischen Produkts $x \times y$ zweier Mengen. Die Mengen $x$ und $y$ können identisch sein.
Beispiel: die Relation "kleiner" über die Ziffern $0..9$:
:dot expr_as_graph ("teilbar",{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")})
```
%% Output
<Dot visualization: expr_as_graph [("teilbar",{x,y| x:1..7 ∧ (x mod 3 =0 => y = "ja") ∧ (x mod 3 >0 => y= "nein")})]>
%% Cell type:markdown id: tags:
Das Kartesische Produkt stellt die Relation dar, die immer wahr ist (für die angegebenen Basismengen). Als Graph ist dies der [vollständige Graph](https://de.wikipedia.org/wiki/Vollständiger_Graph) über die Basismengen:
Man kann die transitive Hülle natürlich mit den anderen Operatoren verknüpfen, zum Beispiel um auszurechnen von welchen Knoten aus man den Knoten 3 erreichen kann:
%% Cell type:code id: tags:
``` prob
closure1(r)⁻¹[{3}]
```
%% Output
$\{1,2\}$
{1,2}
%% Cell type:markdown id: tags:
Anmerkung: die reflexive und transitive Hülle in B wird als ```closure``` geschrieben, ist bei Relationen über Zahlen immer unendlich.
Eine Funktion kann also als Menge von Paaren dargestellt werden. Es sind aber nicht alle Mengen an Paaren auch Funktionen. Zum Beispiel, unsere Relation sub1 von oben ist keine Funktion:
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("sub1",sub1)
```
%% Output
<Dot visualization: expr_as_graph [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)
)END]>
%% 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:
Anmerkung: es wird nicht geprüft ob der komplette Wertebereich abgedeckt wird:
%% Cell type:code id: tags:
``` prob
i10 ∈ 1..10 --> 0..100
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Es wird aber wohl geprüft ob der Definitionsbereich komplett abgedeckt wird:
%% Cell type:code id: tags:
``` prob
i10 ∈ 2..10 --> 0..100
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
i10 ∈ 0..10 --> 0..100
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
dom(i10)
```
%% Output
$\{1,2,3,4,5,6,7,8,9,10\}$
{1,2,3,4,5,6,7,8,9,10}
%% Cell type:markdown id: tags:
Was kann man mit Funktionen machen? Da Funktionen *nur* besondere Relationen sind, und Relationen *nur* besondere Mengen sind, kann man alle Mengen und Relationsoperatoren anwenden:
%% Cell type:code id: tags:
``` prob
(4,z) ∈ i10
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{z} = 5$
TRUE
Solution:
z = 5
%% Cell type:code id: tags:
``` prob
dom(i10)
```
%% Output
$\{1,2,3,4,5,6,7,8,9,10\}$
{1,2,3,4,5,6,7,8,9,10}
%% Cell type:code id: tags:
``` prob
ran(i10)
```
%% Output
$\{2,3,4,5,6,7,8,9,10,11\}$
{2,3,4,5,6,7,8,9,10,11}
%% Cell type:code id: tags:
``` prob
i10[{4,5}]
```
%% Output
$\{5,6\}$
{5,6}
%% Cell type:code id: tags:
``` prob
i10[{4}]
```
%% Output
$\{5\}$
{5}
%% Cell type:code id: tags:
``` prob
i10⁻¹[{4}]
```
%% Output
$\{3\}$
{3}
%% Cell type:code id: tags:
``` prob
(i10 ; i10)[{4}]
```
%% Output
$\{6\}$
{6}
%% Cell type:code id: tags:
``` prob
closure1(i10)[{4}]
```
%% Output
$\{5,6,7,8,9,10,11\}$
{5,6,7,8,9,10,11}
%% Cell type:code id: tags:
``` prob
closure1(i10~)[{4}]
```
%% Output
$\{1,2,3\}$
{1,2,3}
%% Cell type:markdown id: tags:
Anmerkung: um den Wert einer Funktion $F$ für eine Eingabe $x$ zu berechnen, kann man das relationale Bild $F[\{x\}]$ verwenden. Aber: das Ergebnis ist eine Menge! Man kann also nicht direkt zB arithmetische Operatoren anwenden. Dafür wird eine neue Operation für Funktionen eingeführt: die **Funktionsanwendung**: ```F(x)```.
%% Cell type:code id: tags:
``` prob
i10(4)
```
%% Output
$5$
5
%% Cell type:code id: tags:
``` prob
i10(4) + i10(4)
```
%% Output
$10$
10
%% Cell type:markdown id: tags:
Es ist ein Fehler eine Funktion ausserhalb des Definitionsbereiches anzuwenden. Beim relationalen Bild ist dies erlaubt und man bekommt dort die leere Menge als Ausgabe.