关于含高级量词的一目谓词演算公式的■_0永真性的可判定性及其应用

在本文中我们证明含高级量词和等词的一目谓词演算公式是否(?)_0永真为可判定的并且利用这一结果证明了Nakamura在文献3]中提出的带有(?)_0个阈算子的命题演算的判定问题是可解的。 先证若干引理: 引理1 对于含有高级量词和等词的狭谓词演算公式α,恒可能行地作出一只含一级量