Исчисление высказываний: выводимость

[MInenr]

Добрый день.

Вынужден сдавать предмет под называнием Мат. логика в качестве академической разницы "экстерном" и по этой причине во всем приходится разбираться самому.

Дошел до непосредственно Логики и что-то плотно завяз.

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

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

2. Ф-ла Бернайса:
Что значит, что х не является параметром $\psi$? В том смысле, что в реальных выводах я не встречал проверки того, что это так. Таким образом, если это просто проверка на то, чтобы не произошло коллизий с переменными, получается, что $\exists x \psi \leftrightarrow \psi$ - из Б. и аксиом (в моем понимании), но это чушь собачья мне кажется :).

Конкретный пример:
(\forall x \varphi \and \psi) \forall x varphi \psi \varphi (из 2 строки и 12 акс) \psi \and \varphi (3+4+акс) \forall x (varphi \and \psi) (Gen)

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

Спасибо.

[MInenr]

Тот пример, что Source not found и моя попытка решения:
$(\forall x \varphi \wedge \psi)$
$\forall x \varphi$
$\psi $
$\varphi$ (из 2 строки и 12 акс)
$\psi \wedge \varphi$ (3+4+акс)
$\forall x (\varphi \wedge \psi) $(Gen)

Согласно тому, как я понял аксиоматику - верно, но довольно странно.

Не подскажите верно ли я провел рассуждения?