热门问题
时间线
聊天
视角

飲者悖論

来自维基百科,自由的百科全书

Remove ads

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

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

Remove ads

證明

以下證明為藉助 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.

Remove ads

參考資料

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.

Remove ads