math - ヒルベルトシステム-証明の自動化

Question

ヒルベルト流の体系でステートメント〜（a->〜b）=>aを証明しようとしています。残念ながら、証拠を見つけるための一般的なアルゴリズムを思い付くのは不可能のようですが、私はブルートフォースタイプの戦略を探しています。これを攻撃する方法についてのアイデアは大歓迎です。

score 26 · Accepted Answer

組み合わせ論理の「プログラミング」が好きなら、

いくつかの論理問題を別の分野に自動的に「翻訳」することができます: 組み合わせ論理用語の同等性を証明します。
優れた関数型プログラミングの実践で, あなたはそれを解決することができます,
その後、答えを元の論理問題のヒルベルトスタイルの証明に戻すことができます。

カリー・ハワード対応により、この翻訳の可能性が保証されます。

残念ながら、状況は (命題) ロジックのサブセットに対してのみ非常に単純です: 条件を使用して制限されています。否定は合併症です、私はそれについて何も知りません。したがって、私はこの具体的な質問に答えることができません:

¬ ( α ⊃ ¬ β ) ⊢ α

ただし、否定が問題の一部ではない場合、関数型プログラミングまたは組み合わせロジックを既に実践している場合は、前述の自動変換 (および逆変換) が役立ちます。

もちろん、ロジックの領域内にとどまることができる他のヘルプもあります。

より直観的な演繹システム (自然演繹など)で問題を証明する
その後、「コンパイラ」の可能性を提供するメタセオレムを使用して、自然演繹の「高レベル」証明をヒルベルト式演繹システムの「マシンコード」に変換します。たとえば、「演繹定理」というメタロジー定理のことです。

定理証明者に関しては、私が知る限り、それらの一部の機能は、インタラクティブな人間の支援を利用できるように拡張されています。たとえば、 Coqはそのようなものです。

付録

例を見てみましょう。α ⊃ αを証明する方法は?

ヒルベルト系

Verum ex quolibet _{α , β}は公理スキームとして想定され、文α ⊃ β ⊃ αは演繹可能であると予想され、任意のサブセンテンスα , βに対してインスタンス化されます。
チェーンルール_{α , β , γ} は公理スキームとして想定され、その文 ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γは演繹可能であると予想され、サブセンテンスα、βに対してインスタンス化されます。
Modus ponensは推論の規則として仮定されます。α ⊃ βが演繹可能であり、αも演繹可能である場合、 α ⊃ βも演繹可能であると推論することが正当化されると期待されます。

定理を証明しましょう: α ⊃ αは任意のα命題に対して演繹可能です。

「証明計算」を展開して、次の表記法と略語を紹介しましょう。

証明計算

VEQ _{α , β} : ⊢ α ⊃ β ⊃ α
CR _{α , β , γ} : ⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ
MP : ⊢ α ⊃ βおよび ⊢ αの場合、⊢ βも

ツリーダイアグラム表記:

公理スキーム — Verum ex quolibet:

━━━━━━━━━━━━━━━━━ [ VEQ _{α , β} ]
⊢ α ⊃ β ⊃ α

公理スキーム — チェーンルール:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [ CR _{α , β , γ} ]
⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ

推論規則 — ポネン法:

     ⊢ α ⊃ β           ⊢ α
    ━━━━━━━━━━━━━━━━━━━ [ MP ]
                     ⊢ β

証明木

証明のツリーダイアグラム表現を見てみましょう。

━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [ CR _{α , α ⊃α, α} ] ━━━━━━━━━━ ━━━━━━ [ VEQ _{α , α ⊃α} ]
⊢ [ α ⊃( α ⊃α)⊃α]⊃( α ⊃α⊃α )⊃α⊃α ⊢ α ⊃ ( α ⊃ α ) ⊃ α
━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━━━━━━━━━━━━━━━━━━━━━━━━ [ MP ] ━━━━━━━━━━━ [ VEQ _{α , α} ]
 ⊢ ( α ⊃ α⊃ α ) ⊃ α ⊃ α ⊢ α ⊃ α ⊃ α
 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━━━━━━━━━━━━━━ [ MP ]
 ⊢ α ⊃ α

証明式

証明のさらに簡潔な (代数的? 微積分?) 表現を見てみましょう。

( CR _{α , α ⊃α, α} VEQ _{α , α ⊃ α} ) VEQ _{α , α} : ⊢ α ⊃ α

したがって、証明木は次の 1 つの式で表すことができます。

ツリーの分岐 (modus ponens) は、単純な連結 (括弧) によってレンダリングされます。
ツリーの葉は、対応する公理名の省略形によってレンダリングされます。

