Переформулирование можно не учитывать, т.к. при добавлении к системе утверждение проверяется не только на непротиворечивость, но и на невыводимость из других аксиом системы.

Обратная операция, естественно, выглядит как исключение последней аксиомы в списке. Неинтересная.

(Reply to this) (Parent) (Thread)

Я имею в виду, что полученная система может оказаться эквивалентом более простой. Получается как бы смыкание двух ветвей этого дерева. А раз дерево анизотропное, то обратная операция будет нетривиальной.

Задача-то - уменьшить набор аксиом при сохранении приемлемого уровня полноты? Исключая эвклидовы аксиомы, можно получить массу разных неэвклидовых геометрий, но к теории множеств (ну или вообще к чему-то более фундаментальному) так не придешь.

(Reply to this) (Parent)

Ну то есть не уменьшить набор количественно, а упростить, конечно же.

(Reply to this) (Parent)