Decidability of finite forcing companion (Q1176006)

It is well known that the finite forcing companion \(T^ f\) is, in general, hyperarithmetic over \(T_ \forall\). We obtain that \(T^ f\) is \(T_ \forall\)-decidable if it is \(\Sigma_ 1^{T_ \forall}\). A way of computing was found, by which for each positive primitive formula \(\phi\), a single quantifier-free (\(Q\)-free) formula \(\phi^*\) is equivalent to \(\text{Res}_ \varphi\bmod T\), where \(T\) is the theory of fields. A. Robinson developed a model-theoretic approach, showing the existence of such resultants. We go further: the existence of an algorithm for computing the required resultants can also be proved by model-theoretic forcing.