stanford-oval/wikipedia huggingface dataset:
一阶逻辑
常用的推理性質 > 否定

以下的證明會分成使用（A3）的部分跟將公理（A3）取代為（T1）的部分，用以證明兩者的等價性。
（DNe） Double negation, elimination — 

 \vdash \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}
（DNi） Double negation, introduction — 

 \vdash {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}
上面兩定理表達了雙否定推理上等價於於原公式，引用兩者任一會都以（DN）簡寫。
（T1） Transposition-1 — 

 \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}\vdash {\mathcal {B}}\Rightarrow {\mathcal {A}}
（T2） Transposition-2 — 

 {\mathcal {B}}\Rightarrow {\mathcal {A}}\vdash \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}
注意到（T2）的證明引用了（T1）+（DN），但之前已經證明了（A1）+（A2）+（A3）可以推出（T1）；還有（A1）+（A2）+（T1）也可以推出（DN），所以註明使用（T1）即可。
以上二定理說明  {\mathcal {B}}\Rightarrow {\mathcal {A}} 推理上等價於  \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}} ，引用這兩個定理中任一都以（T）表示。
至此，已經可以證明（A1）+（A2）+（T1）可以推出（A3）：
所以綜合以上所述，在有（A1）+（A2）的前提下，公理（T1）等價於公理（A3）。
由（T）可以得到類似於公理（A3）的定理
（A3'） — 

 {\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}
常用的推理性質 > 實質條件

以下的定理重現了實質條件的直觀理解。
（M0）material condition — 

 \neg {\mathcal {A}},{\mathcal {A}}\vdash {\mathcal {B}}
（也就是 \neg {\mathcal {A}}\vdash {\mathcal {A}}\Rightarrow {\mathcal {B}}）
（M1）material condition — 

 {\mathcal {A}},\neg {\mathcal {B}}\vdash \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})
（M2）material condition — 

 \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash \neg {\mathcal {B}}
（M3）material condition — 

 \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {A}}
常用的推理性質 > 反證法

（C1）Proof by Contradiction — 

 {\mathcal {A}}\Rightarrow \neg {\mathcal {B}},{\mathcal {B}}\vdash \neg {\mathcal {A}}
（C2）Proof by Contradiction — 

 \neg {\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}}
常用的推理性質 > 邏輯與和邏輯或 > 且與或的交換性

以下為邏輯與的交換性
元定理 — 

 \vdash ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow ({\mathcal {B}}\wedge {\mathcal {A}})
類似的，（C2）正是邏輯或的交換性：
元定理 — 

 {\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {B}}\vee {\mathcal {A}} （C2, D）
常用的推理性質 > 邏輯與和邏輯或 > 且與或的直觀意義

＂且＂的直觀意義是實質條件元定理的直接結果
（AND）Intuitive meaning of And — 

 {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {A}}\wedge {\mathcal {B}} （M1）
{\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {A}} （M3）
{\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {B}} （M2）
從（AND）和  \Leftrightarrow  的符號定義可知， \vdash {\mathcal {B}}\Leftrightarrow {\mathcal {C}} 的證明可以拆成兩部分；習慣上會以「（  \Rightarrow  ） 」標示  \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}} 部分的證明，而「（  \Leftarrow  ） 」標示  \vdash {\mathcal {C}}\Rightarrow {\mathcal {B}} 部分的證明。
類似的，＂或＂的直觀意義是（M0）跟（D）的直截結果
（OR）Intuitive meaning of OR — 

 {\mathcal {A}}\vdash {\mathcal {A}}\vee {\mathcal {B}} （M0, DN）
{\mathcal {B}}\vdash {\mathcal {A}}\vee {\mathcal {B}} （A1, D）
{\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {A}}\vdash {\mathcal {B}} （D）
{\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}} （交換性, D）
以下的定理則是（A3'）的直截結果
（DisJ）Disjunction — 

 {\mathcal {A}}\Rightarrow {\mathcal {C}},{\mathcal {B}}\Rightarrow {\mathcal {C}},{\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {C}}
常用的推理性質 > 邏輯與和邏輯或 > 且與或的結合律

對於＂且＂，展開符號定義後，可以從直觀意義輕鬆地得到
（ASO-AND）Associativity of AND — 

 \vdash {\mathcal {A}}\wedge ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\wedge {\mathcal {C}}
＂或＂也有類似的性質
（ASO-OR）Associativity of OR — 

 \vdash {\mathcal {A}}\vee ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\vee {\mathcal {C}}
常用的推理性質 > 邏輯與和邏輯或 > 且與或的分配律

＂且＂和＂或＂之間還有分配律
（DIS-1）Distribution — 

 \vdash {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})
（DIS-2）Distribution — 

 \vdash {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})
常用的推理性質 > 德摩根定律

