Question

我正在学习用于自动检查证明的 lean/mathlib 系统，并且真正让我感到惊讶的是，为了证明唯一存在性，那里的结构迫使我们分别证明这些属性：

独特性
存在

当然，独特性已经意味着存在了？

例子

考虑条件 $x - 2 = 3.$ x-2=3.

首先，我只是尝试 $x = 5$ x=5不用担心如何找到这个“证人”。因为 $x = 5 ⟹ x - 2 = 5 - 2 = 3,$ x=5 \implies x-2=5-2=3,我已经证明了这个解决方案满足条件。我可以看出，这表明存在一个解决方案，但并不表明没有其他解决方案。

接下来，我对给定的条件应用一系列代数运算，可能会得出一组解决方案。我得出一个解决方案： $x - 2 = 3 ⟹ x - 2 + 2 = 3 + 2 ⟹ x = 5.$ x-2=3 \implies x-2+2=3+2 \implies x=5.如果条件是二次的，那么代数运算将会让我得到两个解决方案。

因此，我已经证明该条件导致唯一的解决方案（自动证明存在性），并且我不需要分别证明存在性和唯一性。

对于这个例子，我是否正确地认为证明存在是多余的？
如果是这样，那么这仅适用于这种简单的情况吗？

我认为@Bram28 的回答很正确。存在意味着 $\geq 1$ \ge 1例如，独特性意味着 $\leq 1$ \le 1实例。 —

Answer 1

我认为“唯一性”这个概念有点模棱两可。有些人会说唯一性意味着“恰好一个”，而另一些人会说它意味着“最多一个”。在数学中，我们通常指的是后者，但我认为我们的直觉会倾向于前者。但是，是的，如果是后者，那么你仍然需要证明存在性，因为“最多一个”与根本没有解是一致的。

Answer 2

考虑以下陈述：

x - 2 = 3 ⟹ x = 5。

x – 2 = 3 \implies x = 5.

这证明了唯一性，但没有证明存在性。也就是说，你已经证明了，如果存在 $x - 2 = 3,$ ~x-2 = 3,~它一定是集合中的某个元素 $S = {5} .$ ~S = \{5\}.~

所以，你已经证明的是，如果存在一个解决方案，那么它一定是唯一的，因为它一定是集合的一个元素 $S,$ ~S,~只有一个元素。

现在考虑这个说法：

x = 5 ⟹ x - 2 = 3。

x = 5 \implies x – 2 = 3.

这个陈述证明了存在。也就是说，它证明至少存在一个值，即 $x = 5,$ ~x = 5,~满足方程 $x - 2 = 3.$ ~x-2 = 3.~ 然而，该声明并未表明 $x = 5$ ~x = 5~是唯一的。因此，该陈述仅证明至少存在一个解决方案。

感谢您的帮助。为什么第一部分没有证明存在？请原谅我使用非数学语言，但我可以用眼睛看到解决方案存在，它是 $x = 5$ x=5，RHS $x - 2 = 3 ⟹ x = 5$ x-2=3 \implies x=5。我理解这句话错了吗？有没有一种情况会导致我最终 $x = k$ x=k但解的数量严格小于一，即零而不是一？ — 
@Penelope 考虑一下真实的陈述 $(x - 2)^{2} < 0 ⟹ x = 5.$ ~(x – 2)^2 < 0 \implies x = 5.~ — 
一个典型的例子是 $\sqrt{x} = - 1$ \sqrt{x} = -1。如果对两边求平方，则得到 $x = 1$ x=1，但这不是原始方程的解。 —

Answer 3

您的特定示例很特殊，因为线性方程总是有一个（唯一）答案。但当然，事情可能更复杂：

如果 $x$ x是一个实数，它有一个乘法逆元，该逆元是唯一的。

假设 $y$ y和 $z$ z分别是 $x$ x。然后

是 = y \cdot 1 = y \cdot (x z) = （ y x ） \cdotz ​ = 1 \cdot z = z ，

y = y \cdot 1 = y \cdot (xz) = (yx)\cdot z = 1 \cdot z = z,以便

是 = z ，

y = z,但前提是我们已经知道 $1$ 1是乘法恒等式，并且实数乘法是结合的。

但当然，并非每个实数都有乘法逆元。

