Perché la logica del primo ordine (senza aritmetica) è solo una validità ricorsivamente enumerabile e non ricorsiva?

Question

La "complessità computazionale" di Papadimitriou afferma che la validità, il problema di decidere se una formula logica (senza aritmetica) del primo ordine è valida, è ricorsivamente enumerabile. Ciò deriva dai teoremi di completezza e solidità, che equivalgono alla validità e alla teorema, essendo quest'ultimo il problema di trovare una prova per una formula, che in precedenza era stato dimostrato essere ricorsivamente enumerabile.

Tuttavia, non vedo perché anche la validità non sia ricorsiva, perché data una formula $ phi $, si potrebbe eseguire due macchine Turing per teorema, una su $ phi $ e l'altra su $ neg phi $, contemporaneamente . Poiché almeno uno di essi è valido, è sempre possibile decidere se $ phi $ è valido o non valido. Cosa mi manca?

Nota: questa domanda si riferisce alla logica del primo ordine senza Aritmetica, quindi il teorema di incompletezza di Gödel non ha un cuscinetto qui.