Ответ 1

Если вам нравится "программирование" в комбинационная логика, то

• Вы можете автоматически "перевести" некоторые логические задачи в другое поле: доказать равенство комбинаторных логических терминов.
• С хорошей практикой функционального программирования вы можете решить это,
• а затем вы можете перевести ответ обратно на доказательство Гильберта о вашей исходной логической проблеме.

Возможность этого перевода обеспечивается Карри-Говардская переписка.

К сожалению, ситуация настолько проста только для подмножества (пропозициональной) логики: ограничена использованием условных выражений. Отрицание - это сложность, я ничего об этом не знаю. Поэтому я не могу ответить на этот конкретный вопрос:

¬ (α ⊃ ¬β) ⊢ α

Но в тех случаях, когда отрицание не является частью вопроса, упомянутый автоматический перевод (и обратный перевод) может помочь, если вы уже практиковали функциональное программирование или комбинаторную логику.

Конечно, есть и другая помощь, где мы можем оставаться внутри области логики:

• доказательство проблемы в некоторой более интуитивной дедуктивной системе (например, естественная дедукция)
• и затем используя metatheorem, которые предоставляют возможность "компилятора": перевод "высокоуровневого" доказательства естественной дедукции на "машинный код" системы удержания в стиле Гильберта. Я имею в виду, например, металогическую теорему, называемую " теорема дедукции.

Как и для теоретических проксировщиков, насколько я знаю, возможности некоторых из них расширены, чтобы они могли использовать интерактивную человеческую помощь. Например. Coq таков.

Приложение

Давайте посмотрим пример. Как доказать α ⊃ α?

Система Гильберта

