---
jupytext:
  formats: md:myst
  text_representation:
    extension: .md
    format_name: myst
    format_version: 0.13
kernelspec:
  display_name: Python 3
  language: python
  name: python3
---

# 2회 실험 · 양화사의 순서

```{admonition} 이 실험
:class: seealso

| | |
|---|---|
| **짝 서술** | {doc}`L02` |
| **실험 목록** | 실험 1 (1층) — 순서를 바꾸면 참·거짓이 달라진다 / 실험 2 (3층) — 해집합으로 두 명제를 구분한다 |
```

이번 회차의 대상은 논리 규칙이다. 그림으로 확인할 것이 많지 않으므로 실험은 두 개이며, 둘 다 서술 쪽 (2.5)와 (2.6)의 차이를 눈으로 확인하는 데 쓴다.

```{code-cell} ipython3
:tags: [hide-input]

# 공통 준비 — 색 규약과 한글 글꼴을 맞춘다
import numpy as np
import matplotlib.pyplot as plt
import sympy as sp

from calc_viz import 색
from calc_style import 한글글꼴설정

글꼴 = 한글글꼴설정()   # 돌려주는 값은 실제로 선택된 글꼴 이름이다
```

## 실험 1 (1층) — 순서를 바꾸면 참·거짓이 달라진다

두 명제를 다시 적는다.

$$
\text{(2.5)}\quad \forall x,\; \exists y,\; x < y
\qquad\qquad
\text{(2.6)}\quad \exists y,\; \forall x,\; x < y
$$

왼쪽 그림은 (2.5)이다. $x$가 먼저 주어지고 $y$를 뒤에 고르므로, $y$가 $x$를 따라 움직여도 된다. $y = x + 1$로 잡으면 모든 $x$에서 조건이 성립한다.

오른쪽 그림은 (2.6)이다. $y$를 먼저 하나 고정해야 하므로 $y$는 수평선이 된다. 그 선보다 오른쪽에 있는 $x$들이 모두 반례가 된다.

```{code-cell} ipython3
# [2회] 두 양화사의 순서
# 목적 : "모든 x 에 대하여 어떤 y 가 있다" 와 "어떤 y 가 있어 모든 x 에 대하여" 를 구분한다
# 층  : 1층
# 주의 : 그림은 유한개의 x 만 찍는다. 그림이 증명이 될 수는 없다

x값 = np.linspace(0, 10, 11)
고정y = 6

그림, 축 = plt.subplots(1, 2, figsize=(10, 4.2))

# 왼쪽 : x 마다 y 를 새로 고른다
축[0].plot(x값, x값, "--", color="lightgray", label="y = x")
축[0].plot(x값, x값 + 1, "o-", color=색["하합"], label="고른 y = x + 1")
축[0].set_title("(2.5)  모든 x 에 대하여 x < y 인 y 가 존재한다")
축[0].legend()

# 오른쪽 : y 를 하나 고정한다
축[1].plot(x값, x값, "--", color="lightgray", label="y = x")
축[1].axhline(고정y, color=색["상합"], label=f"고정한 y = {고정y}")
반례 = x값[x값 >= 고정y]
축[1].scatter(반례, [고정y] * len(반례), color=색["차이"], zorder=5,
              label=f"반례가 되는 x ({len(반례)}개)")
축[1].set_title(f"(2.6)  y = {고정y} 을 고정하면 반례가 생긴다")
축[1].legend()

for 축하나 in 축:
    축하나.set_xlabel("x"); 축하나.set_ylabel("y")

plt.tight_layout()
plt.show()

print(f"고정한 y = {고정y} 에 대하여 x < y 를 어기는 x :", 반례)
```

$y$를 다른 값으로 고정해도 결과는 같다. 반례가 되는 $x$는 언제나 남는다.

```{code-cell} ipython3
# [2회] y 를 바꾸어 가며 반례를 센다
# 목적 : 어떤 y 를 고정해도 반례가 사라지지 않음을 확인한다
# 층  : 1층
# 주의 : 유한개의 y 만 시험한다. 이것으로 (2.6) 이 거짓임을 증명한 것은 아니다

for 후보y in (0, 3, 6, 9, 12):
    반례 = x값[x값 >= 후보y]
    상태 = "반례 없음" if len(반례) == 0 else f"반례 {len(반례)}개, 예: x = {반례[0]:.0f}"
    print(f"  y = {후보y:>3} 로 고정 →  {상태}")
```

