Kapitel 0: · Abschnitt 0.0:

Das Weihnachtstheorem

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 1

Kapitel 0: · Abschnitt 0.0:

Das Weihnachtstheorem

Theorem 24.12Es gibt einen Weihnachtsmann.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 2

Kapitel 0: · Abschnitt 0.0:

Ein Universum voller Formeln und Lebewesen

Um das Weihnachtstheorem zu beweisen, definieren wir zunachst eine Struktur,welche die Logik und die Welt der Lebewesen miteinander verbindet.

DefinitionDas logisch-lebendige Universum Alol besteht aus allen Formeln der Logik ersterStufe und allen Lebewesen, die auf der Erde existieren:

Alol := {ϕ : ϕ ∈ FO[σ] fur eine Signatur σ} ∪ {` : ` ist ein Lebewesen}

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 3

Kapitel 0: · Abschnitt 0.0:

Ein Universum voller Formeln und Lebewesen

Um das Weihnachtstheorem zu beweisen, definieren wir zunachst eine Struktur,welche die Logik und die Welt der Lebewesen miteinander verbindet.

DefinitionDas logisch-lebendige Universum Alol besteht aus allen Formeln der Logik ersterStufe und allen Lebewesen, die auf der Erde existieren:

Alol := {ϕ : ϕ ∈ FO[σ] fur eine Signatur σ} ∪ {` : ` ist ein Lebewesen}

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 3

Kapitel 0: · Abschnitt 0.0:

Die logisch-lebendige Struktur

Um Aussagen uber Formeln und Lebewesen zu tatigen, verwenden wir dielogisch-lebendige Signatur σlol, die fur jede Teilmenge M des logisch-lebendigenUniversums ein einstelliges Relationssysmbol PM bereit stellt. Formal:

σlol := {PM : M ⊆ Alol}

Die logisch-lebendige Welt lasst sich nun als die folgende σlol-Struktur uber demUniversum Alol auffassen.

DefinitionDie logisch-lebendige Struktur Alol ist die σlol-Struktur

Alol := (Alol, (PAlol

M )PM∈σlol)

mit PAlol

M := M fur alle PM ∈ σlol.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 4

Kapitel 0: · Abschnitt 0.0:

Die logisch-lebendige Struktur

Um Aussagen uber Formeln und Lebewesen zu tatigen, verwenden wir dielogisch-lebendige Signatur σlol, die fur jede Teilmenge M des logisch-lebendigenUniversums ein einstelliges Relationssysmbol PM bereit stellt. Formal:

σlol := {PM : M ⊆ Alol}

Die logisch-lebendige Welt lasst sich nun als die folgende σlol-Struktur uber demUniversum Alol auffassen.

DefinitionDie logisch-lebendige Struktur Alol ist die σlol-Struktur

Alol := (Alol, (PAlol

M )PM∈σlol)

mit PAlol

M := M fur alle PM ∈ σlol.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 4

Kapitel 0: · Abschnitt 0.0:

Die logisch-lebendige Struktur

Um Aussagen uber Formeln und Lebewesen zu tatigen, verwenden wir dielogisch-lebendige Signatur σlol, die fur jede Teilmenge M des logisch-lebendigenUniversums ein einstelliges Relationssysmbol PM bereit stellt. Formal:

σlol := {PM : M ⊆ Alol}

Die logisch-lebendige Welt lasst sich nun als die folgende σlol-Struktur uber demUniversum Alol auffassen.

DefinitionDie logisch-lebendige Struktur Alol ist die σlol-Struktur

Alol := (Alol, (PAlol

M )PM∈σlol)

mit PAlol

M := M fur alle PM ∈ σlol.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 4

Kapitel 0: · Abschnitt 0.0:

BeispieleWir betrachten die folgenden Teilmengen von Alol:

• RT . . . die Menge der Rentiere

• ST . . . die Menge der Saugetiere

• ERF . . . die Menge der erfullbaren Formeln

• ALLG . . . die Menge der allgemeingultigen Formeln

Dann folgt:

Alol |= ∀x(PRT(x)→ PST(x)

)Alol 6|= ∀x

(PST(x)→ PRT(x)

)Alol |= ∃x

(PERF(x) ∧ ¬PALLG(x)

)Alol 6|= ∃x

(PALLG(x) ∧ PST(x)

)

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 5

Kapitel 0: · Abschnitt 0.0:

