Добрый день.
Вынужден сдавать предмет под называнием Мат. логика в качестве академической разницы "экстерном" и по этой причине во всем приходится разбираться самому.
Дошел до непосредственно Логики и что-то плотно завяз.
Не поясните несколько моментов?:
1.
Существует ли "алгоритм" доказательства (без использования т. о полноте) выводимости формулы альтернативный перебору всех возможных аксиом, через которые это можно доказать + МР + правила дедукции, сечения? Например над следующим я бился довольно долго и безрезультатно:

То, что во внутренней скобке чем-то напоминает первую аксиому, а факт наличия большого числа импликаций намекает на необходимость использования дедукции. Но безрезультатно, пока что.
2. Ф-ла Бернайса:
Что значит, что х не является параметром

? В том смысле, что в реальных выводах я не встречал проверки того, что это так. Таким образом, если это просто проверка на то, чтобы не произошло коллизий с переменными, получается, что

- из Б. и аксиом (в моем понимании), но это чушь собачья мне кажется :).
Конкретный пример:

- неубедительно, мне кажется.
Спасибо.