具体的なインスタンス化について記録しておく価値があります。これは、サブインデックスパラメータでここにタイプセットされています。

以下の一連の例からわかるように、公理は基本コンビネータの一種として表記され、法ポネンはその「前提」サブ証明の単なる適用として表記される証明計算を開発できます。

例 1

VEQ _{α , β} : ⊢ α ⊃ β ⊃ α

の意味

α , βでインスタンス化されたVerum ex quolibet公理スキームは、 α ⊃ β ⊃ αが演繹可能であるというステートメントの証明を提供します。

例 2

VEQ _{α , α} : ⊢ α ⊃ α ⊃ α

α , αでインスタンス化されたVerum ex quolibet公理スキームは、 α ⊃ α ⊃ αが演繹可能であるというステートメントの証明を提供します。

例 3

VEQ _{α , α ⊃α} : ⊢ α ⊃ ( α ⊃ α ) ⊃ α

の意味

α , α ⊃α でインスタンス化されたVerum ex quolibet公理スキームは、 α ⊃ ( α ⊃ α ) ⊃ αが演繹可能であるというステートメントの証明を提供します。

例 4

CR _{α , β , γ} : ⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ

の意味

α , β , γでインスタンス化された連鎖律公理スキームは、( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γが演繹可能であるというステートメントの証明を提供します。

例 5

CR _{α , α ⊃α, α} : ⊢ [ α ⊃ ( α ⊃α) ⊃ α ] ⊃ ( α ⊃ α ⊃α) ⊃ α ⊃ α

の意味

α , α ⊃α, αでインスタンス化されたチェーンルール公理スキームは、[ α ⊃ ( α ⊃α) ⊃ α ] ⊃ ( α ⊃ α ⊃α) ⊃というステートメントの証明を提供します。α ⊃ αは演繹可能です。

例 6

CR _{α , α ⊃α, α} VEQ _{α , α ⊃ α} : ⊢ ( α ⊃ α ⊃α) ⊃ α ⊃ α

の意味

CR _{α , α ⊃α, α}とVEQ _{α , α ⊃ α}をmodus ponensを介して組み合わせると、次のステートメントを証明する証明が得られます: ( α ⊃ α ⊃α) ⊃ α ⊃ αは演繹可能です。

例 7

( CR _{α , α ⊃α, α} VEQ _{α , α ⊃ α} ) VEQ _{α , α} : ⊢ α ⊃ α

複合証明 ( CR _{α , α ⊃α, α} ) をVEQ _{α , α ⊃ α} ( modus ponens経由) と組み合わせると、さらに複合証明が得られます。これは、次のステートメントを証明します: α ⊃ αは演繹可能です。

組み合わせロジック

上記のすべてが実際に予想される定理の証明を提供しましたが、非常に直感的ではないようです. 人々がどのように証明を「見つける」ことができるかはわかりません。

同様の問題が調査されている別の分野を見てみましょう。

型指定されていない組み合わせロジック

組み合わせ論理は、非常に最小限の関数型プログラミング言語と見なすこともできます。そのミニマリズムにもかかわらず、それは完全にチューリング完全ですが、さらに、「通常の」関数型プログラミングから得られた練習といくつかの代数的洞察により、モジュラーで再利用可能な方法で、この難読化された言語でも非常に直感的で複雑なプログラムを書くことができます。 .

入力規則の追加

組み合わせロジックには、型付きバリアントもあります。構文は型で拡張され、さらに、還元規則に加えて、型規則も追加されます。

ベースコンビネータの場合:

K _{α , β}を基本コンビネータとして選択し、型 α → β → αに存在する
( α → β → γ ) → ( α → β ) → α → γの型に属するS _{α , β , γ}が基本コンビネータとして選択されます。

適用の入力規則:

Xが型α → βに存在し、Yが型αに存在する場合、X Yは型βに存在します。

表記と略語

K _{α , β} : α → β → α
S _{α , β , γ} : ( α → β → γ ) → ( α → β )* → α → γ .
X : α → βかつY : αの場合、 X Y : βです。

カリー・ハワード対応

「パターン」は、証明計算とこの型付き組み合わせ論理で同形であることがわかります。

証明微積分のVerum ex quolibet公理は、組み合わせ論理のKベース結合子に対応します。
証明計算のチェーン規則公理は、組み合わせ論理のSベース結合子に対応します。
証明計算におけるModus ponensの推論規則は、組み合わせ論理における操作「適用」に対応します。
ロジックの「条件付き」接続詞 ⊃ は、型構築子 → 型理論 (および型付き組み合わせ論理) に対応します。

関数型プログラミング

しかし、利益は何ですか？問題を組み合わせ論理に変換する必要があるのはなぜですか? 個人的には、関数型プログラミングは多くの文献があり、実際の問題に適用されるものであるため、時々役立つと思います。日常のプログラミング作業や練習で強制的に使用することで、人々はそれに慣れることができます。また、関数型プログラミングの実践のいくつかのトリックとヒントは、組み合わせロジックのリダクションで非常にうまく活用できます。そして、「転移された」実践が組み合わせ論理で発展するなら、それはヒルベルト系で証明を見つけることにも利用できる。

外部リンク

関数型プログラミング (ラムダ計算、組み合わせ論理) の型を論理的な証明と定理に変換する方法をリンクします。

Wadler、フィリップ（1989）。無料で定理！.

組み合わせロジックで直接プログラミングするための方法と実践を学ぶ方法のリンク (または書籍):

Madore、David（2003）。Unlambda プログラミング言語。Unlambda: 関数型プログラミング言語の悪夢が現実に。
Curry, Haskell B. & Feys, Robert & Craig, William (1958). 組み合わせロジック。巻。私は。アムステルダム: 北ホラント出版社。
トランプ、ジョン（1999）。バイナリラムダ計算と組み合わせ論理。著者のJohn's Lambda Calculus and Combinatory Logic Playgroundから PDF および Postscript でダウンロードできます。

score 6 · Accepted Answer

通常、ヒルベルトシステムは、自動化された定理証明では使用されません。自然演繹法を使用して証明を行うコンピュータープログラムを作成する方がはるかに簡単です。CSコースの資料より：

Hilbert システムに関するいくつかの FAQ: Q: どの公理スキーマを使用し、どの置換を行うべきかをどのように知ることができますか? 可能性は無数にあるため、原理的にもすべてを試すことはできません。A: アルゴリズムはありません。少なくとも単純なものではありません。むしろ、賢くなければなりません。純粋数学では、証明の存在に最も関心があるため、これは問題とは見なされません。ただし、コンピュータサイエンスアプリケーションでは、演繹プロセスの自動化に関心があるため、これは致命的な欠陥です。通常、ヒルベルトシステムは、自動化された定理証明では使用されません。Q: では、なぜ人々はヒルベルトシステムに関心を持つのでしょうか? A: modus ponens を単一の演繹法として使用することで、人間がどのように数学的証明を考案するかについての好ましいモデルを提供します。後で述べるように、

score 5 · Accepted Answer

¬ α = α → ⊥ と設定することでも問題にアプローチできます。次に、答えの1つの付録に示されているように、ヒルベルトスタイルシステムを採用し、次の2つの公理をそれぞれ定数に追加して古典的にすることができます。

Ex Falso Quodlibet: E _α : ⊥ → α
Consequentia Mirabilis: M _α : (¬ α → α) → α

¬ (α → ¬ β) → α の逐次証明は次のようになります。

α ⊢ α (アイデンティティ)
⊥ ⊢ β → ⊥ (元ファルソクォドリベット)
α → ⊥、α ⊢ β → ⊥ (実装イントロ左 1 & 2)
α → ⊥ ⊢ α → (β → ⊥) (Impl Intro Right 3)
⊥ ⊢ α (元ファルソクォドリベット)
(α → (β → ⊥)) → ⊥, α → ⊥ ⊢ α (実装イントロ左 4 & 5)
(α → (β → ⊥)) → ⊥ ⊢ α (結果 6)
⊢ ((α → (β → ⊥)) → ⊥) → α (実装イントロ右 7)

この一連の証明から、ラムダ式を抽出できます。上記のシーケント証明の可能なラムダ式は次のようになります。

λy.(M λz.(E (y λx.(E (zx)))))

このラムダ式は、SKI 用語に変換できます。上記のラムダ式の可能な SKI 用語は次のとおりです。

S (KM)) (L2 (L1 (K (L2 (L1 (KI))))))
ここで、L1 = (S ((S (KS)) ((S (KK)) I)))
および L2 = ( S (K (S (KE))))