BeispieleWir betrachten die folgenden Teilmengen von Alol:

• RT . . . die Menge der Rentiere

• ST . . . die Menge der Saugetiere

• ERF . . . die Menge der erfullbaren Formeln

• ALLG . . . die Menge der allgemeingultigen Formeln

Dann folgt:

Alol |= ∀x(PRT(x)→ PST(x)

)Alol 6|= ∀x

(PST(x)→ PRT(x)

)Alol |= ∃x

(PERF(x) ∧ ¬PALLG(x)

)Alol 6|= ∃x

(PALLG(x) ∧ PST(x)

)

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 5

Kapitel 0: · Abschnitt 0.0:

BeispieleWir betrachten die folgenden Teilmengen von Alol:

• RT . . . die Menge der Rentiere

• ST . . . die Menge der Saugetiere

• ERF . . . die Menge der erfullbaren Formeln

• ALLG . . . die Menge der allgemeingultigen Formeln

Dann folgt:

Alol |= ∀x(PRT(x)→ PST(x)

)Alol 6|= ∀x

(PST(x)→ PRT(x)

)Alol |= ∃x

(PERF(x) ∧ ¬PALLG(x)

)Alol 6|= ∃x

(PALLG(x) ∧ PST(x)

)

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 5

Kapitel 0: · Abschnitt 0.0:

BeispieleWir betrachten die folgenden Teilmengen von Alol:

• RT . . . die Menge der Rentiere

• ST . . . die Menge der Saugetiere

• ERF . . . die Menge der erfullbaren Formeln

• ALLG . . . die Menge der allgemeingultigen Formeln

Dann folgt:

Alol |= ∀x(PRT(x)→ PST(x)

)Alol 6|= ∀x

(PST(x)→ PRT(x)

)Alol |= ∃x

(PERF(x) ∧ ¬PALLG(x)

)Alol 6|= ∃x

(PALLG(x) ∧ PST(x)

)

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 5

Kapitel 0: · Abschnitt 0.0:

BeispieleWir betrachten die folgenden Teilmengen von Alol:

• RT . . . die Menge der Rentiere

• ST . . . die Menge der Saugetiere

• ERF . . . die Menge der erfullbaren Formeln

• ALLG . . . die Menge der allgemeingultigen Formeln

Dann folgt:

Alol |= ∀x(PRT(x)→ PST(x)

)

Alol 6|= ∀x(PST(x)→ PRT(x)

)Alol |= ∃x

(PERF(x) ∧ ¬PALLG(x)

)Alol 6|= ∃x

(PALLG(x) ∧ PST(x)

)

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 5

Kapitel 0: · Abschnitt 0.0:

BeispieleWir betrachten die folgenden Teilmengen von Alol:

• RT . . . die Menge der Rentiere

• ST . . . die Menge der Saugetiere

• ERF . . . die Menge der erfullbaren Formeln

• ALLG . . . die Menge der allgemeingultigen Formeln

Dann folgt:

Alol |= ∀x(PRT(x)→ PST(x)

)Alol 6|= ∀x

(PST(x)→ PRT(x)

)

Alol |= ∃x(PERF(x) ∧ ¬PALLG(x)

)Alol 6|= ∃x

(PALLG(x) ∧ PST(x)

)

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 5

Kapitel 0: · Abschnitt 0.0:

BeispieleWir betrachten die folgenden Teilmengen von Alol:

• RT . . . die Menge der Rentiere

• ST . . . die Menge der Saugetiere

• ERF . . . die Menge der erfullbaren Formeln

• ALLG . . . die Menge der allgemeingultigen Formeln

Dann folgt:

Alol |= ∀x(PRT(x)→ PST(x)

)Alol 6|= ∀x

(PST(x)→ PRT(x)

)Alol |= ∃x

(PERF(x) ∧ ¬PALLG(x)

)

Alol 6|= ∃x(PALLG(x) ∧ PST(x)

)

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 5

Kapitel 0: · Abschnitt 0.0:

BeispieleWir betrachten die folgenden Teilmengen von Alol:

• RT . . . die Menge der Rentiere

• ST . . . die Menge der Saugetiere

• ERF . . . die Menge der erfullbaren Formeln

• ALLG . . . die Menge der allgemeingultigen Formeln

Dann folgt:

Alol |= ∀x(PRT(x)→ PST(x)

)Alol 6|= ∀x

(PST(x)→ PRT(x)

)Alol |= ∃x