```{admonition} 확인할 것
:class: tip
1. 왼쪽 그림에서 고른 $y$가 $x$에 따라 달라지는지 확인하자. 오른쪽 그림에서 $y$는 몇 개인가.
2. 두 번째 코드에서 $y$를 12까지 키워도 반례가 남는다. 그런데 $x$의 범위를 $[0,10]$으로 잡았기 때문에 $y = 12$에서는 반례가 사라진다. 실제로 그런지 확인하고, 그것이 (2.6)을 참으로 만들지 못하는 이유를 생각해 보자.
3. 유한개의 $x$를 찍어 본 것으로 (2.5)가 참임을 보였다고 할 수 있는가.
```

## 실험 2 (3층) — 해집합으로 두 명제를 구분한다

`sympy`는 일반적인 양화사 판정을 제공하지 않는다. "$\forall x \exists y$"를 넣으면 참·거짓을 돌려주는 함수는 없다.

대신 **조건을 만족하는 값의 집합**을 구할 수는 있다. 그 집합이 비어 있는지 아닌지를 보고 사람이 결론을 내린다.

```{code-cell} ipython3
# [2회] 양화사를 sympy 로 검사한다
# 목적 : 두 명제의 차이를 해집합으로 확인한다
# 층  : 3층
# 주의 : sympy 는 참·거짓을 판정해 주지 않는다. 해집합을 보고 사람이 판단한다

xs, ys = sp.symbols('x y', real=True)

print("명제 (2.5) : 모든 x 에 대하여 x < y 인 y 가 존재한다")
print("  x 를 먼저 고정했을 때, 조건을 만족하는 y 의 집합 :")
sp.pprint(sp.solveset(xs < ys, ys, domain=sp.S.Reals))
print("  x 가 무엇이든 이 집합은 비어 있지 않다. 따라서 (2.5) 는 참이다.\n")

print("명제 (2.6) : 어떤 y 가 존재하여 모든 x 에 대하여 x < y 이다")
print("  y 를 먼저 고정했을 때, 조건을 어기는 x 의 집합 :")
sp.pprint(sp.solveset(xs >= ys, xs, domain=sp.S.Reals))
print("  y 가 무엇이든 이 집합은 비어 있지 않다. 따라서 (2.6) 은 거짓이다.")
```

두 해집합을 나란히 보면 차이가 드러난다. 첫 번째 집합은 $x$를 포함한 식으로 나오고, 두 번째 집합은 $y$를 포함한 식으로 나온다. **먼저 고정한 것이 뒤에 나오는 집합의 모양을 결정한다.** 이것이 양화사 순서가 하는 일이다.

부정 규칙도 확인해 두자. 서술 쪽 (2.7)은 (2.6)의 부정이 $\forall y\, \exists x,\, x \ge y$라고 말한다. 위 출력의 두 번째 집합이 바로 그 $x$들의 집합이며, 어떤 $y$에 대해서도 비어 있지 않다.

```{code-cell} ipython3
# [2회] 구체적인 y 를 넣어 해집합을 본다
# 목적 : 해집합이 y 에 따라 어떻게 달라지는지, 그러나 언제나 비어 있지 않음을 확인한다
# 층  : 3층
# 주의 : 유한개의 y 를 넣어 본 것이며, 이것 자체가 증명은 아니다

어기는x = sp.solveset(xs >= ys, xs, domain=sp.S.Reals)
for 후보 in (-100, 0, 10**6):
    집합 = 어기는x.subs(ys, 후보)
    print(f"  y = {후보:>8} →  반례 x 의 집합 = {집합},  공집합인가? {집합.is_empty}")
```

```{admonition} 확인할 것
:class: tip
1. 명제 (2.5)에서 $y$의 해집합이 $x$에 의존하는지 확인하자.
2. 명제 (2.6)에서 반례가 되는 $x$의 집합이 항상 비어 있지 않은지 확인하자.
3. 두 경우에 무엇을 먼저 고정했는지 비교하자.
```

```{admonition} 판정은 자동화되지 않는다
:class: warning

`sympy`는 해집합을 계산해 줄 뿐이고, "그러므로 명제가 참이다"라는 결론은 내려 주지 않는다. 위 코드에서도 결론 문장은 사람이 미리 적어 둔 것이다.

`solveset`이 돌려준 집합이 비어 있지 않다는 것을 확인했다고 해서 전칭명제가 증명된 것도 아니다. 실제로 확인한 것은 유한개의 값뿐이다. 논증은 여전히 손으로 해야 한다.
```

```{admonition} 짝이 되는 서술
:class: note
{doc}`L02`
```