以下的元定理的名字來自於英國邏輯學家奧古斯塔斯·德摩根。
De Morgan I — 

 \vdash [\neg ({\mathcal {A}}\wedge {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\vee (\neg {\mathcal {B}})]
De Morgan II — 

 \vdash [\neg ({\mathcal {A}}\vee {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\wedge (\neg {\mathcal {B}})]
常用的推理性質 > 普遍化元定理

公理模式（A7）可以稍加延伸成以下的元定理
定理的普遍化 —
對任意變數  x ，若  \vdash {\mathcal {B}} 則有  \vdash (\forall x){\mathcal {B}}。
更進一步，有以下元定裡
（GEN） — 

在  {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n} 裡變數  x 都完全被約束，若
則有
（GEN）可以稍加修飾，以套用在含有存在量詞的公式上
（GENe） —
若變數  x 在  \Gamma  的公式和  {\mathcal {C}} 裡都完全被約束則
（1） 若  \Gamma \vdash {\mathcal {A}}\Rightarrow {\mathcal {B}} 則  \Gamma \vdash (\exists x){\mathcal {A}}\Rightarrow (\exists x){\mathcal {B}}
（2） 若  \Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}} 則  \Gamma \vdash (\exists x){\mathcal {B}}\Rightarrow {\mathcal {C}}
常用的推理性質 > 等價代換

以下的定理，說明兩條「等價」的公式可以互相代換
（Equv）Equivalence of WF — 

 \Gamma  代表一群公式，若公式  {\mathcal {A}} 和  {\mathcal {B}} 滿足：
則對變數  x 和任意公式  {\mathcal {C}} ：
\Gamma \vdash (\neg {\mathcal {A}})\Leftrightarrow (\neg {\mathcal {B}})
\Gamma \vdash ({\mathcal {C}}\Rightarrow {\mathcal {A}})\Leftrightarrow ({\mathcal {C}}\Rightarrow {\mathcal {B}})
\Gamma \vdash ({\mathcal {A}}\Rightarrow {\mathcal {C}})\Leftrightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})
變數  x 於  \Gamma  完全被約束 ，則
這些定理通常是混合使用，以達到「等價代換」的結果，例如，考慮到「邏輯與」是以下的符號定義：
那如果假設  \vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}} ，就有：
\vdash [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]\Leftrightarrow [{\mathcal {B}}\Rightarrow (\neg {\mathcal {C}})]
\vdash \neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]\Leftrightarrow \{\neg [{\mathcal {B}}\Rightarrow (\neg {\mathcal {C}})]\}
換句話說，從「  \vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}  」可以得到「  \vdash ({\mathcal {A}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {B}}\wedge {\mathcal {C}})」，直觀上相當於，把  {\mathcal {A}} 都代換成  {\mathcal {B}} 則兩式等價。日後像這樣遞迴地套用上述定理來得到「代換則某兩式等價」，都簡單地以「引用（Equv）」來表示這段實際的推演過程。
常用的推理性質 > 量詞的可交換性

由普遍化，很容易證明以下關於＂交換性＂的定理
元定理 — 

（1）  (\forall x)(\forall y){\mathcal {A}}\vdash (\forall y)(\forall x){\mathcal {A}}
（2）  (\exists x)(\exists y){\mathcal {A}}\vdash (\exists y)(\exists x){\mathcal {A}}
（3）  (\exists x)(\forall y){\mathcal {A}}\vdash (\forall y)(\exists x){\mathcal {A}}
注意最後（3）一般來說是不能反向的，只要想到＂對每個  a，都有一個數（也就是  -a ），使  a+(-a)=0＂，但是任取一個  a 的數  (-a) 和任意的數  b ，  b+(-a) 並不一定會為零。
常用的推理性質 > 量詞的簡寫

數學中常常有 ＂對所有  \epsilon >0 有...＂，或是 ＂存在  \delta >0 使的...＂。而兩句話比較清晰，接近一階邏輯語言的說法是 ＂對所有  \epsilon  ，只要  \epsilon >0 則...＂ 與  ＂存在  \delta  ，  \delta >0 且...＂。「大於」直觀上是一個二元关系，也就是說，在公理化集合論裡對應於一條  \epsilon  （ 或  \delta  ） 在裡面完全自由的合式公式。據此，可做以下的符號定義
符號定義 — 

如果變數  x 和  y 都於合式公式  {\mathcal {A}}(x,\,y) 裡完全自由，那
[\,\forall {\mathcal {A}}(x,\,y)\,]{\mathcal {B}}:=(\forall x)[\,{\mathcal {A}}(x,\,y)\Rightarrow {\mathcal {B}}\,]
[\,\exists {\mathcal {A}}(x,\,y)\,]{\mathcal {B}}:=(\exists x)[\,{\mathcal {A}}(x,\,y)\wedge {\mathcal {B}}\,]
但直觀上也會說 ＂對所有  n>0 和  m>0 有...＂，這樣連續，帶有條件的全稱量詞也是有＂交換性＂的。 為了討論這個問題，首先需要一些前置的定理
（abb） — 

 \vdash [{\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Leftrightarrow [({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}]
這樣就可以證明以下定理
元定理 — 

如果變數  x 和  y 都於合式公式  {\mathcal {A}}(x,\,y) 和  {\mathcal {B}}(x,\,y) 裡完全自由，若項  T 裡沒有  y 那
\vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\Leftrightarrow \forall x\forall y\{[{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)]\Rightarrow {\mathcal {C}}\}
如果再加上 ＂項  S 裡沒有  x ＂ 那就是 ＂對所有  n>0 和  m>0 有...＂，也就是以上所討論的情況了。以這個定理配上全稱量詞本身的交換性定理，那這句話就可以等價的說成 ＂對所有  m 和  n 若   n>0 且  m>0  則...＂，所以根據＂且＂的可交換性，可以進一步的說成 ＂對所有  m>0 和  n>0 有...＂，所以連續帶有條件的全稱量詞是＂可交換的＂。也就是說
元定理 — 

如果變數  x 和  y 都於合式公式  {\mathcal {A}}(x,\,y) 和  {\mathcal {B}}(x,\,y) 裡完全自由，若項  T 裡沒有  y ，且項  S 裡沒有  x 則
\vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\Leftrightarrow [\,\forall {\mathcal {B}}(y,\,S)\,][\,\forall {\mathcal {A}}(x,\,T)\,]{\mathcal {C}}
但對於帶條件的存在量詞，首先可以得到以下非等價的定理。
元定理 — 

 (\exists x)(\exists y)({\mathcal {A}}\wedge {\mathcal {B}}\wedge {\mathcal {C}})\vdash (\exists x)[\,{\mathcal {A}}\wedge (\exists y)({\mathcal {B}}\wedge {\mathcal {C}})\,]
這是因為一般來說，  (\exists y){\mathcal {D}} 不總是能推出  {\mathcal {D}} 。雖說如此，只要對公式做出一些限制，就會有以下交換的直觀定理：
（Ce）－Commutativity of existential quantification — 

若變數  x 於公式  {\mathcal {Q}} 完全被約束，且  {\mathcal {R}}  是另外一條公式，則：
也就是直觀上，「存在x使得 x>0 且 y>0」與｢y>0 且存在x使得 x>0」是一樣的意思。
常用的推理性質 > 等式定理

一般來說，等式  (x=y) 會被視為某個合式公式  {\mathcal {E}}(x,\,y) 的簡寫。若使用元定理的形式刻劃等式的性質，會作如下的定義
元定義 — 

說一階邏輯理論  {\mathcal {L}} 帶相等符號  {\mathcal {E}}(x,\,y) 意為（  x_{1},\,\cdots ,\,x_{n} 、  x 和  y 都是  {\mathcal {L}} 的任意變數）
除了變數  x 和  y 於  {\mathcal {E}}(x,\,y) 是完全自由外其他變數都完全被約束
（E1）  \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,x) 。
（E2'）  {\mathcal {B}}(x,\,x) 為  {\mathcal {L}} 內不含函數符號與常數符號的原子公式 ， x 若以  {\mathcal {B}}(x,\,y) 表示  {\mathcal {B}}(x,\,x) 內某一個  x 被取代成  y 而成的新公式，則有
（E2＂） 若以  f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n}) 代表項  f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}) 裡的  x_{k} 被取代成  y 而成的新項，則有
（E3）  \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(y,\,x) 。
並在這種狀況下，規定  (x=y) 為  {\mathcal {E}}(x,\,y) 的簡寫。
上面的定義符合函數符號直觀上的＂唯一對應＂。為了證明常數符號的＂唯一性＂，需要以下元定理
元定理 — 