(PERF(x) ∧ ¬PALLG(x)

)Alol 6|= ∃x

(PALLG(x) ∧ PST(x)

)Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 5

Kapitel 0: · Abschnitt 0.0:

Sei nun W ⊆ Alol die (moglicherweise leere) Menge der Weihnachtsmanner.

Dann ist das Weihnachtstheorem aquivalent zu der Aussage

Alol |= ∃y PW(y)

Fur jede Formel ϕ ∈ Alol sei

• βϕ : VAR→ Alol die Belegung mit βϕ(z) := ϕ fur alle z ∈ VAR und

• Iϕ := (Alol, βϕ) die dazugehorige Interpretation.

Sei T die Menge der Formeln, die wahre Aussagen uber sich selbst machen:

T := {ϕ ∈ FO[σlol] : Iϕ |= ϕ}

Beispiele

• Fur alle σlol-Satze ϕ gilt: ϕ ∈ T ⇐⇒ Alol |= ϕ

• PERF(x) ∧ ¬PALLG(x) ∈ T,

da PERF(x) ∧ ¬PALLG(x) erfullbar, aber nicht allgemeingultig ist.

• ¬PST(y) ∈ T, da ¬PST(y) kein Saugetier ist.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 6

Kapitel 0: · Abschnitt 0.0:

Sei nun W ⊆ Alol die (moglicherweise leere) Menge der Weihnachtsmanner.Dann ist das Weihnachtstheorem aquivalent zu der Aussage

Alol |= ∃y PW(y)

Fur jede Formel ϕ ∈ Alol sei

• βϕ : VAR→ Alol die Belegung mit βϕ(z) := ϕ fur alle z ∈ VAR und

• Iϕ := (Alol, βϕ) die dazugehorige Interpretation.

Sei T die Menge der Formeln, die wahre Aussagen uber sich selbst machen:

T := {ϕ ∈ FO[σlol] : Iϕ |= ϕ}

Beispiele

• Fur alle σlol-Satze ϕ gilt: ϕ ∈ T ⇐⇒ Alol |= ϕ

• PERF(x) ∧ ¬PALLG(x) ∈ T,

da PERF(x) ∧ ¬PALLG(x) erfullbar, aber nicht allgemeingultig ist.

• ¬PST(y) ∈ T, da ¬PST(y) kein Saugetier ist.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 6

Kapitel 0: · Abschnitt 0.0:

Sei nun W ⊆ Alol die (moglicherweise leere) Menge der Weihnachtsmanner.Dann ist das Weihnachtstheorem aquivalent zu der Aussage

Alol |= ∃y PW(y)

Fur jede Formel ϕ ∈ Alol sei

• βϕ : VAR→ Alol die Belegung mit βϕ(z) := ϕ fur alle z ∈ VAR und

• Iϕ := (Alol, βϕ) die dazugehorige Interpretation.

Sei T die Menge der Formeln, die wahre Aussagen uber sich selbst machen:

T := {ϕ ∈ FO[σlol] : Iϕ |= ϕ}

Beispiele

• Fur alle σlol-Satze ϕ gilt: ϕ ∈ T ⇐⇒ Alol |= ϕ

• PERF(x) ∧ ¬PALLG(x) ∈ T,

da PERF(x) ∧ ¬PALLG(x) erfullbar, aber nicht allgemeingultig ist.

• ¬PST(y) ∈ T, da ¬PST(y) kein Saugetier ist.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 6

Kapitel 0: · Abschnitt 0.0:

Sei nun W ⊆ Alol die (moglicherweise leere) Menge der Weihnachtsmanner.Dann ist das Weihnachtstheorem aquivalent zu der Aussage

Alol |= ∃y PW(y)

Fur jede Formel ϕ ∈ Alol sei

• βϕ : VAR→ Alol die Belegung mit βϕ(z) := ϕ fur alle z ∈ VAR und

• Iϕ := (Alol, βϕ) die dazugehorige Interpretation.

Sei T die Menge der Formeln, die wahre Aussagen uber sich selbst machen:

T := {ϕ ∈ FO[σlol] : Iϕ |= ϕ}

Beispiele

• Fur alle σlol-Satze ϕ gilt: ϕ ∈ T ⇐⇒ Alol |= ϕ

• PERF(x) ∧ ¬PALLG(x) ∈ T,

da PERF(x) ∧ ¬PALLG(x) erfullbar, aber nicht allgemeingultig ist.