これにより、次のヒルベルトスタイルの証明が得られます。

補題 1: 連鎖律の弱体化:
1: ((A → B) → ((C → A) → (C → B))) → (((A → B) → (C → A)) → ((A → B) → (C → B))) [連鎖]
2: ((A → B) → ((C → (A → B)) → ((C → A) → (C → B)) )) → ((((A → B) → (C → (A → B))) → ((A → B) → ((C → A) → (C → B)))) [チェーン]
3: ( (C → (A → B)) → ((C → A) → (C → B))) → ((A → B) → ((C → (A → B)) → ((C → A) → (C → B)))) [Verum Ex]
4: (C → (A → B)) → ((C → A) → (C → B)) [Chain]
5: (A → B) → (( C → (A → B)) → ((C → A) → (C → B))) [MP 3, 4]
6: ((A → B) → (C → (A → B))) → ( (A → B) → ((C → A) → (C → B))) [MP 2、5]
7: ((A → B) → ((A → B) → (C → (A → B) ))) → (((A → B) → (A → B)) → ((A → B) → (C → (A → B)))) [連鎖]
8: ((A → B) → ( C → (A → B))) → ((A → B) → ((A → B) → (C → (A → B)))) [Verum Ex]
9：(A→B)→(C→(A→B))【Verum Ex】
10：(A→B)→((A→B)→(C→(A→B)))【MP8、 9]
11: ((A → B) → (A → B)) → ((A → B) → (C → (A → B))) [MP 7, 10]
12: (A → B) → ( A → B) [同一性]
13: (A → B) → (C → (A → B)) [MP 11, 12]
14: (A → B) → ((C → A) → (C → B) ) [MP 6, 13]
15: ((A → B) → (C → A)) → ((A → B) → (C → B)) [MP 1, 14]

