1.10 Craig’s Interpolation Theorem
Theorem 1.10.1 [Craig’s Interpolation Theorem]
$\models (F \rightarrow G)$이고, $F$는 contradiction이 아니며 $G$는 tautology가 아니라고 하자.
그러면 어떤 formula $H$가 존재하여,1 $H$의 모든 atomic formula가 $F$와 $G$ 양쪽에 속하고 $\models (F \rightarrow H)$와 $\models (H \rightarrow G)$를 만족한다.
Proof.
$\models (F \rightarrow G)$라고 가정하자. Mathematical induction을 이용하고자 한다. $F$에는 등장하나 $G$에는 등장하지 않는 atomic formula의 수를 $n$이라고 하고, 이를 $|atoms(F)-atoms(G)| = n$으로 나타내자. 즉 $atoms(F)$는 $F$의 atomic formula들의 set.
[Base Step] $n=0$이라고 하자. $F$의 모든 atomic formula는 $F$와 $G$ 양쪽에 속하고, $\models (F \rightarrow F)$와 $\models (F \rightarrow G)$이다. 따라서 $F$가 원하는 interpolant가 된다.
[Inductive Step] $\vert atoms(X)-atoms(G) \vert = n$을 만족하는 $X$에 대해 정리가 성립한다고 가정한다. $\vert atoms(F)-atoms(G)\vert = n+1$이라고 하자. 그 중 하나를 $A$라고 하자. 즉, $A \in atoms(F)$이다.
이제 다음을 정의:
$F_{0}= $[$F$에 등장하는 모든 $A$를 tautology $T$로 치환한 formula].
$F_{1}= $[$F$에 등장하는 모든 $A$를 contradiction $\perp$로 치환한 formula].
$F’=F_{0} \vee F_{1}$라고 하자. 그러면 다음 세 가지가 성립한다.
\[\models (F’ \rightarrow G) \tag{1} \]
\[\vert atoms(F’)-atoms(G) \vert = n \tag{2} \]
\[\models (F \rightarrow F’) \tag{3} \]
$(1),(2)$와 induction hypothesis에 의해, interpolant $H$가 존재해서,
\[\models (F’ \rightarrow H) \tag{4}\]
\[\models (H \rightarrow G) \tag{5}\]
또한, $(3),(4)$로부터,
\[\models (F \rightarrow H) \tag{6}\]
따라서, 원하는 interpolant $H$를 얻는다. $\square$
-
그러한 $H$를 interpolant라고 한다. ↩