說一階邏輯理論  {\mathcal {L}} 帶相等符號  {\mathcal {E}}(x,\,y) ，等同於要求：
{\mathcal {E}}(x,\,y) 除了變數  x 和  y 於  {\mathcal {E}}(x,\,y) 是完全自由外其他變數都完全被約束。
符合（E1）。
（E2） 對於任意變數  x 和  y，若在公式  {\mathcal {A}} 中自由的  y 都不在  \forall x 的範圍內。若以 {\mathcal {A}}_{y} 代表  {\mathcal {A}} 某些自由的  x  被取代成  y 而成的新公式，則
從上面可以得知，如果等式符號僅僅為斷言符號，那等式和它的公理一節的等式公理模式，是等價於本節的（E1）+（E2'）+（E2＂）。
由上面的元定理，對帶有等式符號的  {\mathcal {L}} 可以證明以下的等式性質
元定理 — 

若  T 、  S 與  R 為  {\mathcal {L}} 的任意項，則有
\vdash _{\mathcal {L}}T=T
\vdash _{\mathcal {L}}(T=S)\Rightarrow (S=T)
\vdash _{\mathcal {L}}(S=T)\Rightarrow [(S=R)\Rightarrow (T=R)]
證明提示：
（E1）+（GEN）+（A4）。
將  (x=x) 帶入（E2）後使用（D2），然後套用兩次（GEN）+（A4）即可。
注意到從（E2）有  \vdash _{\mathcal {L}}(x=y)\Rightarrow [(x=z)\Rightarrow (y=z)]，然後套用三次（GEN）+（A4）即可。
對任意常數符號  c ，上列元定理確保了
也就是常數符號的＂唯一性＂。
函數符號與唯一性 > 唯一性

數學討論中，常常唯一存在某個符合特定條件的數，像是「存在唯一的實數  s\in \mathbb {R}  使的對所有的实数  r\in \mathbb {R}  ，  r+s=r 」；更精確地來說，這句話的意思是：
這樣一般來說，可以對任意變數  x 和合式公式  {\mathcal {B}}(x) 做以下的符號定義：
符號定義 — 

 \exists !x{\mathcal {B}}(x):=\exists x{\mathcal {B}}(x)\wedge (\forall x)(\forall y)[\,{\mathcal {B}}(x)\wedge {\mathcal {B}}(y)\Rightarrow (x=y)\,]
（其中  y 必須是展開以上定義時首次出現的變數；  {\mathcal {B}}(y) 是將  {\mathcal {B}}(x) 內自由的  x 都取代成  y 所形成的新公式。）
注意到要能定義唯一性，一階邏輯理論一定要帶有等號。
函數符號與唯一性 > 新舊理論的等效條件

上節所提到的例子，實際上就是所謂的實數  0 ，但常數符號不能憑空從理論中冒出來，所以仔細來說，「定義實數  0 」的過程應該是在原來的理論添加新的常數符號「  0 」與以下的公理：
這樣的話，「  r>0」就是一條含有新常數符號的敘述，它應等價於：
也就是說，添加「  0 」創造了一套新理論，新理論的每條新敘述會對應到舊理論的某條舊敘述，且照理來說，新的對舊的也會對，反之亦然。
更一般的來說，如果新的一階邏輯理論，是在舊的理論增添一些新符號跟新公理（並額外要求新符號與舊公理相容），那為了讓新舊理論等效，對於任意新理論的合式公式  {\mathcal {C}} ，都要有某條相應的舊理論公式  {\mathcal {C}}^{\prime } 滿足以下條件：
新舊理論的等價條件 — 

（  \vdash _{o} 代表舊理論可以推出；  \vdash _{n} 代表新理論可以推出。）
（1）若  {\mathcal {C}} 本來就內含在舊理論裡，則  {\mathcal {C}}^{\prime } 就是  {\mathcal {C}} 。
（2） \vdash _{n}{\mathcal {C}}^{\prime }\Leftrightarrow {\mathcal {C}}
（3）若  \vdash _{n}{\mathcal {C}} ，則有  \vdash _{o}{\mathcal {C}}^{\prime } 。
從條件（2）事實上就可以推出「若  \vdash _{o}{\mathcal {C}}^{\prime } ，則有  \vdash _{n}{\mathcal {C}} 」，因為  \vdash _{o}{\mathcal {C}}^{\prime } 的話， 新理論只是擴張舊理論而沒改變舊理論固有的定理，所以有  \vdash _{n}{\mathcal {C}}^{\prime } ，但這樣根據條件（2）跟MP律就會有  \vdash _{n}{\mathcal {C}}。所以條件（2）事實上是比「舊的對那新的也對」強的條件，但在之後的推導上（2）會比較方便。
函數符號與唯一性 > 預備定理

