跳至內容

飲者悖論

維基百科,自由的百科全書

飲者悖論(也被稱為飲者定理,飲者原理,或飲酒原理)是經典謂詞邏輯的一個定理。它實際上並不是一個悖論。它的明顯的矛盾的性質來自於它通常的在自然語言中的表述:在酒吧裏會有一個人,對於這個人,如果他在喝酒,那麼所有在酒吧裏的人都在喝酒。 有兩點看起來是反直覺的 1) 這裏面有一個人,他會引起其他人喝酒。2)這裏有一個人,一整夜他都是最後一個喝酒的。第一個反對的理由是由於混淆了形式的 IF...THEN 陳述與因果關係(見相關不蘊涵因果)。定理的形式化陳述是不受時間限制的,我們可以消除第二個反對理由是因為,在一個時刻使得陳述成立的那個特別的人(見證者),並不需要與在任何其它時刻使得陳述成立的那個人是同一個人。實際的定理是

其中 D 是一個任意的謂詞英語Predicate_(mathematical_logic),P是一個任意的集合。這個悖論是因數理邏輯學家雷蒙·思木里安而廣為人知的。雷蒙·思木里安在他 1978 年出版的書 What is the Name of this Book?[1] 中稱它為 「飲酒原理」。

證明

[編輯]

以下證明為藉助 Coq 的 proof script.

Lemma drinker (X: Type)(d: X -> Prop):
XM -> (exists x: X, True) -> exists x, d x -> forall x, d x.
Proof.
  intros xm A. assert(s:= xm). specialize (s (exists x, d x -> forall x, d x)). destruct s as [s0 | s1].
  - exact s0.
  - exfalso. apply s1. destruct A as [x _]. exists x. intros B x0. specialize (xm (d x0)). destruct xm as [xm0 | xm1].
    -- exact xm0.
    -- exfalso. apply s1. exists x0. intros C. exfalso. exact(xm1 C).
Qed.

參考資料

[編輯]
  1. ^ Raymond Smullyan. What is the Name of this Book? The Riddle of Dracula and Other Logical Puzzles. Prentice Hall. 1978. chapter 14. How to Prove Anything. (topic) 250. The Drinking Principle. pp. 209–211. ISBN 0-13-955088-7.