Три способа выявления несущественных формул в секвенциях

Первый способ основан на известном приеме спуска утончений вниз и является дальнейшим развитием лемм о “прополке” работы [1]. Второй способ основан на использовании достаточно широких классов секвенций, для которых выводимость в интуиционистском исчислении предикатов совпадает с выводимостью в классическом исчислении предикатов и верно известное свойство дизъюнкции. Этим способом можно получить, например, синтаксическое доказательство следующего утверждения. Если положительная формула $A$ выводима в теории групп при дополнительных предположениях вида
$$ \rceil\forall x_1\dots x_n\bigvee_{i<j}x_i=x_j\quad\text{или}\quad\rceil\forall x(x^n=e)\quad\text{или}\quad\rceil\forall x\exists y(y^n=x), $$
то $A$ выводима в теории групп и без этих предположений. В качестве третьего способа предложен синтаксически формулируемый критерий консервативности расширений интуиционистских аксиоматических теорий. С помощью этого критерия может быть получено, например, синтаксическое доказательство наследственной неразрешимости интуиционистской теории равенства, дополнительными аксиомами которой являются формула $\rceil\rceil\forall xy(x=y)$, все формулы вида $\rceil A\vee\rceil\rceil A$ и все отрицания формул, выводимых в классическом исчислении предикатов. Библ. – 12 назв.