• ¬PST(y) ∈ T, da ¬PST(y) kein Saugetier ist.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 6

Kapitel 0: · Abschnitt 0.0:

Sei nun W ⊆ Alol die (moglicherweise leere) Menge der Weihnachtsmanner.Dann ist das Weihnachtstheorem aquivalent zu der Aussage

Alol |= ∃y PW(y)

Fur jede Formel ϕ ∈ Alol sei

• βϕ : VAR→ Alol die Belegung mit βϕ(z) := ϕ fur alle z ∈ VAR und

• Iϕ := (Alol, βϕ) die dazugehorige Interpretation.

Sei T die Menge der Formeln, die wahre Aussagen uber sich selbst machen:

T := {ϕ ∈ FO[σlol] : Iϕ |= ϕ}

Beispiele

• Fur alle σlol-Satze ϕ gilt: ϕ ∈ T ⇐⇒ Alol |= ϕ

• PERF(x) ∧ ¬PALLG(x) ∈ T,

da PERF(x) ∧ ¬PALLG(x) erfullbar, aber nicht allgemeingultig ist.

• ¬PST(y) ∈ T, da ¬PST(y) kein Saugetier ist.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 6

Kapitel 0: · Abschnitt 0.0:

Sei nun W ⊆ Alol die (moglicherweise leere) Menge der Weihnachtsmanner.Dann ist das Weihnachtstheorem aquivalent zu der Aussage

Alol |= ∃y PW(y)

Fur jede Formel ϕ ∈ Alol sei

• βϕ : VAR→ Alol die Belegung mit βϕ(z) := ϕ fur alle z ∈ VAR und

• Iϕ := (Alol, βϕ) die dazugehorige Interpretation.

Sei T die Menge der Formeln, die wahre Aussagen uber sich selbst machen:

T := {ϕ ∈ FO[σlol] : Iϕ |= ϕ}

Beispiele

• Fur alle σlol-Satze ϕ gilt: ϕ ∈ T ⇐⇒ Alol |= ϕ

• PERF(x) ∧ ¬PALLG(x) ∈ T,

da PERF(x) ∧ ¬PALLG(x) erfullbar, aber nicht allgemeingultig ist.

• ¬PST(y) ∈ T, da ¬PST(y) kein Saugetier ist.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 6

Kapitel 0: · Abschnitt 0.0:

Sei nun W ⊆ Alol die (moglicherweise leere) Menge der Weihnachtsmanner.Dann ist das Weihnachtstheorem aquivalent zu der Aussage

Alol |= ∃y PW(y)

Fur jede Formel ϕ ∈ Alol sei

• βϕ : VAR→ Alol die Belegung mit βϕ(z) := ϕ fur alle z ∈ VAR und

• Iϕ := (Alol, βϕ) die dazugehorige Interpretation.

Sei T die Menge der Formeln, die wahre Aussagen uber sich selbst machen:

T := {ϕ ∈ FO[σlol] : Iϕ |= ϕ}

Beispiele

• Fur alle σlol-Satze ϕ gilt: ϕ ∈ T ⇐⇒ Alol |= ϕ

• PERF(x) ∧ ¬PALLG(x) ∈ T,

da PERF(x) ∧ ¬PALLG(x) erfullbar, aber nicht allgemeingultig ist.

• ¬PST(y) ∈ T, da ¬PST(y) kein Saugetier ist.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 6

Kapitel 0: · Abschnitt 0.0:

Sei nun W ⊆ Alol die (moglicherweise leere) Menge der Weihnachtsmanner.Dann ist das Weihnachtstheorem aquivalent zu der Aussage

Alol |= ∃y PW(y)

Fur jede Formel ϕ ∈ Alol sei

• βϕ : VAR→ Alol die Belegung mit βϕ(z) := ϕ fur alle z ∈ VAR und

• Iϕ := (Alol, βϕ) die dazugehorige Interpretation.

Sei T die Menge der Formeln, die wahre Aussagen uber sich selbst machen:

T := {ϕ ∈ FO[σlol] : Iϕ |= ϕ}

Beispiele

• Fur alle σlol-Satze ϕ gilt: ϕ ∈ T ⇐⇒ Alol |= ϕ

• PERF(x) ∧ ¬PALLG(x) ∈ T,

da PERF(x) ∧ ¬PALLG(x) erfullbar, aber nicht allgemeingultig ist.

