update: logic-1

Author: Rratic

content/posts/logic_1.md

@@ -1,6 +1,7 @@
 +++
 title = "【逻辑学】简单的形式语言及可靠性、完全性证明"
 date = 2026-03-10
+updated = 2026-03-18
 
 [extra]
 math = true
@@ -92,7 +93,7 @@ $$\frac{\text{Some } X \text{ is } Y}{\text{Some } X \text{ is } X} \mathrm{Ex}$
 $$\mathcal{M} \models \text{Some } X \text{ is } Y \iff I(X) \cap I(Y) \neq \emptyset$$
 
 {% admonition(type="question", title="习题") %}
-在 $\mathrm{Sys}_{\text{some}}^S$ 中分别用树形和线性推演证明 Some $X$ is $Y$ 可以推出 Some $Y$ is $Y$.
+在 $\mathrm{Sys}_{\text{some}}^S$ 中分别用树形和线性推演证明 $\text{Some } X \text{ is } Y$ 可以推出 $\text{Some } Y \text{ is } Y$.
 {% end %}
 
 主要是记住格式：
@@ -135,6 +136,34 @@ $$
 
 $$\frac{\text{Some } X \text{ is } Y \quad \text{All } Y \text{ are } Z}{\text{Some } X \text{ is } Z} \mathrm{Unnamed}$$
 
-其完全性确实不容易证（甚至并且很不直观，我看着它都无法保证提供了足够的规则），先空着。
+<div id="anchor"></div>
 
-{{ todo() }}
+其完全性确实不容易证（甚至并且很不直观，我看着它都无法保证提供了足够的规则）。
+
+实际上会发现：我们无法通过构造单个典范模型说明这一点（否则，如果 $X$ 不满足 $\text{Some } X \text{ is } X$, 则 $I(X) = \emptyset$, 从而 $\text{All } X \text{ is } Y$ 总是成立）。
+
+这里回答一个问题：从语义上说，如果 $A$ 不满足 $\text{Some } A \text{ is } A$, 那么所有的 $\text{All } A \text{ is } B$ 总是成立，也就是说，孤零零两个点 $X, Y$ 之间没有任何关系（只有 $\text{All}$ 自己是自己）不是合法的最终图景，是否说明上述五条规则不是完全的？答案是否定的，回到定义会发现，我们定义的不是“最终图景”这样的东西。我们说在某个前提下可以推演出某个结果，而没有说“某个前提不成立”下可以推出哪个结果。语言中也没有 $\text{Not}$ 之类的句子来间接表达这一点。在孤零零两个点例子中，我们确实不能推出 $\text{Some } X \text{ is } Y$, 因为也有可能是另一种情况。而如果你想问：“我们知道这个事实存在，但是无法写成规则，会不会丢失信息？”，会发现最终自然的要求就是完全性。
+
+考虑分情况讨论 $\varphi$ 是 $\text{All}$-句子和 $\text{Some}$-句子两种情形（来自助教的提示）。回顾定义，只需要分别构造模型 $\mathcal{M}$ 满足：
+
+$$\mathcal{M} \models \Gamma \tag{1}$$
+
+$$\mathcal{M} \models \varphi \iff \Gamma \vdash \varphi \tag{2}$$
+
+对于 $\text{All}$-句子，考虑我们之前构造的 $\mathrm{Sys}_{\text{all}}^S$ 的典范模型 $\mathcal{M}'$, 现在在对象域中加入 $\star$, 并在所有 $I(X)$ 中添上 $\star$. 这会使得所有 $\text{Some}$-句子都成立，从而 (1) 成立；同时 (2) 成立。
+
+对于 $\text{Some}$-句子，使用图论直观，考虑对象域为 $O = \\{w_{X, Y} | \Gamma \vdash \text{Some } X \text{ is } Y \\}$ 其中 $w_{X,Y} = w_{Y,X}$, 解释函数 $I(X) = \\{w_{Y, Z} \in O | \text{All } X \text{ are } Y\\}$. 读者可验证 (1) (2) 成立。注意其中 $\text{Ex}$ 与 $\text{Unnamed}$ 规则的混合使用。
+
+---
+
+特别地，我的同学 [@Kavod](https://space.bilibili.com/1861613068) 提出了对 $\varphi: \text{Some } X \text{ is } Y$ 构造反模型的方法（如果 $\varphi$ 不成立，有一个模型使 $I(X), I(Y)$ 无交）；采取图论视角：
+1. 取 $\mathcal{M} \models \Gamma$
+2. 令 $N(X) = \\{Z | \Gamma \vdash \text{All } Z \text{ are } X\\}$, 则 $N(X) \cap N(Y)$ 中的元素不能有 $\text{Some}$-边，语义上它们都是空集
+3. 只考虑 $X \notin N(Y), Y \notin N(X)$ 的情形，并略去不看 $N(X) \cap N(Y)$
+4. 我们将 $N(X) \setminus N(Y)$ 捏成 $X$, 将 $N(Y) \setminus N(X)$ 捏成 $Y$: 在新的图中，如果原本存在点 $Z \in N(X) \setminus N(Y)$ 满足 $\text{All } Z \text{ are } W$, 则加上边 $\text{All } X \text{ are } W$
+5. 新的图有模型 $\mathcal{M}_0$, 另外 $\mathcal{M}$ 诱导了 $N(X) \setminus N(Y)$ 上的模型 $\mathcal{M}_X$ 和 $N(Y) \setminus N(X)$ 上的模型 $\mathcal{M}_Y$, 让它们使用不同的集合元素
+6. 现在，对一个 $Z$, $I(Z)$ 初始取为 $\mathcal{M}_0$ 中的，如果 $Z \in N(X)$ 再并上 $\mathcal{M}_X$ 中的，如果 $Z \in N(Y)$ 再并上 $\mathcal{M}_Y$ 中的
+
+这里需要解释为什么总是可以在一组前提集上构造模型，特别是对于 $\mathcal{M} _0$ 的构造，要求对 $X, Y$ 满足没有 $\text{All } Z$ 是它时 $I(X), I(Y)$ 无交。我的想法是，对于有限情形，略去不看 $\text{All}$-有向边成圈的情形，此时先赋值 $I(Z) = \emptyset$, 然后对所有 $\text{Some}$-无向边，填入新元 $\star _w$ 然后向上传递，可以在有限步停止。对于一般的可数情形，考虑把一些名字捏成相同的并 $\bigcup _{\text{finite } S} \\{\star _{w _S}\\}$, 按照某个点是否包含某个 $\star _w$ 看成赋值，使用紧致性定理的方法（大意是归纳，总有一半满足对所有有限子集存在赋值成立）。
+
+以上过程省略了大量细节，暂时没有完全验证。