9. World 9: Puzzles
Three puzzles. All need classical logic, and all need some planning: think about the proof first, then build it.
Drei Rätsel. Alle brauchen klassische Logik, und alle brauchen etwas Planung: Überlege dir den Beweis zuerst, dann baue ihn.
The drinker paradox: in every pub there is someone such that, if they drink (P), everybody drinks. Classical, with TND.
The lemma of level 8.20 helps: from (∀ x, P x) → ⊥ it gives ∃ x, P x → ⊥ (in Lean push_neg).
Das Trinker-Paradox: In jeder Kneipe gibt es jemanden, für den gilt: Wenn er trinkt (P), trinken alle. Klassisch, mit TND.
Dabei hilft der Hilfssatz aus Level 8.20: Aus (∀ x, P x) → ⊥ macht er ∃ x, P x → ⊥ (in Lean push_neg).
The hardest level of the Proof Machine. Find an object b with R b first; then look at R (f (f b)).
Das schwerste Level der Proof Machine. Finde zuerst ein Objekt b mit R b; dann schau dir R (f (f b)) an.
The final level, a puzzle of propositional logic by Raymond Smullyan. On an island, knights always tell the truth and
knaves always lie. A says: “We are both knaves.” Let A stand for “A is a knight” and B for “B is
a knight”. That A says it means: A holds exactly when what A says is true, A ↔ (A → ⊥) ∧ (B → ⊥).
Show: A is a knave and B is a knight. First show A → ⊥.
Das letzte Level, ein Rätsel der Aussagenlogik von Raymond Smullyan. Auf einer Insel sagen Ritter immer die Wahrheit,
und Schurken lügen immer. A sagt: „Wir sind beide Schurken.“ A steht für „A ist ein Ritter“, B
für „B ist ein Ritter“. Dass A das sagt, bedeutet: A gilt genau dann, wenn wahr ist, was A sagt,
A ↔ (A → ⊥) ∧ (B → ⊥). Zeige: A ist ein Schurke und B ein Ritter. Zeige zuerst A → ⊥.