• ¬PST(y) ∈ T, da ¬PST(y) kein Saugetier ist.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 6

Kapitel 0: · Abschnitt 0.0:

Sei nun W ⊆ Alol die (moglicherweise leere) Menge der Weihnachtsmanner.Dann ist das Weihnachtstheorem aquivalent zu der Aussage

Alol |= ∃y PW(y)

Fur jede Formel ϕ ∈ Alol sei

• βϕ : VAR→ Alol die Belegung mit βϕ(z) := ϕ fur alle z ∈ VAR und

• Iϕ := (Alol, βϕ) die dazugehorige Interpretation.

Sei T die Menge der Formeln, die wahre Aussagen uber sich selbst machen:

T := {ϕ ∈ FO[σlol] : Iϕ |= ϕ}

Beispiele

• Fur alle σlol-Satze ϕ gilt: ϕ ∈ T ⇐⇒ Alol |= ϕ

• PERF(x) ∧ ¬PALLG(x) ∈ T,

da PERF(x) ∧ ¬PALLG(x) erfullbar, aber nicht allgemeingultig ist.

• ¬PST(y) ∈ T, da ¬PST(y) kein Saugetier ist.

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 6

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Beweis

Iψ |= PT(x) ⇐⇒ βψ(x) ∈ PAlol

T (da Iψ = (Alol, βψ))

⇐⇒ ψ ∈ T (da βψ(x) := ψ und PAlol

T := T)

⇐⇒ Iψ |= ψ (Definition von T)

Lemma 2(PT(x)→ ψ) ≡ ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Beweis

Iψ |= PT(x) ⇐⇒ βψ(x) ∈ PAlol

T (da Iψ = (Alol, βψ))

⇐⇒ ψ ∈ T (da βψ(x) := ψ und PAlol

T := T)

⇐⇒ Iψ |= ψ (Definition von T)

Lemma 2(PT(x)→ ψ) ≡ ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Beweis

Iψ |= PT(x) ⇐⇒ βψ(x) ∈ PAlol

T (da Iψ = (Alol, βψ))

⇐⇒ ψ ∈ T (da βψ(x) := ψ und PAlol

T := T)

⇐⇒ Iψ |= ψ (Definition von T)

Lemma 2(PT(x)→ ψ) ≡ ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis.Das Lemma folgt aus einfachen Aquivalenzumformumgen:(

PT(x)→ ψ)

=(PT(x)→

(PT(x)→ ∃yPW(y)

))

≡(¬PT(x) ∨

(¬PT(x) ∨ ∃yPW(y)

))≡(¬PT(x) ∨ ∃yPW(y)

)≡(PT(x)→ ∃yPW(y)

)= ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis.Das Lemma folgt aus einfachen Aquivalenzumformumgen:(

PT(x)→ ψ)

=(PT(x)→

(PT(x)→ ∃yPW(y)

))≡(¬PT(x) ∨

(¬PT(x) ∨ ∃yPW(y)

))

≡(¬PT(x) ∨ ∃yPW(y)

)≡(PT(x)→ ∃yPW(y)

)= ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis.Das Lemma folgt aus einfachen Aquivalenzumformumgen:(

PT(x)→ ψ)

=(PT(x)→

(PT(x)→ ∃yPW(y)

))≡(¬PT(x) ∨

(¬PT(x) ∨ ∃yPW(y)

))≡(¬PT(x) ∨ ∃yPW(y)

)

≡(PT(x)→ ∃yPW(y)

)= ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis.Das Lemma folgt aus einfachen Aquivalenzumformumgen:(

PT(x)→ ψ)

=(PT(x)→

(PT(x)→ ∃yPW(y)

))≡(¬PT(x) ∨

(¬PT(x) ∨ ∃yPW(y)

))≡(¬PT(x) ∨ ∃yPW(y)

)≡(PT(x)→ ∃yPW(y)

)= ψ

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis von Theorem 24.12.Es bleibt zu zeigen, dass Alol |= ∃y PW(y).

(A) Iψ |= (PT(x)→ ψ) (folgt aus Lemma 1)

(B) Iψ |= ψ (folgt aus (A) und Lemma 2)

(C) Iψ |= PT(x) (folgt aus (B) und Lemma 1)

(D) Iψ |= ∃y PW(y) (modus ponens mit (B) und (C))

=⇒ Alol |= ∃y PW(y) (Koinzidenzlemma und (D))

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis von Theorem 24.12.Es bleibt zu zeigen, dass Alol |= ∃y PW(y).