補題 2: Ex Falso の弱体化形式:
1: (A → ((B → ⊥) → (B → C))) → ((A → (B → ⊥)) → (A → (B → C)) ) [チェーン]
2: ((B → ⊥) → (B → C)) → (A → ((B → ⊥) → (B → C))) [Verum Ex]
3: (B → (⊥ → C )) → ((B → ⊥) → (B → C)) [Chain]
4: (⊥ → C) → (B → (⊥ → C)) [Verum Ex]
5: ⊥ → C [Ex Falso]
6 : B → (⊥ → C) [MP 4, 5]
7: (B → ⊥) → (B → C) [MP 3, 6]
8: A → ((B → ⊥) → (B → C)) [MP 2, 7]
9: (A → (B → ⊥)) → (A → (B → C)) [MP 1, 8]

最終証明:
1: (((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A)) → ((((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) → (((A → (B → ⊥)) → ⊥) → A)) [連鎖]
2: (((A → ⊥) → A) → A) → ( ((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A)) [Verum Ex]
3: ((A → ⊥) → A) → A [Mirabilis]
4: ((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A) [MP 2, 3]
5: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) → (((A → (B → ⊥)) → ⊥) → A) [MP 1, 4]
6: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥)) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) [補題 2]
7: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥)))) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥ )) [補題 1]
8: ((A → ⊥) → (A → (B → ⊥))) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥)))) [Verum Ex]
9: ((A → ⊥) → (A → ⊥)) → ((A → ⊥) → (A → (B → ⊥))) [補題 2]
10: ((A → ⊥) → (A → A )) → ((A → ⊥) → (A → ⊥)) [補題 1]
11: (A → A) → ((A → ⊥) → (A → A)) [Verum Ex]
12: A → A [同一性]
13: (ア → ⊥) → (ア → ア) [MP 11, 12]
14: (ア → ⊥) → (ア → ⊥) [MP 10, 13]
15: (ア → ⊥) → ( A → (B → ⊥)) [MP 9, 14]
16: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥))) [MP 8 , 15]
17: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥) [MP 7, 16]
18: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A) [MP 6, 17]
19: ((A → (B → ⊥)) → ⊥) → A [MP 5, 18]

かなり長い証拠！

さよなら

score 4 · Accepted Answer

ヒルベルト計算で証明を見つけるのは非常に困難です。

逐次微積分または自然演繹の証明をヒルベルト微積分に変換してみてください。

score 2 · Accepted Answer

どの特定のヒルベルトシステムですか？トンがあります。
おそらく最良の方法は、シークエント計算で証明を見つけて、それをヒルベルト流の体系に変換することです。

score 1 · Accepted Answer

ポーランド語表記を使用しています。

あなたはウィキペディアを参照したので、私たちの根拠は

1 CpCqp。

2 CCpCqrCCpqCpr。

3 CCNpNqCqp.

証明したい

NCaNb |- a.

私は定理証明者Prover9を使用しています。したがって、すべてを括弧で囲む必要があります。また、Prover9 の変数は (x, y, z, u, w, v5, v6, ..., vn) になります。他のすべての記号は、関数または関係または述語として解釈されます。すべての公理は、それらの前にも述語記号「P」を必要とします。これは、「... が証明可能である」またはより単純に「証明可能」を意味すると考えることができます。また、Prover9 のすべての文はピリオドで終了する必要があります。したがって、公理 1、2、および 3 はそれぞれ次のようになります。

