С т. зр. теории графов это получится не дерево, однако, а ориентированный граф без циклов - одна и та же аксиома может быть присоединена ко многим системам аксиом. Ну, а мне нравится смотреть на эту конструкцию как на фрактал. Обладающий самоподобием и т.п.

(Reply to this) (Parent) (Thread)

Так вот рот открыл уже :) На граф оно тоже не сильно похоже - на каком-то этапе происходит еще и переформулирование аксиом, кроме присоединения. и как оно выглядит на самом деле, непонятно.
Еще интересно, как может выглядеть обратная операция (к "корню"), потому что она как раз и есть самая интересная.

(Reply to this) (Parent) (Thread)

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

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

(Reply to this) (Parent) (Thread)

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

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

(Reply to this) (Parent)

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

(Reply to this) (Parent)