まず次が成り立つ r.e. 集合 \(X' \supseteq X\) をとる（このような \(X'\) がとれることは下のコメント参照）：
- (1) \(X'\) は monoconsistent with \({\sf Q}\),
- (2) \(\varphi \to \psi \in X'\) かつ \({\sf Q} \vdash \varphi\) ならば \(\psi \in X'\),
- (3) \(\varphi \in X'\) かつ \({\sf Q} \vdash \varphi \to \psi\) ならば \(\psi \in X'\).
\(X'\) は r.e. なので \(X' = \{k : \exists m P(k, m)\}\) となるような原始再帰的関係 \(P\) がとれる． \(R(k, i, \gamma, p)\) を次の原始再帰的関係とする：
"ある二進列 \(s\) があって，\(s_k = i\) であり \(P(\gamma(0)^{s_0} \lor \cdots \lor \gamma(k)^{s_k}, p)\) が成り立つ"．
\(\rho(x, y, z, w)\) を \(R(k, i, \gamma, p)\) の PR binumeration とし， \[ {\sf Q} \vdash \eta(x) \leftrightarrow \forall z(\rho(x, 0, \eta, z) \to \exists u \leq z \rho(x, 1, \eta, u)) \] を満たす
\(\Pi_1\) 論理式 \(\eta(x)\) をとる． ここで \(\eta(k)\) という形の文のトートロジーでないような propositional combination \(\xi\) の conjunctive normal form \(\xi_0 \land \cdots \land \xi_m\) をとれば \({\sf Q} \vdash \xi \to
\xi_0\) となる（ここで各 \(\xi_j\) は異なる \(k\) について \(\eta(k)^i\)(\(i = 0, 1\)) という形の文の disjunction）． したがって \(\xi_0 \notin X'\) が示せれば、条件 (3) より \(\xi \notin X'\) が従い，\(X' \supseteq X\) より \(\xi \notin X\)
が結論付けられる． またある二進列 \(s\) と自然数 \(n\) について \({\sf Q} \vdash \xi_0 \to \eta(0)^{s_0} \lor \cdots \lor \eta(n)^{s_n}\) なので，条件 (3) より \(\eta(0)^{s_0} \lor \cdots \lor \eta(n)^{s_n} \notin X'\) ならば
\(\xi_0 \notin X'\) である．
以上より，全ての二進列 \(s\) と自然数 \(n\) について \(\eta(0)^{s_0} \lor \cdots \lor \eta(n)^{s_n} \notin X'\) となることが示せればよいことがわかった．
\(\eta(0)^{s_0} \lor \cdots \lor \eta(n)^{s_n} \in X'\) となる二進列 \(s\) と自然数 \(n\) があると仮定して矛盾を導く． そのような二進列 \(s\) があるような最小の \(n\) をとる．
- \(n=0\) のときある二進列 \(s\) について \(\eta(0)^{s_0} \in X'\) である． \(P(\eta(0)^{s_0}, p)\) となるような \(s\) がある最小の \(p\) をとる．
- \(s_0 = 0\) のとき：\(\eta(0) \in X'\) である． \(p\) の取り方より \({\sf Q} \vdash \rho(0, 0, \eta, p) \land \forall u \leq p \neg \rho(0, 1, \eta, u)\) なので \({\sf Q} \vdash \neg \eta(0)\)
となり，\(X'\) が monoconsistent with \({\sf Q}\) であることに反する．
- \(s_0 = 1\) のとき：\(\neg \eta(0) \in X'\) である． \(p\) の取り方より \({\sf Q} \vdash \rho(0, 1, \eta, p) \land \forall z < p \neg \rho(0, 0, \eta, z)\) なので \({\sf Q} \vdash \eta(0)\) となる．
よって \(X'\) が monoconsistent with \({\sf Q}\) であることに反する．
- \(n > 0\) のとき，ある二進列 \(s\) について \(\eta(0)^{s_0} \lor \cdots \lor \eta(n)^{s_n} \in X'\) である． \(P(\eta(0)^{s_0} \lor \cdots \lor \eta(n)^{s_n}, p)\) となる \(s\) があるような最小の \(p\) をとる．
- \(s_n = 0\) のとき：\(\eta(0)^{s_0} \lor \cdots \lor \eta(n) \in X'\) である． 条件 (3) より \(\neg \eta(n) \to \eta(0)^{s_0} \lor \cdots \lor \eta(n-1)^{s_{n-1}} \in X'\) である． \(p\) の取り方より
\({\sf Q} \vdash \rho(n, 0, \eta, p) \land \forall u \leq p \neg \rho(n, 1, \eta, u)\) なので \({\sf Q} \vdash \neg \eta(n)\) となる． 条件 (2) より \(\eta(0)^{s_0} \lor \cdots \lor
\eta(n-1)^{s_{n-1}} \in X'\) となるため，\(n\) の最小性に反する．
- \(s_0 = 1\) のとき：\(\eta(0)^{s_0} \lor \cdots \lor \neg \eta(n) \in X'\) である． 条件 (3) より \(\eta(n) \to \eta(0)^{s_0} \lor \cdots \lor \eta(n-1)^{s_{n-1}} \in X'\) である． \(p\) の取り方より
\({\sf Q} \vdash \rho(n, 1, \eta, p) \land \forall z < p \neg \rho(n, 0, \eta, z)\) なので \({\sf Q} \vdash \eta(n)\) となる． 条件 (2) より \(\eta(0)^{s_0} \lor \cdots \lor \eta(n-1)^{s_{n-1}}
\in X'\) となるため，\(n\) の最小性に反する．
いずれの場合も矛盾するため，全ての二進列 \(s\) と自然数 \(n\) について \(\eta(0)^{s_0} \lor \cdots \lor \eta(n)^{s_n} \notin X'\) となることが示せた．
コメント
\(X\) を monoconsistent with \({\sf Q}\) である r.e. 集合とする． このとき，
- (1) \(X'\) は monoconsistent with \({\sf Q}\),
- (2) \(\varphi \to \psi \in X'\) かつ \({\sf Q} \vdash \varphi\) ならば \(\psi \in X'\),
- (3) \(\varphi \in X'\) かつ \({\sf Q} \vdash \varphi \to \psi\) ならば \(\psi \in X'\),
を満たす r.e. 集合 \(X' \supseteq X\) がとれることを証明する．
まず集合の列 \(X_0, X_1, \cdots\) と \(Y_1, Y_2, \cdots\) を次のように定める：
- \(X_0 : = X\)
- \(Y_{i+1} : = X_i \cup \{\psi : \varphi \to \psi \in X_i\) かつ \({\sf Q} \vdash \varphi\}\)
- \(X_{i+1} : = Y_{i+1} \cup \{\psi : \varphi \in Y_{i+1}\) かつ \({\sf Q} \vdash \varphi \to \psi\}\)
そして \(X' : = \bigcup_{i \in \omega} X_i\) とする． \(X' \supseteq X\) であることは明らか． また各 \(i \in \omega\) について \(X_i\) は r.e. 集合なので \(X'\) も r.e. 集合である．