在以嚴謹的方式實踐以上提及的直觀動機前，需要一個預備定理
元定理 — 

變數  x 在和合式公式  {\mathcal {B}}(x) 與  {\mathcal {C}}(x) 完全自由，則有
（Aux） \exists !{\mathcal {B}}(x)\vdash (\exists x)[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\Leftrightarrow (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]
函數符號與唯一性 > 新理論的假設

一般來說，如果變數  t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x 在  {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x) 完全自由，且舊理論裡有：
那所謂的新理論，就是添加一個函數符號  f_{k}^{n} 和以下的新公理：
如果僅僅是：
的話，添加的是常數符號  c_{k} 與以下的新公理：
添加常數符號的情況可視為添加函數符號情況的特例，因為常數符號可以視為「零變數」的函數符號。
但不管如何，還需假設  f_{k}^{n} 和新理論的邏輯公理、量詞公理相容，也就是所有公理模式須涵蓋內含  f_{k}^{n} 的項。特別像是（A4）這種將自由變數代換成項的公理模式，也就是說，若項  T 內含  f_{k}^{n} ，且公式  {\mathcal {D}}(x) 內自由的  x 都不在  T 的變數的量詞範圍內，那
仍然是新理論的公理。
另外還需要考慮到  f_{k}^{n} 與等號的相容性（換句話說，新理論仍須是帶等號的一階邏輯理論），這樣的話，考慮到上面等式定理所述的條件（E2''），需額外假設：
新理論的額外假設 — 

對任何介於  1 與  n 的下標  k 和變數  t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x
(t_{k}=x)\Rightarrow [\,f_{k}^{n}(t_{1},\,\ldots ,\,t_{k},\,\ldots ,\,t_{n})=f_{k}^{n}(t_{1},\,\ldots ,\,x,\,\ldots ,\,t_{n})\,]
是公理
（若是添加常數符號的特例，就不須額外假設以上的公理）
這樣就有以下直觀的定理
元定理 — 

對變數  t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x 有
（E） \vdash _{n}[\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Leftrightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)
換句話說，「  s=0  」在新理論裡等價於 「對所有的實數  r\in \mathbb {R}  ，  r+s=r」。
一阶逻辑的元定理

下面列出了一些重要的元逻辑定理。
不像命题演算，一阶逻辑是不可判定性的。对于任意的公式P，可以证实没有判定过程，判定P是否有效，（参见停机问题）。（结论独立的来自于邱奇和图灵。）
有效性的判定问题是半可判定的。按哥德尔完备性定理所展示的，对于任何有效的公式P, P是可证明的。
一元斷言逻辑（就是说，斷言只有一个参数的斷言逻辑）是可判定的。
转换自然语言到一阶逻辑

用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中， p\lor q意味着“要么p要么q要么二者”，就是说它是“包容性”的。在英语中，单词“or”有时是包容性的（比如，“加牛奶或糖？”），有时是排斥性的（比如，“喝咖啡或茶？”，通常意味着取其中一个或另一个但非二者）。类似的，英语单词“some”可以意味着“至少一个，可能全部”，有时意味着“不是全部，可能没有”。英语单词“and”有时要按“or”转换（比如，“男人和女人可以申请”）。
一阶逻辑的限制

所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。
一阶逻辑的限制 > 难于表达if-then-else

带有等式的FOL不包含或允许定义if-then-else斷言或函数if（c,a,b），这裡的c是表达为公式的条件，而a和b是要么都是项要么都是公式，并且它的结果是a如果c为真，或者b如果它为假。问题在于FOL中，斷言和函数二者只接受（“非布尔类型”）项作为参数，而条件的明确表达是（“布尔类型”）公式。这是不幸的，因为很多数学函数是依据if-then-else而方便的表达的，而if-then-else是描述大多数计算机程序的基础。
在数学上，有可能重定义匹配公式算子的新函数的完备集合，但是这是非常笨拙的。
斷言if（c,a,b）如果重写为 (c\wedge a)\lor (\neg c\wedge b)就可以在FOL中表达，但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况斷言叫做“if（条件，a, b）”（这里a和b是公式）和／或函数“ite（条件，a, b）”（这裡的a和b是项），它们都接受一个公式作为条件，并且等于a如果条件为真，或b如果条件为假。这些扩展使FOL易于用于某些问题，并使某类自动定理证明更容易。
其他人进一步扩展FOL使得函数和斷言可以在任何位置接受项和公式二者。
一阶逻辑的限制 > 类型（种类）

除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。
某些人争辩说缺乏类型是巨大优点
，而很多其他人发觉了定义和使用类型（种类）的优点，比如帮助拒绝某些错误或不想要的规定
。
想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂，并也容易导致错误。
单一参数斷言可以用来在合适的地方实现类型的概念。例如：
斷言Man（x）可以被认为是一类“类型断言”（就是说，x必须是男人）。
斷言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如：
容易写成 \exists xMan(x)\rightarrow Mortal(x)，但这将等价与 \exists x\neg Man(x)\lor \exists xMortal(x)（“存在不是男人的事物或者存在是人类的事物”），这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如：
一阶逻辑的限制 > 难于刻画模型大小

条目：二阶逻辑
从Löwenheim–Skolem定理得出在一阶逻辑中不可能刻画有限性或可数性。若一階理論有任意有限大的模型，則也有無窮大的模型，所以說不能刻劃有限性。而若理論有某個無窮基數大小的模型，則也必有任意更大的模型，所以不能刻劃可數性。另一個例子，是無法用一階語言將實數系公理化，因為不論用何種一階理論描述，既然該理論有實數系此種無窮模型（大小為 2^{\aleph _{0}}），所以必有比實數系更大（比如 2^{2^{\aleph _{0}}}）的另一個模型，從而該理論不是（唯一地）刻劃實數系的性質。實數系滿足的公理中，有上确界性质一項，它声称实数的所有有界的、非空集合都有上确界。一階邏輯祗能對元素量化，但此公理中，要對模型的全部子集量化，这就需要二阶逻辑了。
一阶逻辑的限制 > 图可及性不能表达

很多情况可以被建模为节点和有向连接（边）的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用斷言逻辑完全表达。换句话说，没有斷言逻辑公式f，带有u和v作为它的唯一自由变量，而R作为它唯一的（2元）斷言符号，使得f在一个有向图中成立，如果在这个图中存在从关联于u的节点到关联于v的节点的路径。
情人節 (馬)

| 日語寫法 |
| --- | --- |
日語原文: 
平文式罗马字: 
情人節（日语：，英語：），是日本純種競賽馬匹。生涯活躍於一哩及中距離賽事，曾勝出花仙錦標、京都牝馬錦標及愛知盃，亦於優駿牝馬（日本橡樹大賽）、維多利亞一哩賽及女皇伊利沙伯二世盃中跑獲季軍。
出賽前

2002年1月28日出生於北海道早來町（今安平町）北部牧場，成長途中於一口馬主俱樂部Carrot Farm Co. Ltd.進行馬主募集。
競賽生涯 > 2歲

2004年12月12日出戰阪神競馬場2歲新馬戰，維持於中團位置下在直路一舉衝出，最終以 1 3/4馬位優勢取得首勝。
競賽生涯 > 3歲

2005年首戰為條件戰白梅賞，繼續採取居中戰術下於直路爆發出優秀的末腳速度，最終成功超越所有對手並拉開第二名的賽駒2馬位獲勝。
3月5日挑戰鬱金香賞，雖然比賽初段進佔中團位置穩步推進，但於直路上僅能維持均速，最終跑獲第七的戰績。
1星期後為求取得櫻花賞的優先出賽權而連鬥雌馬賽，選擇留後下雖然於通過彎道時候提早取位並在直路不斷衝刺，但仍然敗於前方的萊茵力量、Daring Heart及Air Messiah取得第四。
由於未能獲得優先出賽權以及獎金不足，其放棄櫻花賞並以花仙錦標作為目標。比賽開始後，其緩慢地維持於最後方的位置等待時機，通過第三彎道後逐步加速上前望空。進入直路後，其於外檔位置展開追逐，進入全速狀態下成功跑出全場最快末腳速度，最終以頸位優勢壓贏對手取得首個分級賽冠軍。
其後按照計劃出戰優駿牝馬（日本橡樹大賽），維持於中團靠後位置推進下於第四彎道開始發力取位，並一直尋找有利的加速位置。進入直路後，其嘗試於中檔位置突圍並準備加速，雖然跑出不俗的勢頭，但於最後彎頭仍被西沙里奧及Air Messiah壓制，以第三的戰績完賽。
賽後原定和廄侶西沙里奧一同遠征美國出戰美國橡樹大賽，但於骨折下未能成行並進入休養
競賽生涯 > 4歲

2006年以京都金盃作為首戰，但於其中僅跑獲第六的戰績，其後出戰京都牝馬錦標亦以第五落敗。
3月12日出戰中山牝馬錦標，比賽初段在處於中團位置的情況下於入彎時放慢節奏墮後，於最後彎道開始加速重新上前，但未能對前方的Yamanin Sucre的造成威脅下跑獲第二。
4月轉戰混合賽事，以讀賣盃作為目標。比賽開始後，其一直維持於約莫第六的位置展開推進，並於比賽途中一直處於有遮擋的狀態。進入直路後，其隨即抽出中檔位置望空衝刺，但於中後段逐漸被前方的大和主將及隨心起舞拉開，最終以第三落敗。
5月返回雌馬限定賽事挑戰一級賽維多利亞一哩賽，本次比賽其採取居中戰術，於第九左右的位置穩步推進，但於最後彎道時候經已有動作。進入直路後，其繼續以不俗的姿態展開衝刺，但被同樣位置的Air Messiah壓制下亦未能追上前方的隨心起舞，最終取得第三。
稍為休養後於秋季復出出戰產經賞，比賽初段以較為主動的方式進佔中團的位置，於通過彎道進入直路時嘗試加速透出，可惜最終未能追上各有千秋和大宇宙下以第三完賽。
其後出戰府中牝馬錦標，繼續以居中戰術展開賽事，在比賽途中一直維持沉穩的狀態，未有太大的上前動作。進入直路後，其於外檔位置成功尋找到加速點並逐步侵蝕前方的賽駒，可惜於最後一步仍然未能壓過Daring Heart及Sanrei Jasper，取得第三的戰績。
11月出戰秋季的大目標女皇伊利沙伯二世盃，維持於中團位置下嘗試於直路突圍，未能進入全速狀態下最終以第四衝線。然而由於第一名衝線的川上公主於審議中被指出存在妨礙行為而貶至第十二，情人節獲遞補成為第三，因而其連續五場賽事均跑獲第三的戰績。
其後陣營決定安排其遠征香港出戰香港盃，但於比賽途中未能由中團位置衝出，最終僅跑獲第七的戰績。
競賽生涯 > 5歲

2007年1月出戰京都牝馬錦標作為年度首戰，保持於中後方的有利位置下在最後彎道逐步透出，進入直路後一舉加速超越前方所有賽駒，最終以4馬位的優勢取得時隔1年9個月的勝利。
4月7日出戰阪神牝馬錦標，本次比賽一反以往做法採用前置戰術維持於第三左右，然而於進入直路後稍為力弱，最終被歡欣起舞及Agnes Raspberry超越取得第三。
其後繼續於一哩戰線中征戰，但出戰維多利亞一哩賽未能順利加速僅跑獲第六，於安田紀念更以第十四大敗。
7月其再度進行遠征，目標為美國的奇斯高一哩賽。比賽開始後，其重新採取留後的戰術於隊伍最後方位置等待時機，然而於直路上無法順利衝刺突破，最終以第五落敗。
回國後，其先出戰府中牝馬錦標及在以維多利亞一哩賽作為目標，雖然未能獲勝，但均跑獲第四的入板戰績。
年末出戰三級賽愛知盃，比賽途中以穩定的節奏一直維持於中團有利位置，於直路上成功突圍並開始衝刺，最終以1/2馬位壓贏同樣維持加速的西野掌珠取得第三個分級賽冠軍。
競賽生涯 > 6歲

2006年年初出戰京都金盃及小倉大賞典，但狀態下滑下均以兩位數戰績落敗。
其後，其因為一口馬主俱樂部Carrot Farm Co. Ltd.旗下雌馬必須於6歲3月前退役的規例，在3月5日取消日本中央競馬會的賽駒註冊。
競賽生涯 > 詳細賽績

| 日期 | 舉辦國家/地區 | 馬場 | 距離 | 級別 | 賽事名稱 | 負重 | 騎師 | 馬號 | 出馬 | 名次 | 時間 | 頭馬（二馬） |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| 12/12/2004 |  日本 | 阪神 | 草1600 |  | 2歲新馬 | 54 | 武幸四郎 | 14 | 14 | 1 | 1:36.1 | （Marubutsu Light） |
| 15/1/2005 |  日本 | 京都 | 草1600 |  | 白梅賞 | 54 | 安藤勝己 | 11 | 13 | 1 | 1:36.5 | （Air Messiah） |
| 3/5/2005 |  日本 | 阪神 | 草1600 | GIII | 鬱金香賞 | 54 | 安藤勝己 | 13 | 15 | 7 | 1:36.1 | Eishin Tender |
| 13/3/2005 |  日本 | 阪神 | 草1400 | GII | 雌馬賽 | 54 | 安藤勝己 | 13 | 15 | 4 | 1:21.3 | 萊茵力量 |
| 24/4/2005 |  日本 | 東京 | 草2000 | GII | 花仙錦標 | 54 | 武豐 | 15 | 15 | 1 | 2:01.8 | （Race Pilot） |
| 22/5/2005 |  日本 | 東京 | 草2400 | GI | 優駿牝馬 | 55 | 戴崇謀 | 9 | 18 | 3 | 2:28.9 | 西沙里奧 |
| 5/1/2006 |  日本 | 京都 | 草1600 | GIII | 京都金盃 | 54 | 武豐 | 4 | 16 | 6 | 1:34.4 | Big Planet |
| 29/1/2006 |  日本 | 京都 | 草1600 | GIII | 京都牝馬錦標 | 54 | 武豐 | 6 | 16 | 5 | 1:33.9 | Meine Samantha |
| 12/3/2006 |  日本 | 中山 | 草1800 | GIII | 中山牝馬錦標 | 55 | 岩田康誠 | 4 | 16 | 2 | 1:48.0 | Yamanin Sucre |
| 15/4/2006 |  日本 | 阪神 | 草1600 | GII | 讀賣盃 | 55 | 岩田康誠 | 3 | 11 | 3 | 1:36.5 | 大和主將 |
| 14/5/2006 |  日本 | 東京 | 草1600 | GI | 維多利亞一哩賽 | 55 | 岩田康誠 | 13 | 18 | 3 | 1:34.4 | 隨心起舞 |
| 24/9/2006 |  日本 | 中山 | 草2200 | GII | 產經賞 | 55 | 岩田康誠 | 10 | 15 | 3 | 2:12.1 | 各有千秋 |
| 15/10/2006 |  日本 | 東京 | 草1800 | GIII | 府中牝馬錦標 | 55 | 北村宏司 | 8 | 16 | 3 | 1:47.5 | Daring Heart |
| 12/11/2006 |  日本 | 京都 | 草2200 | GI | 女皇伊利沙伯二世盃 | 56 | 岩田康誠 | 11 | 15 | 3 | 2:11.7 | 火神 |
| 10/12/2006 |  香港 | 沙田 | 草2000 | GI | 香港盃 | 55.5 | 福永祐一 | 11 | 12 | 7 | 2:02.4 | 自豪 |
| 28/1/2007 |  日本 | 京都 | 草1600 | GIII | 京都牝馬錦標 | 54 | 岩田康誠 | 4 | 16 | 1 | 1:33.0 | （Winglet） |
| 7/4/2007 |  日本 | 阪神 | 草1400 | GII | 阪神牝馬錦標 | 55 | 岩田康誠 | 5 | 10 | 3 | 1:21.0 | 歡欣起舞 |
| 13/5/2007 |  日本 | 東京 | 草1600 | JpnI | 維多利亞一哩賽 | 55 | 岩田康誠 | 2 | 18 | 6 | 1:32.8 | 戀曲 |
| 3/6/2007 |  日本 | 東京 | 草1600 | GI | 安田紀念 | 56 | 岩田康誠 | 14 | 18 | 14 | 1:33.3 | 大和主將 |
| 6/7/2007 |  美國 | 聖雅尼塔 | 草1600 | GII | 奇斯高一哩賽 | 55 | 岩田康誠 | 9 | 9 | 5 | 1:33.5 | Lady of Venice |
| 14/10/2007 |  日本 | 東京 | 草1800 | GIII | 府中牝馬錦標 | 55 | 横山典弘 | 7 | 16 | 4 | 1:45.9 | Daring Heart |
| 11/11/2007 |  日本 | 京都 | 草2200 | GI | 女皇伊利沙伯二世盃 | 56 | 武豐 | 13 | 13 | 4 | 2:12.5 | 大和赤驥 |
| 15/12/2007 |  日本 | 中京 | 草2000 | GIII | 愛知盃 | 57 | 李慕華 | 6 | 16 | 1 | 1:58.9 | （西野掌珠） |
| 5/1/2008 |  日本 | 京都 | 草1600 | GIII | 京都金盃 | 56.5 | 武豐 | 4 | 16 | 13 | 1:34.6 | 榮進代表 |
| 9/2/2008 |  日本 | 小倉 | 草1800 | JpnIII | 小倉大賞典 | 56.5 | 李慕華 | 11 | 16 | 10 | 1:48.4 | Asaka Defeat |
退役後

退役後，情人節成為了繁殖雌馬，於北海道安平町北部牧場休養，在2008年進行配種。首匹子嗣Dia de la Bandera於2009年出生，可於2011年出賽。2014年6月15日，Dia de la Madre在人魚錦標取勝，成為首匹勝出分級賽的子嗣。
2020年開始不進行配種，但於2021年7月16日才由繁殖牝馬退役，繼續於北部牧場進行養老生活。
2023年4月10日，其被發現死亡，享年21歲。
退役後 > 主要子嗣 > 分級賽優勝子嗣

2010年生
Dia de la Madre（人魚錦標、府中牝馬錦標、愛知盃）
2013年生
無畏恐龍（京都兩歲錦標、京都大賞典）
退役後 > 詳細繁殖資料

| 數目 | 馬名 | 出生年 | 性別 | 父系 | 練馬師 | 馬主 | 戰績 |
| --- | --- | --- | --- | --- | --- | --- | --- |
| 第一匹 | Dia de la Bandera | 2009年 | 雄 | 吉兆 | 栗東・角居勝彥 →栗東・吉村圭司 →笠松・笹野博司 →高知・那俄性哲也 | Carrot Farm Co. Ltd. →杉浦和也 | 50戰5冠3亞7季（退役） |
| 第二匹 | Dia de la Madre | 2010年 | 雌 | 夏威夷王 | 栗東・角居勝彦 | Carrot Farm Co. Ltd. | 16戰6冠1亞1季（退役・繁殖） 分級賽3勝 |
| 第三匹 | 王之日 | 2011年 | 雄 | 夏威夷王 | 美浦・牧光二 →船橋・川島正一 | Carrot Farm Co. Ltd. | 38戰8冠5亞2季（退役） |
| 第四匹 | San Martin | 2012年 | 雄 | 無敵先鋒 | 美浦・國枝榮 →浦和・水野貴史 →盛岡・齋藤雄一 →名古屋・安部幸夫 | Carrot Farm Co. Ltd. →齊藤秀文 →木村良明 | 44戰10冠1亞1季（退役） |
| 第5匹 | 無畏恐龍 | 2013年 | 雄 | 無敵先鋒 | 栗東・矢作芳人 | Carrot Farm Co. Ltd. | 31戰6冠1亞5季（退役） 分級賽2勝 |
| 第六匹 | Valdes | 2014年 | 雄 | 無敵先鋒 | 美浦・木村哲也 | Carrot Farm Co. Ltd. | 7戰3冠0亞1季（退役） |
| 第七匹 | El Diamante | 2015年 | 雌 | 夏威夷王 | 美浦・國枝榮 | Carrot Farm Co. Ltd. | 5戰0冠1亞2季（退役・繁殖） |
| 第八匹 | Caudillo | 2016年 | 雄 | 夏威夷王 | 美浦・堀宣行 | Carrot Farm Co. Ltd. | 20戰5冠1亞0季 |
| 第九匹 | Great Author | 2017年 | 雄 | 小說名家 | 美浦・堀宣行 | Carrot Farm Co. Ltd. | 17戰3冠2亞1季（退役） |
| 第十匹 | 尊勇神 | 2018年 | 雄 | 龍王 | 美浦・堀宣行 | Carrot Farm Co. Ltd. | 20戰4冠6亞3季（現役） |
| 第十一匹 | 佳日 | 2019年 | 雄 | 無敵先鋒 | 栗東・中内田充正 | Carrot Farm Co. Ltd. | 19戰4冠4亞2季（現役） |
| 第十二匹 | Me Gustas | 2020年 | 雌 | 澤芳 | 栗東・森田直行 | Carrot Farm Co. Ltd. | 5戰0亞0冠1季（退役） |
|  | （未配種） |  |  |  |  |  |  |
血統簡介

父系週日寧靜是美國三冠賽雙冠馬，退役後在日本配種，在日本馬壇相當成功，贏得多項分級賽事，其子嗣贏得巨額獎金，連續12年成為日本冠軍種馬。祖父Halo爲美國賽駒，曾贏得一級賽冠軍，爲美國冠軍種馬。
母系Potrizaris為阿根廷賽駒，生涯戰績優秀，曾勝出一級賽阿根廷打吡及阿根廷橡樹大賽。外祖父Potrillazo為阿根廷馬匹，未有出賽記錄。
血統簡介 > 血統表

| 0 | 1 | 2 | 3 |
| --- | --- | --- | --- |
父線：週日寧靜系（Halo系）
| 種馬  週日寧靜 1986年（棕色） |  Halo 1969年（棕色） |  Hail to Reason |  Turn-to |
| 種馬  週日寧靜 1986年（棕色） |  Halo 1969年（棕色） |  Hail to Reason |  Nothirdchance |
| 種馬  週日寧靜 1986年（棕色） |  Halo 1969年（棕色） |  Cosmah |  Cosmic Bomb |
| 種馬  週日寧靜 1986年（棕色） |  Halo 1969年（棕色） |  Cosmah |  Almahmoud |
| 種馬  週日寧靜 1986年（棕色） |  Wishing Well 1975年（棗色） |  Understanding |  Promised Land |
| 種馬  週日寧靜 1986年（棕色） |  Wishing Well 1975年（棗色） |  Understanding |  Pretty Ways |
| 種馬  週日寧靜 1986年（棕色） |  Wishing Well 1975年（棗色） |  Mountain Flower |  Montparnasse |
| 種馬  週日寧靜 1986年（棕色） |  Wishing Well 1975年（棗色） |  Mountain Flower |  Edelweiss |
| 繁殖雌馬  Potrizaris 1995年（栗色） |  Potrillazo 1982年（棗色） |  Ahmad |  Good Manners |
| 繁殖雌馬  Potrizaris 1995年（栗色） |  Potrillazo 1982年（棗色） |  Ahmad |  Azyade |
| 繁殖雌馬  Potrizaris 1995年（栗色） |  Potrillazo 1982年（棗色） |  Azalee |  Tropical Sun |
| 繁殖雌馬  Potrizaris 1995年（栗色） |  Potrillazo 1982年（棗色） |  Azalee |  Akinos |
| 繁殖雌馬  Potrizaris 1995年（栗色） |  Chaldee 1978年（栗色） |  Banner Sport |  Raise a Native |
| 繁殖雌馬  Potrizaris 1995年（栗色） |  Chaldee 1978年（栗色） |  Banner Sport |  La Dauphine |
| 繁殖雌馬  Potrizaris 1995年（栗色） |  Chaldee 1978年（栗色） |  Gevar |  Right of Way |
| 繁殖雌馬  Potrizaris 1995年（栗色） |  Chaldee 1978年（栗色） |  Gevar |  Zaris |
雌系：號族：2-u
五代內近親交配：無
命名由來

名字Dia de la Novia（ディアデラノビア）於西班牙語中，意思就是「情人節」。
相關條目

三連冠：同主兼同父馬
西沙里奧、出類拔萃、邁向輝煌、實際影響、邁向世界、織女星、神威啟示、新寫實派、醋丈夫、善得福、雍容白荷、金之霸、勝之石、翠綠晶石、實力比試、白朗冰川、賢者、農神節慶、拉丁城市、麗冠花環、遊遍汪洋、樂透心、匯兩川、飄揚青帆、鍵琴高奏、堅韌力、幸運銀幣：同主馬
參考資料

↑  . JBISサーチ. 公益社団法人日本軽種馬協会.   [2024-12-18] （日语）.
↑  . netkeiba.com. 株式会社ネットドリーマーズ.   [2024-12-18] （日语）.
↑  . netkeiba.com. 株式会社ネットドリーマーズ.   [2024-12-18] （日语）.
↑  . netkeiba.com. 株式会社ネットドリーマーズ.   [2024-12-18] （日语）.
外部連結

情人節 netkeiba.com
血統表
死侍：好心沒好報

| 死侍：好心沒好報  |
| --- | --- |
短片中的死侍
基本资料
导演: 大衛·雷奇
编剧:  雷特·瑞斯  保羅·韋尼克 
原著: 《死侍》 羅布·李斐德（英语：） 法比安·尼謝薩（英语：）作品
主演:  萊恩·雷諾斯  史丹·李（線上版本） 
片长: 4分鐘
产地:  美国
语言: 英語  
上映及发行
上映日期: 2017年3月3日（ 美国） 2017年3月4日（線上版本）
发行商: 二十世紀福斯
前作与续作
续作: 《死侍2》
《死侍：好心沒好報》（英語：，又稱）是一部於2017年出品的美國超級英雄短片，劇情改編自漫威漫畫旗下的同名反英雄角色死侍，由二十世紀福斯負責發行，大衛·雷奇執導，雷特·瑞斯與保羅·韋尼克編劇，萊恩·雷諾斯回歸飾演死侍。影片講述韋德·威爾遜試圖從歹徒手中救出一名老人，但決定在此之前先換上他的死侍服裝。
2017年，在電影《羅根》上映前夕，該片的戲院放映片長增加了幾分鐘。片方之所以做出這個改動，是因為電影正片之前加入了一支關於死侍的短片，取代了傳統的片尾彩蛋。該短片名為《死侍：好心沒好報》，拍攝於2016年12月，是2018年電影《死侍2》的一個先導短片，但並非該片的真正預告片。短片以多種方式利用了專屬於死侍的獨特幽默感，例如建基於故事長片無法使用的荒誕設定、打破第四面牆提及《羅根》、調侃DC漫畫的角色超人以及讓史丹·李在片中客串等。
《死侍：好心沒好報》於2017年3月3日連同《羅根》一起上映。隔天，雷諾斯在其YouTube頻道上傳了稍作修改的另一版本。該片作為《死侍2》的先導預告得到了好評，並因為證明了導演雷奇在執導《死侍2》前已經對角色有充分理解而廣受讚譽。影片的幽默手法也被許多影評人著重指出。
劇情

韋德·威爾遜路過一個巷口時看見一名剛購買完雜貨的老人在小巷裡遭到一名持槍的歹徒搶劫。韋德決定施救，於是便模仿超人跑進附近的一座電話亭裡，開始脫下自己的衣服並換上死侍的緊身衣。然而，狹小的空間讓他無法迅速換裝，因而消耗了大量時間。於是他中途停下，打電話給服裝師，不過接聽電話的並不是服裝師本人。他放下電話後繼續換裝，但隨後聽見了槍聲。他驚了一下，緊接著加快了換裝速度。
換好裝之後，韋德衝出了電話亭。史丹·李看見了他並稱讚了他的緊身衣，但韋德認出了史丹並喝斥他閉嘴。韋德繼續以慢動作跑到小巷，卻發現老人已經被槍殺，兇手亦已經逃之夭夭。韋德開始自言自語，說自己決策失當、街角的電話亭像是來自上個時代、換作金鋼狼等其他超級英雄都能快速換裝等。他在小巷地面躺下，把頭靠在老人的腰上，並隨手從老人的購物袋裡拿出了一桶冰淇淋吃。