Aus den beiden Lemmata und der Definition von ψ folgt:

(A) Iψ |= (PT(x)→ ψ) (folgt aus Lemma 1)

(B) Iψ |= ψ (folgt aus (A) und Lemma 2)

(C) Iψ |= PT(x) (folgt aus (B) und Lemma 1)

(D) Iψ |= ∃y PW(y) (modus ponens mit (B) und (C))

=⇒ Alol |= ∃y PW(y) (Koinzidenzlemma und (D))

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis von Theorem 24.12.Es bleibt zu zeigen, dass Alol |= ∃y PW(y).

Aus den beiden Lemmata und der Definition von ψ folgt:

(A) Iψ |= (PT(x)→ ψ) (folgt aus Lemma 1)

(B) Iψ |= ψ (folgt aus (A) und Lemma 2)

(C) Iψ |= PT(x) (folgt aus (B) und Lemma 1)

(D) Iψ |= ∃y PW(y) (modus ponens mit (B) und (C))

=⇒ Alol |= ∃y PW(y) (Koinzidenzlemma und (D))

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis von Theorem 24.12.Es bleibt zu zeigen, dass Alol |= ∃y PW(y).

Aus den beiden Lemmata und der Definition von ψ folgt:

(A) Iψ |= (PT(x)→ ψ) (folgt aus Lemma 1)

(B) Iψ |= ψ (folgt aus (A) und Lemma 2)

(C) Iψ |= PT(x) (folgt aus (B) und Lemma 1)

(D) Iψ |= ∃y PW(y) (modus ponens mit (B) und (C))

=⇒ Alol |= ∃y PW(y) (Koinzidenzlemma und (D))

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis von Theorem 24.12.Es bleibt zu zeigen, dass Alol |= ∃y PW(y).

Aus den beiden Lemmata und der Definition von ψ folgt:

(A) Iψ |= (PT(x)→ ψ) (folgt aus Lemma 1)

(B) Iψ |= ψ (folgt aus (A) und Lemma 2)

(C) Iψ |= PT(x) (folgt aus (B) und Lemma 1)

(D) Iψ |= ∃y PW(y) (modus ponens mit (B) und (C))

=⇒ Alol |= ∃y PW(y) (Koinzidenzlemma und (D))

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis von Theorem 24.12.Es bleibt zu zeigen, dass Alol |= ∃y PW(y).

Aus den beiden Lemmata und der Definition von ψ folgt:

(A) Iψ |= (PT(x)→ ψ) (folgt aus Lemma 1)

(B) Iψ |= ψ (folgt aus (A) und Lemma 2)

(C) Iψ |= PT(x) (folgt aus (B) und Lemma 1)

(D) Iψ |= ∃y PW(y) (modus ponens mit (B) und (C))

=⇒ Alol |= ∃y PW(y) (Koinzidenzlemma und (D))

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Im folgenden sei ψ :=(PT(x)→ ∃y PW(y)

).

Lemma 1Iψ |= PT(x) ⇐⇒ Iψ |= ψ

Lemma 2(PT(x)→ ψ) ≡ ψ

Beweis von Theorem 24.12.Es bleibt zu zeigen, dass Alol |= ∃y PW(y).

Aus den beiden Lemmata und der Definition von ψ folgt:

(A) Iψ |= (PT(x)→ ψ) (folgt aus Lemma 1)

(B) Iψ |= ψ (folgt aus (A) und Lemma 2)

(C) Iψ |= PT(x) (folgt aus (B) und Lemma 1)

(D) Iψ |= ∃y PW(y) (modus ponens mit (B) und (C))

=⇒ Alol |= ∃y PW(y) (Koinzidenzlemma und (D))

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 7

Kapitel 0: · Abschnitt 0.0:

Historisches

• Der Beweis des Weihnachtstheorems beruht auf Currys Paradoxon, welchesverwandt mit dem Paradoxon des Barbiers von Sonnenthal ist.

• Eine wichtige Anwendung dieser Schlussweise ist der Satz von Lob.

• Mit dem gleichen Argument kann man auch zeigen, dass es neun fliegendeRentiere gibt, d. h.

Alol |= ∃x1 · · · ∃x9

( ∧16i<j69

¬xi = xj ∧∧i∈[9]

(PRT(xi ) ∧ PFLIEGT(xi )

) )(Details: Ubung)