1 P(C(x,C(y,x)))。

2 P(C(C(x,C(y,z)),C(C(x,y),C(x,z))))。

3 P(C(C(N(x),N(y)),C(y,x)))。

均一な置換と分離の規則を、凝縮された分離の規則に組み合わせることができます。Prover9 では、これを次のように表すことができます。

-P(C(x,y)) | -P(x) | P(y)。

「|」は論理和、「-」は否定を表します。Prover9 は矛盾によって証明します。このルールは、「x の場合、y が証明可能であるとは限らない、または x が証明可能であるとは限らない、または y が証明可能であるとは限らない」と解釈することができます。したがって、x の場合、y が証明可能であると保持する場合、最初の選言は失敗します。x が証明可能であることが保持される場合、2 番目の選言は失敗します。したがって、x の場合、y が証明可能である場合、x が証明可能である場合、y が証明可能であるという 3 番目の選言は規則に従います。

NCaNb はトートロジーではないため、置換を行うことはできません。「あ」でもありません。したがって、

P(N(C(a,N(b))))。

前提として、Prover9 は "a" と "b" をnullary関数として解釈し、効果的にそれらを定数に変換します。また、目標として P(a) を作成したいと考えています。

これで、重み付け、共鳴、サブフォーミュラ、選択比、レベル飽和などのさまざまな定理証明戦略を使用して、Prover9 を「調整」することもできます (または独自に発明することさえできます)。すべての仮定 (推論規則を含む) と目標をヒントにすることで、ヒント戦略を少し使用します。また、最大重みを 40 に下げ、最大変数の数を 5 にします。

私はグラフィカルインターフェイスを備えたバージョンを使用していますが、入力全体は次のとおりです。

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
assign(max_seconds, -1).
assign(max_weight, 40).
end_if.

if(Mace4).   % Options for Mace4
assign(max_seconds, 60).
end_if.

if(Prover9). % Additional input for Prover9
formulas(hints).
-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).
P(a).
end_of_list.
assign(max_vars,5).
end_if.

formulas(assumptions).

-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).

end_of_list.

formulas(goals).

P(a).

end_of_list.

これが私に与えた証拠です：

============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 1312 was started by Doug on Machina2,
Mon Jun  9 22:35:37 2014
The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace43/bin-win32/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.01) seconds.
% Length of proof is 23.
% Level of proof is 9.
% Maximum clause weight is 20.
% Given clauses 49.

1 P(a) # label(non_clause) # label(goal).  [goal].
2 -P(C(x,y)) | -P(x) | P(y).  [assumption].
3 P(C(x,C(y,x))).  [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).  [assumption].
5 P(C(C(N(x),N(y)),C(y,x))).  [assumption].
6 P(N(C(a,N(b)))).  [assumption].
7 -P(a).  [deny(1)].
8 P(C(x,C(y,C(z,y)))).  [hyper(2,a,3,a,b,3,a)].
9 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).  [hyper(2,a,4,a,b,4,a)].
12 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))).  [hyper(2,a,4,a,b,5,a)].
13 P(C(x,C(C(N(y),N(z)),C(z,y)))).  [hyper(2,a,3,a,b,5,a)].
14 P(C(x,N(C(a,N(b))))).  [hyper(2,a,3,a,b,6,a)].
23 P(C(C(a,N(b)),x)).  [hyper(2,a,5,a,b,14,a)].
28 P(C(C(x,C(C(y,x),z)),C(x,z))).  [hyper(2,a,9,a,b,8,a)].
30 P(C(x,C(C(a,N(b)),y))).  [hyper(2,a,3,a,b,23,a)].
33 P(C(C(x,C(a,N(b))),C(x,y))).  [hyper(2,a,4,a,b,30,a)].
103 P(C(N(b),x)).  [hyper(2,a,33,a,b,3,a)].
107 P(C(x,b)).  [hyper(2,a,5,a,b,103,a)].
113 P(C(C(N(x),N(b)),x)).  [hyper(2,a,12,a,b,107,a)].
205 P(C(N(x),C(x,y))).  [hyper(2,a,28,a,b,13,a)].
209 P(C(N(a),x)).  [hyper(2,a,33,a,b,205,a)].
213 P(a).  [hyper(2,a,113,a,b,209,a)].
214 $F.  [resolve(213,a,7,a)].

============================== end of proof ==========================