有限力迫伴随的可判定性

众所周知,有限力迫伴随T~f关于T_v通常是超算术的。我们证明如果T~f是∑_1-理论(相对于T_v)则它便是可判定的(相对于T_v)。十九世纪数学的成就之一,是找到一种计算方法,对每一个正的原始公式φ,得出一个无量词公式φ~*(结式),使得,这里T是域的理论。A。Robinson发展了一种模型论的方法,可证明这种结式的存在性。我们进一步说明,计算所需结式的(能行)算法的存在性,亦可用模型论力迫加以证明(由于方法的一般性)。还有其它应用。