• Verum ex quolibet _{α, β} предполагается как схема аксиомы, в котором предполагается, что предложение α ⊃ β ⊃ α будет выводимым, созданным для любых подмножеств α, β
• Правило цепочки _{α, β, γ} принимается как схема аксиомы, указывая, что предложение (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α ⊃ γ, как ожидается, будет выводимым, созданным для любых подмножеств α, β
• Предполагается, что modus ponens считается предпосылкой вывода: при условии, что α ⊃ β выводимо, а также α выводимо, тогда мы ожидаем оправдания, чтобы сделать вывод, что также α ⊃ β выводимо.

Докажем теорему: α ⊃ α выводимо для любого α-предложения.

Введем следующие обозначения и сокращения, разработав "исчисление исчисления":

Исчисление доказательств

• VEQ _{α, β}: ⊢ α ⊃ β ⊃ α
• CR _{α, β, γ}: ⊢ (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ
• MP: если ⊢ α ⊃ β и ⊢ α, затем также ⊢ β

Обозначение древовидной диаграммы:

Схема аксиом - Verum ex quolibet:

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

Аксиома - цепное правило:

    ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [ CR <суб > α, β, γсуб > ]
          ⊢ (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ

Правило вывода - modus ponens:

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

Дерево доказательств

Обратимся к древовидному представлению доказательства:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [ CR _{α, α⊃α, α}]     ━━━━━━━━━━━━━━━ [ VEQ _{α, α⊃α}]
⊢ [Α⊃ (α⊃α) ⊃α] ⊃ (α⊃α⊃α) ⊃α⊃α                         ⊢ α ⊃ (α ⊃ α) ⊃ α
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━━━ [ МП]       &nbsp ━━━━━━━━━━━; [ VEQ <суб > α, αсуб > ]
                                          ⊢ (α ⊃ α ⊃ α) ⊃ α ⊃ α                                               ⊢ α ⊃ α ⊃ α
                                          ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━ [ MP]
                                                                                      ⊢ α ⊃ α

Формулы доказательства

Посмотрим четное конвейерное (алгебраическое?) представление доказательства:

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

поэтому мы можем представить дерево доказательства по одной формуле:

• разворачивание дерева (modus ponens) выполняется простым конкатенацией (круглые скобки),
• а листья дерева отображаются аббревиатурами соответствующих имен аксиом.

Стоит вести запись о конкретном экземпляре, который здесь набирается с субиндексическими параметрами.

Как видно из серии примеров ниже, мы можем разработать исчисление доказательств, где аксиомы обозначаются как сорт базовых комбинаторов, а 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 в исчислении доказательств соответствует операции "приложение" в комбинационной логике.
• "условная" связка ⊃ логики соответствует конструктору типа → теории типов (и типизированной комбинаторной логике)

Функциональное программирование

Но что такое выигрыш? Почему мы должны переводить проблемы на комбинаторную логику? Я лично считаю, что это иногда полезно, потому что функциональное программирование - это вещь, которая имеет большую литературу и применяется в практических задачах. Люди могут привыкнуть к этому, когда вынуждены использовать его в сквозных задачах программирования и pracice. И некоторые трюки и намеки на функциональную программирующую практику можно очень хорошо использовать при сокращении комбинаторной логики. И если "переданная" практика развивается в комбинаторной логике, ее можно использовать и для поиска доказательств в системе Гильберта.

Внешние ссылки

Ссылки, как типы в функциональном программировании (лямбда-исчисление, комбинаторная логика) могут быть переведены на логические доказательства и теоремы:

• Вадлер, Филипп (1989). Теоремы бесплатно!.

Ссылки (или книги), как научиться методам и практике напрямую программировать в комбинаторной логике:

• Мадоре, Дэвид (2003). Язык программирования Unlambda. Unlambda: Ваш функциональный язык программирования Кошмары верны.
• Карри, Хаскелл Б. и Фейс, Роберт и Крейг, Уильям (1958). Комбинированная логика. Vol. I. Амстердам: Издательская компания North-Holland.
• Тромп, Джон (1999). Бинарное исчисление лямбда и комбинационная логика. Загружается в PDF и Postscript от автора Исходное и комбинированное логическое пространство Джона Лямбда.

Ответ 2

Система Гильберта обычно не используется в автоматическом доказательстве теоремы. Гораздо проще написать компьютерную программу для выполнения доказательств с использованием естественной дедукции. Из материала курса CS:

Некоторые часто задаваемые вопросы о системе Гильберта: В: Как узнать, какая аксиома схемы, которые замещения сделать? Поскольку есть бесконечно много возможностей, это невозможно попробовать их всех, даже в princple. A: Нет алгоритма; в наименее простой. Скорее, быть умным. В чистой математике, это не рассматривается как проблема, поскольку один больше всего обеспокоен существование доказательства. Однако в компьютерных приложений, один заинтересованы в автоматизации вычета процесс, так что это фатальный недостаток. Система Гильберта обычно не используется в автоматическое доказательство теоремы. Q: Итак, почему люди заботятся о Гильберте система? A: С modus ponens как его одно дедуктивное правило, оно обеспечивает приемлемая модель того, как люди изобретают математических доказательств. Как мы увидим, методы, которые более поддаются компьютерная реализация дает доказательства которые менее "похожи на людей".

Ответ 3

Найти доказательства в исчислении Гильберта очень сложно.

Вы могли бы попытаться перевести доказательства в последовательном исчислении или естественном выводе на исчисление Гильберта.

Ответ 4

Вы можете обратиться к проблеме также, установив ¬ α = α → ⊥. Затем мы можем принять систему стиля Гильберта, как показано в приложении к одному из ответов, и сделать ее классической, добавив следующие две аксиомы соответственно:

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

Последовательное доказательство ¬ (α → ¬ β) → α затем читается следующим образом:

• α ⊢ α (Identity)
• ⊥ ⊢ β → ⊥ (Ex Falso Quodlibet)
• α → ⊥, α ⊢ β → ⊥ (Impl Intro Left 1 и 2)
• α → ⊥ ⊢ α → (β → ⊥) (Impl Intro Right 3)
• ⊥ ⊢ α (Ex Falso Quodlibet)
• (α → (β → ⊥)) → ⊥, α → ⊥ ⊢ α (Impl Intro Left 4 и 5)
• (α → (β → ⊥)) → ⊥ ⊢ α (Consequentia Mirabilis 6)
• ⊢ ((α → (β → ⊥)) → ⊥) → α (Impl Intro Right 7)

Из этого последовательного доказательства можно извлечь лямбда-выражение. Возможная лямбда-выражения для вышеуказанного последовательного доказательства читаются следующим образом:

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

Это выражение лямбда может быть преобразовано в термин SKI. Возможная Термин SKI для вышеуказанного выражения лямбда выглядит следующим образом:

S (K M)) (L2 (L1 (K (L2 (L1 (K I))))))
где L1 = (S ((S (K S)) ((S (K K)) I)))
и L2 = (S (K (S (K E))))

Это дает следующие доказательства стиля Гильберта:

Лемма 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)) [Цепь]
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))) [MP 8, 9]
11: ((A → B) → (A → B)) → ((A → B) → (C → (A → B))) [MP 7, 10]
12: (A → B) → (A → B) [Identity]
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)) [Цепочка]
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)) → ((((→ → B)) → ⊥) → (( A → ⊥) → A)) → (((→ → (B → ⊥)) → ⊥) → A)) [Цепочка]
2: (((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) [MP 1, 4 ]
6: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥)) → (((→ → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) [Лемма 2]
7: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥)))) → (((→ → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥)) [Лемма 1]
8: ((A → ⊥) → (A → (B → ⊥))) → (((→ → 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: (A → ⊥) → (A → A) [MP 11, 12]
14: (A → ⊥) → (A → ⊥) [MP 10, 13]
15: (A → ⊥) → (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]

Довольно долгое доказательство!

Bye

Ответ 5

• Какая конкретная система Гильберта? Есть тонн.
• Вероятно, лучший способ - найти доказательство в секвенциальном исчислении и преобразовать его в систему Гильберта.

Ответ 6

Я использую польскую нотацию.

Поскольку вы ссылаетесь на Википедию, мы предположим, что наша основа

1 CpCqp.

2 CCpCqrCCpqCpr.

3 CCNpNqCqp.

Мы хотим доказать

NCaNb | - a.

Я использую метод проверки теоремы Prover9. Итак, нам нужно в скобках все. Кроме того, переменные Prover9 go (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))).

Мы можем объединить правила равномерной подстановки и отстранения в правило condensed отслойка. В Prover9 мы можем представить это как:

-P (C (x, y)) | -P (x) | Р (у).

"|" указывает на логическую дизъюнкцию, а "-" указывает на отрицание. Prover9 доказывает противоречие. Правило говорит словами, можно интерпретировать как "либо не так, как если бы х, то у доказуемо, или это не так, что х доказуемо, или у доказуемо". Таким образом, если оно верно, если x, то y доказуемо, первый дизъюнкт не выполняется. Если он сохраняет, что x доказуемо, то вторая дизъюнкция терпит неудачу. Итак, если, если x, то y доказуемо, если x доказуемо, то третий дизъюнкт, что y доказуемо, следует правилу.

Теперь мы не можем делать замены в NCaNb, так как это не тавтология. Не является "а". Таким образом, если положить

P (N (С (а, Н (б)))).

как предположение, Prover9 будет интерпретировать "a" и "b" как нулевые функции, что фактически превращает их в константы. Мы также хотим сделать 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 ==========================