DadurchhabenwirAlolunterVerwendungvonAloldefiniert,wasimallgemeinennichterlaubtist.welchedieMengeallerSatzeenthalt,dievonAlolerfulltwerden.DiezwielichtigeStelleinunseremBeweisistdieselbstbezuglicheDefinitionvonP

AlolT

,

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 8

Kapitel 0: · Abschnitt 0.0:

Historisches

• Der Beweis des Weihnachtstheorems beruht auf Currys Paradoxon, welchesverwandt mit dem Paradoxon des Barbiers von Sonnenthal ist.

• Eine wichtige Anwendung dieser Schlussweise ist der Satz von Lob.

• Mit dem gleichen Argument kann man auch zeigen, dass es neun fliegendeRentiere gibt, d. h.

Alol |= ∃x1 · · · ∃x9

( ∧16i<j69

¬xi = xj ∧∧i∈[9]

(PRT(xi ) ∧ PFLIEGT(xi )

) )(Details: Ubung)

DadurchhabenwirAlolunterVerwendungvonAloldefiniert,wasimallgemeinennichterlaubtist.welchedieMengeallerSatzeenthalt,dievonAlolerfulltwerden.DiezwielichtigeStelleinunseremBeweisistdieselbstbezuglicheDefinitionvonP

AlolT

,

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 8

Kapitel 0: · Abschnitt 0.0:

Historisches

• Der Beweis des Weihnachtstheorems beruht auf Currys Paradoxon, welchesverwandt mit dem Paradoxon des Barbiers von Sonnenthal ist.

• Eine wichtige Anwendung dieser Schlussweise ist der Satz von Lob.

• Mit dem gleichen Argument kann man auch zeigen, dass es neun fliegendeRentiere gibt

, d. h.

Alol |= ∃x1 · · · ∃x9

( ∧16i<j69

¬xi = xj ∧∧i∈[9]

(PRT(xi ) ∧ PFLIEGT(xi )

) )(Details: Ubung)

DadurchhabenwirAlolunterVerwendungvonAloldefiniert,wasimallgemeinennichterlaubtist.welchedieMengeallerSatzeenthalt,dievonAlolerfulltwerden.DiezwielichtigeStelleinunseremBeweisistdieselbstbezuglicheDefinitionvonP

AlolT

,

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 8

Kapitel 0: · Abschnitt 0.0:

Historisches

• Der Beweis des Weihnachtstheorems beruht auf Currys Paradoxon, welchesverwandt mit dem Paradoxon des Barbiers von Sonnenthal ist.

• Eine wichtige Anwendung dieser Schlussweise ist der Satz von Lob.

• Mit dem gleichen Argument kann man auch zeigen, dass es neun fliegendeRentiere gibt, d. h.

Alol |= ∃x1 · · · ∃x9

( ∧16i<j69

¬xi = xj ∧∧i∈[9]

(PRT(xi ) ∧ PFLIEGT(xi )

) )(Details: Ubung)

DadurchhabenwirAlolunterVerwendungvonAloldefiniert,wasimallgemeinennichterlaubtist.welchedieMengeallerSatzeenthalt,dievonAlolerfulltwerden.DiezwielichtigeStelleinunseremBeweisistdieselbstbezuglicheDefinitionvonP

AlolT

,

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 8

Kapitel 0: · Abschnitt 0.0:

Historisches

• Der Beweis des Weihnachtstheorems beruht auf Currys Paradoxon, welchesverwandt mit dem Paradoxon des Barbiers von Sonnenthal ist.

• Eine wichtige Anwendung dieser Schlussweise ist der Satz von Lob.

• Mit dem gleichen Argument kann man auch zeigen, dass es neun fliegendeRentiere gibt, d. h.

Alol |= ∃x1 · · · ∃x9

( ∧16i<j69

¬xi = xj ∧∧i∈[9]

(PRT(xi ) ∧ PFLIEGT(xi )

) )(Details: Ubung)

DadurchhabenwirAlolunterVerwendungvonAloldefiniert,wasimallgemeinennichterlaubtist.welchedieMengeallerSatzeenthalt,dievonAlolerfulltwerden.DiezwielichtigeStelleinunseremBeweisistdieselbstbezuglicheDefinitionvonP

AlolT

,

Christoph Berkholz · HU Berlin · Vorlesung Logik in der Informatik Version vom 20. Dezember 2018 Folie 8