39. The drinker paradox
Raymond Smullyan’s drinker paradox: in any nonempty pub there is a person such that, if that person is drinking, then everyone in the pub is drinking. It sounds wrong, but it is a theorem of classical logic.
Prove it for a type α of people with at least one person a in the pub, and any predicate D saying who drinks.
Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.
1theorem solution (α : Type) (a : α) (D : α → Prop) : ∃ x, D x → ∀ y, D y := by
givenLoading editor…
Type
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
α:Type
a:α
D:α → Prop
⊢∃ x, D x → ∀ y, D y
ReadyLn 1, Col 1Lean 4
Draft saved in this browser