很多时候，存在性证明有不可逆的步骤（或者至少，步骤不能以独特的方式逆转）。你如何区分你的步骤，表明 $x - 2 = 3$ x-2=3有一个唯一的解决方案，并且 $x^{2} = 9$ x^2 = 9 不是吗？好吧，我们都知道求平方根会带来复杂性（即它们不是精确可逆的），但一般来说，许多问题都是通过不可逆过程解决的。显示 $x^{2} = 9$ x^2 = 9有一个解决方案只需要我展示 $x = 3$ x = 3。但当然，我们知道解决方案不是唯一的。

作为更“常规”的代数情况，考虑两个方程组

x + y x - y = 5 = 3

\begin{align*}
x + y &= 5\\
x-y &= 3\\
\end{align*}只有解决方案 $x = 4, y = 1$ x = 4, y = 1。

然而，系统

x + y 2 x + 2 y = 5 = 10

\begin{align*}
x + y &= 5\\
2x+2y &= 10\\
\end{align*}还有 $x = 4, y = 1$ x = 4, y = 1作为一个解决方案，以及无数其他解决方案。解决第一个系统的人可能会选择一条恰好同时证明存在性和唯一性的解决方案路径。然而，我可以通过简单地展示 $(4, 1)$ (4,1)作为解决方案，然后声称由于系统定义的线具有不同的斜率，它们必须只在一个点相交。这与通过更典型的代数推导出存在性和唯一性一样有效 $(4, 1)$ (4,1)是唯一的解决方案。

Answer 4

为了证明唯一存在性，那里的结构迫使我们分别证明这些属性：

独特性

存在

更准确地说，属性的结合

最多一个；即不超过一个（“如果 x 存在，那么就有一个唯一的 x”）
至少一个；即存在

等同于（并隐含）属性

恰好一个，即（“唯一存在”基本上就是这个意思）。

当然，独特性已经意味着存在了？

是的。

例子

考虑条件 $x - 2 = 3.$ x-2=3.

我得出一个解决方案： $x - 2 = 3 ⟹ x - 2 + 2 = 3 + 2 ⟹ x = 5.$ x-2=3 \implies x-2+2=3+2 \implies x=5.如果条件是二次的，那么代数运算将会让我得到两个解决方案。

处理二次方程最多会产生两个（实数）解（不一定完全是两个）。无论如何，在这里，您已经证明了最多只有一个解（属性 1：如果存在解，则存在唯一解）。请注意，此步骤本身仅表明 $x = 5$ x=5是一个，但它可能会被证明是无关的，在这种情况下给定的条件实际上没有解。

自从 $x = 5 ⟹ x - 2 = 5 - 2 = 3,$ x=5 \implies x-2=5-2=3,我已经证明了这个解决方案满足条件。我可以看出，这表明存在一个解决方案

这里，你已经证明至少有一个解决方案（属性 2：存在一个解决方案）。

因此，我已经证明该条件导致唯一的解决方案（自动证明存在性），并且我不需要分别证明存在性和唯一性。

更简单地说：您前面的两个步骤加在一起得出了所需的结论，即只有一个解决方案（有一个唯一的解决方案）。

对于这个例子，我是否正确地认为证明存在是多余的？

您的独特性证明已经包含存在性的证明。

如果是这样，那么这仅适用于这种简单的情况吗？

不。

Answer 5

当然，独特性已经意味着存在了？

你可以拥有唯一性而不存在。请考虑以下示例：

$X = {0, 1, 2}$ X=\{0,1,2\}

$f = {(1, 0), (2, 1)}$ f=\{(1,0), (2,1)\}

通过检查，我们有唯一性：

$\forall a, b, c \in X : [(a, b) \in f \land (a, c) \in f ⟹ b = c]$ \forall a,b,c \in X:[(a,b)\in f~ \land ~(a,c)\in f \implies b=c]

然而，我们并不存在：

$\neg \forall a \in X : \exists b \in X : (a, b) \in f$ \neg \forall a\in X: \exists b\in X: (a,b) \in f~~~~~

$a = 0$ a=0~反例

理解“唯一存在”证明的逻辑

5 个回答
5

理解“唯一存在”证明的逻辑

5 个回答 5

5 个回答
5