1.4 Formal Proof
논리학에는 한 statement가 참이라는 것을 다른 statement들로부터 추론할 수 있는 규칙이 존재한다.
Proof system(증명 체계)은 derivation(유도)에 관한 기본 규칙들의 집합으로 구성되어 있다. 이 규칙을 이용하면 formula들의 집합으로부터 formula를 유도해 낼 수 있다. $\mathcal{F}$로부터 $G$를 추론하는데 몇 가지 step이 소요된다고 하자. 각 step은 기본 규칙들 중 하나를 적용한 셈이다. 이러한 step들의 목록이 $\mathcal{F}$로부터 $G$의 formal proof(형식 증명)를 형성한다.
우리의 proof system은 sound(건전)해야 한다.
Soundness
위 성질은 formal proof의 개념과 consequence의 개념이 어떻게 연결되는지를 알려준다. 만일 proof system이 sound하면, 이것이 진리표를 대신해 $G$가 $\mathcal{F}$의 consequence인지 아닌지를 판단할 대체 수단이 된다.
우리가 사용할 proof system의 기본 규칙들을 나열하자. Formal proof system의 목표는 빈틈없는 추론 과정을 만들어내는 것. 이상적으로는 우리의 사고 과정을 완전히 대체할 수 있어야 한다.1
Basic Rules for Proof system
대다수의 규칙들은 꽤 자명하다.
예를 들어, $F$와 $G$가 $\mathcal{F}$로부터 유도될 수 있다면, $F \wedge G$도 $\mathcal{F}$로부터 유도될 수 있다. 이 규칙을 $``\wedge - \textrm{Introduction}”$이라고 한다. “$G$가 $\mathcal{F}$로부터 유도될 수 있다”를 $\mathcal{F} \vdash G$로 나타내면, 위는 다음과 같이 쓸 수 있다:
\[\textrm{If } \mathcal{F} \vdash F \textrm{ and }\mathcal{F} \vdash G \textrm{, then }\mathcal{F} \vdash (F \wedge G)\]
| Premise(전제) | Conclusion(결론) | Name |
|---|---|---|
| $G\textrm{ is in }\mathcal{F}$ | $\mathcal{F} \vdash G$ | $\textrm{Assumption}$ |
| $\mathcal{F} \vdash G \textrm{ and } \mathcal{F} \subset\mathcal{F’}$ | $\mathcal{F}’ \vdash G$ | $\textrm{Monotonicity}$ |
| $\mathcal{F} \vdash G$ | $\mathcal{F} \vdash \neg \neg G$ | $\textrm{Double negation}$ |
| $\mathcal{F} \vdash F,\mathcal{F} \vdash G$ | $\mathcal{F} \vdash (F\wedge G)$ | $\wedge - \textrm{Introduction}$ |
| $\mathcal{F} \vdash (F\wedge G)$ | $\mathcal{F} \vdash F$ | $\wedge - \textrm{Elimination}$ |
| $\mathcal{F} \vdash (F\wedge G)$ | $\mathcal{F} \vdash (G\wedge F)$ | $\wedge - \textrm{Symmetry}$ |
| $\mathcal{F} \vdash F$ | $\mathcal{F} \vdash (F\vee G)$ | $\vee - \textrm{Introduction}$ |
| $\mathcal{F} \vdash (F\vee G),$ $\mathcal{F} \cup \{F\} \vdash H, \mathcal{F} \cup \{G\} \vdash H$ | $\mathcal{F} \vdash H$ | $\vee - \textrm{Elimination}$ |
| $\mathcal{F} \vdash (F\vee G)$ | $\mathcal{F} \vdash (G\vee F)$ | $\vee - \textrm{Symmetry}$ |
| $\mathcal{F} \cup \{F\} \vdash G$ | $\mathcal{F} \vdash (F\rightarrow G)$ | $\rightarrow- \textrm{Introduction}$ |
| $\mathcal{F} \vdash (F\rightarrow G), \mathcal{F} \vdash F$ | $\mathcal{F} \vdash G$ | $\rightarrow- \textrm{Elimination}$ |
| $\mathcal{F} \vdash F$ | $\mathcal{F} \vdash (F)$ | $(,)- \textrm{Introduction}$ |
| $\mathcal{F} \vdash (F)$ | $\mathcal{F} \vdash F$ | $(,)- \textrm{Elimination}$ |
| $\mathcal{F} \vdash ((F\wedge G)\wedge H)$ | $\mathcal{F} \vdash (F\wedge G\wedge H)$ | $\wedge - \textrm{Parentheses rule}$ |
| $\mathcal{F} \vdash ((F\vee G)\vee H)$ | $\mathcal{F} \vdash (F\vee G\vee H)$ | $\vee- \textrm{Parentheses rule}$ |
| Rules | Name |
|---|---|
| $\mathcal{F} \vdash (F\vee G)\textrm{ iff } \mathcal{F} \vdash \neg (\neg F\wedge \neg G)$ | $\vee - \textrm{Definition}$ |
| $\mathcal{F} \vdash (F\rightarrow G)\textrm{ iff } \mathcal{F} \vdash (\neg F\vee G)$ | $\rightarrow- \textrm{Definition}$ |
| $\mathcal{F} \vdash (F\leftrightarrow G)\textrm{ iff both }\mathcal{F} \vdash (F\rightarrow G)\textrm{ and }\mathcal{F} \vdash (G\rightarrow F)$ | $\leftrightarrow- \textrm{Definition}$ |
위 규칙들은 너무 많다. $\vee$는 $\neg$와 $\wedge$로부터 유도되므로, $\vee - \textrm{Symmetry}$는 $\wedge - \textrm{Symmetry}$로부터 바로 따라온다. 사실상 필요한 규칙들은 훨씬 적다. 반면에 어떤 면에서는 이 목록은 많이 부족한데, 위 규칙들로부터 유도되는 다른 규칙들도 얼마든지 있기 때문.
이제 “formal proof”를 정의.
Definition 1.4.1
$\mathcal{X}$를 formula들의 집합, $Y$를 formula라고 하자.
Propositional logic의 formal proof(형식 증명)란 $``\mathcal{X} \vdash Y”$ 형태의 statement들의 finite sequence를 말한다. 이때 각 statement들은 두 Table 중 하나를 따른다. 만약 statement $\mathcal{F} \vdash G$로 결론지어지는 formal proof가 존재하면, $G$는 $\mathcal{F}$로부터 유도된다(derived)고 한다.
Example 1.4.2
$\mathcal{H}=\{(\neg A \vee B), (\neg A \vee C), (A, \vee \neg D)\}$라고 하자.
$\mathcal{H}$로부터 formula $D \rightarrow (A \wedge B \wedge C)$를 유도하자.
| Statement | Justification |
|---|---|
| 1. $\mathcal{H} \cup \{D\} \vdash D$ | $\textrm{Assumption}$ |
| 2. $\mathcal{H} \cup \{D\} \vdash (A \vee \neg D)$ | $\textrm{Assumption}$ |
| 3. $\mathcal{H} \cup \{D\} \vdash (\neg D \vee A)$ | $\vee - \textrm{Symmetry}$ applied to 2 |
| 4. $\mathcal{H} \cup \{D\} \vdash (D \rightarrow A)$ | $\rightarrow- \textrm{Definition}$ applied to 3 |
| 5. $\mathcal{H} \cup \{D\} \vdash A$ | $\rightarrow- \textrm{Elimination}$ applied to 4 and 1 |
| 6. $\mathcal{H} \cup \{D\} \vdash (\neg A \vee B)$ | $\textrm{Assumption}$ |
| 7. $\mathcal{H} \cup \{D\} \vdash (A \rightarrow B)$ | $\rightarrow- \textrm{Definition}$ applied to 6 |
| 8. $\mathcal{H} \cup \{D\} \vdash B$ | $\rightarrow- \textrm{Elimination}$ applied to 7 and 5 |
| 9. $\mathcal{H} \cup \{D\} \vdash (\neg A \vee C)$ | $\textrm{Assumption}$ |
| 10. $\mathcal{H} \cup \{D\} \vdash (A \rightarrow C)$ | $\rightarrow- \textrm{Definition}$ applied to 9 |
| 11. $\mathcal{H} \cup \{D\} \vdash C$ | $\rightarrow- \textrm{Elimination}$ applied to 10 and 5 |
| 12. $\mathcal{H} \cup \{D\} \vdash (A \wedge B)$ | $\wedge - \textrm{Introduction}$ applied to 5 and 8 |
| 13. $\mathcal{H} \cup \{D\} \vdash ((A \wedge B) \wedge C)$ | $\wedge - \textrm{Introduction}$ applied to 12 and 11 |
| 14. $\mathcal{H} \cup \{D\} \vdash (A \wedge B \wedge C)$ | $\wedge - \textrm{Parentheses rule}$ applied to 13 |
| 15. $\mathcal{H} \vdash (D \rightarrow (A \wedge B \wedge C))$ | $\rightarrow- \textrm{Introduction}$ applied to 14 |
| 16. $\mathcal{H} \vdash D \rightarrow (A \wedge B \wedge C)$ | $(,)- \textrm{Elimination}$ applied to 15 |
별로 복잡하지도 않은 사실을 설명하는데 아주 복잡해 보인다! 그렇지만 증명을 한 줄 한 줄 읽어보면 단순한 사실을 말하고 있을 뿐이다. 몇 가지 추가 규칙을 도입해서 간결하게 만들자.
Additional Rules for Derivations
예를 들어, Example. 1.4.2에서 $\rightarrow$의 도입은 단지 $\rightarrow$의 소거를 위해서만 쓰였다. 대신에 다음 규칙을 따로 증명하자.
Example 1.4.3 $\vee$ - Modus Ponens 2
$\qquad\textrm{Premise : }\mathcal{F} \vdash (\neg F \vee G), \mathcal{F} \vdash F$
$\qquad\textrm{Conclusion : }\mathcal{F} \vdash G$
| Statement | Justification |
|---|---|
| 1. $\mathcal{F} \vdash F$ | $\textrm{Premise}$ |
| 2. $\mathcal{F} \vdash (\neg F \wedge G)$ | $\textrm{Premise}$ |
| 3. $\mathcal{F} \vdash (F \rightarrow G)$ | $\rightarrow- \textrm{Definition}$ applied to 2 |
| 4. $\mathcal{F} \vdash G$ | $\rightarrow- \textrm{Elimination}$ applied to 3 and 1 |
위 과정을 3번 반복한 것이 Example. 1.4.2의 증명. 이 4줄짜리 증명을 하나의 subroutine으로 간주할 수 있다. 이하는 증명을 간소화시키는 다른 규칙들.
Example 1.4.4 [Tautology Rule]
이 규칙은 임의의 formula $G$에 대해 $(\neg G \vee G)$가 임의의 formula들의 집합으로부터 유도된다는 것을 말한다.
$\qquad\textrm{Premise : None}$
$\qquad\textrm{Conclusion : }\mathcal{F} \vdash (\neg G \vee G)$
| Statement | Justification |
|---|---|
| 1. $\mathcal{F} \cup \{G\} \vdash G$ | $\textrm{Assumption}$ |
| 2. $\mathcal{F} \vdash (G \rightarrow G)$ | $\rightarrow- \textrm{Introduction}$ applied to 1 |
| 3. $\mathcal{F} \vdash (\neg G \vee G)$ | $\rightarrow- \textrm{Definition}$ applied to 2 |
Example 1.4.5 [Contradiction Rule]
이 규칙은 임의의 formula $G$가 contradiction $(F \wedge \neg F)$로부터 유도된다는 것을 말한다.
$\qquad\textrm{Premise : }\mathcal{F} \vdash (F \wedge \neg F)$
$\qquad\textrm{Conclusion : }\mathcal{F} \vdash G$
| Statement | Justification |
|---|---|
| 1. $\mathcal{F} \vdash (F \wedge \neg F)$ | $\textrm{Assumption}$ |
| 2. $\mathcal{F} \vdash (\neg F\wedge F)$ | $\wedge - \textrm{Symmetry}$ applied to 1 |
| 3. $\mathcal{F} \vdash \neg F$ | $\wedge - \textrm{Elimination}$ applied to 2 |
| 4. $\mathcal{F} \vdash (\neg F\vee G)$ | $\vee- \textrm{Introduction}$ applied to 3 |
| 5. $\mathcal{F} \vdash F$ | $\wedge - \textrm{Elimination}$ applied to 1 |
| 6. $\mathcal{F} \vdash G$ | $\vee- \textrm{Modus Ponens}$ applied to 4 and 5 |
Example 1.4.6 [Contrapositive]
이 규칙은 $p$ implies $q$라면, $\neg q$ implies $\neg p$라는 것을 말해 준다.
$\qquad\textrm{Premise : }\mathcal{F} \cup \{F\} \vdash G$
$\qquad\textrm{Conclusion : }\mathcal{F} \cup \{\neg G\} \vdash \neg F$
| Statement | Justification |
|---|---|
| 1. $\mathcal{F} \cup \{F\} \vdash G$ | $\textrm{Premise}$ |
| 2. $\mathcal{F} \cup \{F\} \vdash \neg \neg G$ | $\textrm{Double negation}$ applied to 1 |
| 3. $\mathcal{F} \vdash (F \rightarrow \neg \neg G)$ | $\rightarrow- \textrm{Introduction}$ applied to 2 |
| 4. $\mathcal{F} \vdash (\neg F \vee \neg \neg G)$ | $\rightarrow- \textrm{Definition}$ applied to 3 |
| 5. $\mathcal{F} \vdash (\neg \neg G \vee \neg F)$ | $\wedge - \textrm{Symmetry}$ applied to 4 |
| 6. $\mathcal{F} \vdash (\neg G \rightarrow \neg F)$ | $\rightarrow- \textrm{Definition}$ applied to 5 |
| 7. $\mathcal{F} \cup \{\neg G\} \vdash (\neg G \rightarrow \neg F)$ | $\textrm{Monotonicity}$ applied to 6 |
| 8. $\mathcal{F} \cup \{\neg G\} \vdash \neg G$ | $\textrm{Assumption}$ |
| 9. $\mathcal{F} \cup \{\neg G\} \vdash \neg F$ | $\rightarrow- \textrm{Elimination}$ applied to 6 and 8 |
Example 1.4.7 [Proof by Cases]
$\qquad\textrm{Premise : }\mathcal{F} \cup \{F\} \vdash G, \mathcal{F} \cup \{\neg F\} \vdash G$
$\qquad\textrm{Conclusion : }\mathcal{F} \vdash G$
| Statement | Justification |
|---|---|
| 1. $\mathcal{F} \cup \{F\} \vdash G$ | $\textrm{Premise}$ |
| 2. $\mathcal{F} \cup \{\neg F\} \vdash G$ | $\textrm{Premise}$ |
| 3. $\mathcal{F} \vdash (\neg F \vee F)$ | $\textrm{Tautology rule}$ |
| 4. $\mathcal{F} \vdash G$ | $\vee- \textrm{Elimination}$ applied to 3, 2 and 1 |
Example 1.4.8 [Proof by Contradiction]
본질적으로는 Example 1.4.7, proof by case의 contrapositive version.
$\qquad\textrm{Premise : }\mathcal{F} \cup \{F\} \vdash G, \mathcal{F} \cup \{F\} \vdash \neg G$
$\qquad\textrm{Conclusion : }\mathcal{F} \vdash \neg F$
| Statement | Justification |
|---|---|
| 1. $\mathcal{F} \cup \{F\} \vdash G$ | $\textrm{Premise}$ |
| 2. $\mathcal{F} \cup \{\neg G\} \vdash \neg F$ | $\textrm{Contraposition}$ applied to 1 |
| 3. $\mathcal{F} \cup \{F\} \vdash \neg G$ | $\textrm{Premise}$ |
| 4. $\mathcal{F} \cup \{\neg \neg G\} \vdash \neg F$ | $\textrm{Contraposition}$ applied to 3 |
| 5. $\mathcal{F} \vdash \neg F$ | $\textrm{Proof by Cases}$ applied to 2 and 4 |
여기까지 정립된 규칙들은 이후의 증명 내에서 statement를 정당화시킬 때 사용된다. 규칙이 “정립되었다’는 말은, 만약 Table의 규칙들이 참이라면, 위 새로운 규칙들도 참이라는 뜻이다. 이를 보이기 위해서 우리는 이 proof system이 sound함을 보여야 한다.
Soundness of Proof system
Soundness를 다시 쓰자. 만약 $G$가 $\mathcal{F}$로부터 유도될 수 있다면, $G$는 $\mathcal{F}$의 consequence이다.3
Theorem 1.4.9 [Soundness]
$\mathcal{F} \vdash G$이면, $\mathcal{F} \models G$이다.
Proof.
만약 $\mathcal{F} \vdash G$이면, $\mathcal{F} \vdash G$를 conclusion으로 갖는 formal proof가 존재할 것이다. 이 증명의 각 row에는 Table의 규칙으로부터 정당화된 $\mathcal{X} \vdash Y$ 꼴의 statement가 들어 있다. 증명의 각 row에서 $\mathcal{X} \vdash Y$이면 $\mathcal{X} \models Y$임을 보이고자 한다. 즉, 각 규칙들을 모조리 하나씩 확인하면 된다. 여기서는 세 개, Assumption, $\wedge$-Elmination, $\rightarrow$-Introduction만 확인하자.
[Assumption] 이 규칙의 conclusion은 $\mathcal{F} \vdash G$. 이를 premise로 두고, $\mathcal{F} \models G$를 보이려 한다. Premise는 $G$가 $\mathcal{F}$ 안에 있음을 말해 주므로, 만약 $\mathcal{A}$가 $\mathcal{F}$를 model한다면, $\mathcal{A}$는 $G$ 역시 model한다.
[$\wedge$-Elmination] $\mathcal{F} \vdash (F \wedge G)$이면, $\mathcal{F} \vdash F$이다. 이로부터 [$\mathcal{F} \models (F \wedge G)$이면, $\mathcal{F} \models F$]를 보이자. 즉, $F$가 $(F \wedge G)의 consequence임을 보인다. 이는 진리표로부터,
| $F$ | $G$ | $(F\wedge G)$ | $(F\wedge G) \rightarrow F$ |
|---|---|---|---|
| $0$ | $0$ | $0$ | $1$ |
| $0$ | $1$ | $0$ | $1$ |
| $1$ | $0$ | $0$ | $1$ |
| $1$ | $1$ | $1$ | $1$ |
[$\rightarrow$-Introduction] $\mathcal{F} \cup \{F\} \vdash G$이면, $\mathcal{F} \vdash (F \rightarrow G)$이다. 이로부터 $\mathcal{F} \cup \{F\} \models G$를 가정, 임의의 assignment $\mathcal{A}$에 대해, 만약 $\mathcal{A} \models \mathcal{F}$이면 $\mathcal{A} \models (F \rightarrow G)$를 보이면 된다.
따라서, $\mathcal{A} \models \mathcal{F}$이고 $\mathcal{A}(F)$가 정의되었다고 하자. 만약 $\mathcal{A}(F)=0$이면, $\mathcal{A} \models (F \rightarrow G)$는 $\mathcal{A}(G)$의 값과 관계없이 참. 반면 만약 $\mathcal{A}(F)=1$이면, $\mathcal{A} \models \mathcal{F} \cup \{F\}$이다. 가정으로부터, $\mathcal{A} \models G$이다. 어느 경우에서도 $\mathcal{A} \models (F \rightarrow G)$이고, $\mathcal{A}$는 임의로 결정한 ($\mathcal{F}$를 model하는) assignment이므로, $\mathcal{F} \models (F \rightarrow G)$를 얻는다.
근본적으로, 우리는 $\vdash$가 $\models$로 대체될 수 있음을 보여야 한다. 대다수의 규칙들은 진리표를 계산할 필요가 있으며, 아무것도 보일 게 없는 규칙들도 있다. 첫 번째 표의 마지막 4개는 (C1), (C2)에 의해 당연. 또한 그 밑의 두 번째 표는 $\vee$, $\rightarrow$, $\leftrightarrow$의 정의이므로 당연히 sound. $\square$
Formal proof는 어느 formula가 다른 formula들의 consequence가 됨을 보이는 방법을 제공한다. 다음의 corollary들에 따르면, formal proof는 formula가 valid인지, unsatisfiable인지까지도 보일 수 있다.
Corollary 1.4.10
$G$가 empty set으로부터 유도될 수 있으면, $G$는 tautology이다.
Proof.
$\varnothing \vdash G$이면, Monotonicity에 의해, 임의의 formula들의 집합 $\mathcal{F}$에 대해 $\mathcal{F} \vdash G$. Theorem 1.4.9로부터 $\mathcal{F} \models G$이고, 이는 임의의 assignment $\mathcal{A}$에 대해 $\mathcal{A} \models G$를 의미. 따라서 $G$는 tautology. $\square$
Corollary 1.4.11
$\neg G$가 empty set으로부터 유도될 수 있으면, $G$는 contradiction이다.
Proof.
Corollary 1.4.10과 contradiction의 정의에 의해 자명. $\square$
Example 1.4.12
다음은 $((A\rightarrow B) \vee A)$가 tautology임을 보이는 formal proof.
| Statement | Justification |
|---|---|
| 1. $\{\neg A\} \vdash \neg A $ | $\textrm{Assumption}$ |
| 2. $\{\neg A\} \vdash (\neg A \vee B) $ | $\vee- \textrm{Introduction}$ applied to 1 |
| 3. $\{\neg A\} \vdash (A \rightarrow B) $ | $\rightarrow- \textrm{Definition}$ applied to 2 |
| 4. $\{\neg A\} \vdash (( A \rightarrow B) \vee A) $ | $\vee- \textrm{Introduction}$ applied to 3 |
| 5. $\{ A\} \vdash A $ | $\textrm{Assumption}$ |
| 6. $\{ A\} \vdash (A \vee ( A \rightarrow B)) $ | $\vee- \textrm{Introduction}$ applied to 5 |
| 7. $\{ A\} \vdash (( A \rightarrow B) \vee A) $ | $\vee- \textrm{Symmetry}$ applied to 6 |
| 8. $\varnothing \vdash (( A \rightarrow B) \vee A) $ | $\textrm{Proof by Cases}$ applied to 4 and 7 |
Provably Equivalent
Formal proof는 두 formula가 동치임을 보일 때도 쓰인다.
Definition 1.4.13
$\{ F\} \vdash G $이고 $\{ G\} \vdash F $이면, formula $F$와 $G$는 provably equivalent(증명 가능하게 동치)이다.
Corallary 1.4.14
Formula $F$와 $G$가 provably equivalent이면, $F$와 $G$는 equivalent.
Proof.
Theorem 1.4.9로부터 자명. $\square$
Theorem 1.4.9와 그 역을 생각해 보자. Theorem 1.4.9는 $G$가 $\mathcal{F}$로부터 유도되면 $G$가 $\mathcal{F}$의 consequence가 된다는 의미이다. 그럼 그 역은? $\mathcal{F}$의 모든 consequence로부터 $\mathcal{F}$를 유도해낼 수 있을까? Example 1.4.12처럼 모든 tautology들이 formal proof를 가질 수 있을까? 임의의 두 formula가 equivalent이면, 그것을 증명할 수 있을까?
Answer.
Yes. Propositional logic에서 참인 모든 rule은 $\wedge$와 $\not$의 table로부터 유도해낼 수 있다. 그러나 이는 자명하진 않다.
Example 1.4.15
아직 rule list가 완전하지 않은 것 같다. $F$와 $\neg \neg F$는 명백히 equivalent. 그렇다면 우리는 $\neg \neg F$가 포함된 formula들의 집합으로부터 $F$를 유도해낼 수 있어야 한다. Double negation의 역을 보이자.
$\qquad\textrm{Premise : }\mathcal{F} \vdash \neg \neg F$
$\qquad\textrm{Conclusion : }\mathcal{F} \vdash F$
| Statement | Justification |
|---|---|
| 1. $\mathcal{F} \vdash \neg \neg F$ | $\textrm{Premise}$ |
| 2. $\mathcal{F} \cup \{\neg F\} \vdash \neg \neg F$ | $\textrm{Monotonicity}$ |
| 3. $\mathcal{F} \cup \{\neg F\} \vdash \neg F$ | $\textrm{Assumption}$ |
| 4. $\mathcal{F} \cup \{\neg F\} \vdash (\neg F \wedge \neg \neg F)$ | $\wedge- \textrm{Introduction}$ applied to 3 and 2 |
| 5. $\mathcal{F} \cup \{\neg F\} \vdash F$ | $\textrm{Contradiction rule}$ applied to 4 |
| 6. $\mathcal{F} \cup \{F\} \vdash F$ | $\textrm{Assumption}$ |
| 7. $\mathcal{F} \vdash F$ | $\textrm{Proof by Cases}$ applied to 5 and 6 |
즉, $F$와 $\neg \neg F$가 equivalent라는 사실뿐만 아니라 이들이 equivalent임을 증명할 수 있다. 이제 Section 1.3에서 등장한 모든 equivalence들이 ‘provably equivalent’라고 주장할 수 있겠다. 다음은 Example 1.3.6의 Distributivity Rule과 Example 1.3.7의 De Morgan’s Rule 차례.
Proposition 1.4.16 [De Morgan’s Rules]
Example 1.3.7의 equvalent formula들의 순서쌍들은 provably equivalent.
Proof.
두 번째 것만 보이자. 다음 두 formal proof가 필요하다:
$\qquad \{\neg(F\vee G)\} \vdash (\neg F \wedge \neg G)\textrm{, and} \\ \qquad \{\neg F\wedge \neg G)\} \vdash \neg (F \vee G).$
| Statement | Justification |
|---|---|
| 1. $\{\neg (\neg F \wedge \neg G)\} \vdash (F \vee G)$ | $\vee- \textrm{Introduction}$ |
| 2. $\{\neg(F\vee G)\} \vdash \neg \neg(\neg F \wedge \neg G)$ | $\textrm{Contrapositive}$ applied to 1 |
| 3. $\{\neg(F\vee G)\} \vdash (\neg F \wedge \neg G)$ | $\textrm{Double negation}$ applied to 2 |
| Statement | Justification |
|---|---|
| 1. $\{(\neg F\wedge \neg G)\} \cup \{ (F \vee G)\} \vdash (F \vee G)$ | $\textrm{Assumption}$ |
| 2. $\{(\neg F\wedge \neg G)\} \cup \{ (F \vee G)\} \vdash (\neg F\wedge \neg G)$ | $\textrm{Assumption}$ |
| 3. $\{(\neg F\wedge \neg G)\} \cup \{ (F \vee G)\} \vdash \neg F$ | $\wedge- \textrm{Elimination}$ applied to 2 |
| 4. $\{(\neg F\wedge \neg G)\} \cup \{ (F \vee G)\} \vdash G$ | $\vee- \textrm{Elimination}$ applied to 1 and 3 |
| 5. $\{(\neg F\wedge \neg G)\} \cup \{ (F \vee G)\} \vdash (\neg G\wedge \neg F)$ | $\wedge- \textrm{Symmetry}$ applied to 2 |
| 6. $\{(\neg F\wedge \neg G)\} \cup \{ (F \vee G)\} \vdash \neg G$ | $\wedge- \textrm{Elimination}$ applied to 5 |
| 7. $\{\neg F\wedge \neg G)\} \vdash \neg (F \vee G)$ | $\textrm{Proof by Contradiction}$ applied to 4 and 6 |
남은 하나도 유사하게 보일 수 있다. $\square$
Proposition 1.4.17 [Distributivity]
임의의 formula $F$, $G$, $H$에 대해
$(F \wedge (G \vee H))$와 $((F \wedge G) \vee (F \wedge H))$는 provably equivalent.
또, $(F \vee (G \wedge H))$와 $((F \vee G) \wedge (F \vee H))$는 provably equivalent.
Proof.
첫 번째만 보이자. 각 formula가 반대쪽으로부터 유도될 수 있음을 보여야 한다.
먼저 $F \wedge (G \vee H)$로부터 $(F \wedge G) \vee (F \wedge H)$가 유도될 수 있음을 보이자.
$\qquad\textrm{Premise : }\mathcal{F} \vdash F \wedge (G \vee H)$
$\qquad\textrm{Conclusion : }\mathcal{F} \vdash (F \wedge G) \vee (F \wedge H)$
Proof by Case를 사용. Premise를 가정한 상태에서, $\mathcal{F} \cup \{G\}$와 $\mathcal{F} \cup \{\neg G\}$로부터 $(F \wedge G) \vee (F \wedge H)$를 보인다.
Premise로부터 $\mathcal{F} \cup \{G\} \vdash F$이고, $\mathcal{F} \cup \{G\}$로부터 $(F \wedge G)$가 유도된다. $\vee$-Introduction를 적용하면 $\mathcal{F} \cup \{G\}\vdash (F \wedge G) \vee (F \wedge H)$를 얻는다.
다시, Premise에 의하면 $\mathcal{F} \cup \{\neg G\}$로부터 $F$와 $(G \vee H)$가 유도된다. $\mathcal{F} \cup \{\neg G\} \vdash \neg G$이므로, $\vee$-Modus Ponens에 의하여 $(G \vee H)$로부터 $\mathcal{F} \cup \{\neg G\}\vdash H$가 유도된다. 이제 $\wedge$-Introduction과 $\vee$-Introduction을 사용하면 끝.
역방향도 보여야 한다.
$\qquad\textrm{Premise : }\mathcal{F} \vdash (F \wedge G) \vee (F \wedge H)$
$\qquad\textrm{Conclusion : }\mathcal{F} \vdash F \wedge (G \vee H)$
$\wedge$-Elimination과 $\vee$-Elimination을 각각 2번씩 사용한다. $\wedge$-Elimination에 의해 $\mathcal{F} \cup \{(F \wedge G)\}$와 $\mathcal{F} \cup \{(F \wedge H)\}$으로부터 각각 $(G \vee H)$를 유도할 수 있으므로, $\vee$-Elimination에 의해 $\mathcal{F} \vdash (G \vee H)$. 마찬가지로 $\mathcal{F} \vdash F$를 얻을 수 있다. $\wedge$-Introduction으로 마무리. $\square$
물론, 이러한 equivalence를 보이기 위해 꼭 formal proof를 사용해야 하는 것은 아니다. Distributivity나 De Morgan’s Rules은 오히려 진리표를 확인하는 것이 더 효율적이다. 그렇지만 위 두 내용은 ‘Propositional logic에서 참인 것은 형식적으로 증명 가능하다!’는 우리의 예상에 힘을 실어준다.
이 Section의 맨 앞에서 우리는 formal proof의 개념과 consequence의 개념이 어떻게 연결되는지에 관심이 있다고 했다. Theorem 1.4.9에서 우리는 $G$가 $F$로부터 형식적으로 증명된다면 $G$가 $F$의 consequence임을 보였다. 그리고, 그 역도 (증명은 안 했지만) 참이라고 했다. 즉, Propositional logic에서 기호 $\models$와 $\vdash$는 같은 의미를 갖는다. 이를 Completeness Theorem for propositional logic이라고 하며, 이를 증명하는 것이 Chapter 1의 목표이다.