公理化集合论就是寻找逻辑空间的正则基的努力（所以Goedel和Cohen证明了连续统假设与ZFC公理的逻辑无关性，ZFC集合论并不能通过其公理有限生成），而机器证明或许就是...在某个子空间中按照正则基分解一个命题当然无穷维（不可能在有限步内构造的公理）的形式系统很可能和不可重整的QFT模型一样毫无预测能力，但是我们可以继续类比EFT：就scale来说EFT表现某种局部性质，而公理化形式系统则是逻辑空间（所有命题构成的空间）的局部坐标化，，