Why Can Effectively Enumerated Theories Not Be Effectively Decidable?

[agapito]

Given an arbitrary effectively axiomatized theory T, the set of its wff's can be effectively enumerated. Why can it not also be effectively decidable? Under the definition of "effectively axiomatized theory" it is effectively decidable what is a wff of its language. Thus my question, thanks for all help.

 

[Evgeny.Makarov]

Given an arbitrary effectively axiomatized theory T, the set of its wff's can be effectively enumerated. Why can it not also be effectively decidable? Under the definition of "effectively axiomatized theory" it is effectively decidable what is a wff of its language.

I assume a theory $T$ is called effectively axiomatized if its set of axioms is decidable. (The following argument does not change if the set of axioms is only enumerable.) Then indeed $T$ is enumerable. We can systematically construct all derivations, and every formula in $T$ turns out to be the last formula of some derivation. It is also true that the set of all formulas in the given first-order language, whether in or outside $T$, is decidable. However, there is no a priori algorithm to determine whether a formula is in $T$. Namely, if a formula $A$ is not in $T$, then it is never proved by any derivation we enumerate, but we can not be sure that this is the case, i.e., that some future derivation does not prove it. And, as Church's theorem shows, predicate calculus is undecidable.

Note that if $T$ is consistent, effectively axiomatized and complete, which means that $A\in T$ or $\not A\in T$ for every formula $A$ in the language, then $T$ is decidable. Asked whether $A\in T$, we search through all derivations and will eventually encounter either $A$ or $\neg A$ because one or the other is in $T$. If $\neg A\in T$, then $A\notin T$ due to consistency.

Does this help?

 

[agapito]

I assume a theory $T$ is called effectively axiomatized if its set of axioms is decidable. (The following argument does not change if the set of axioms is only enumerable.) Then indeed $T$ is enumerable. We can systematically construct all derivations, and every formula in $T$ turns out to be the last formula of some derivation. It is also true that the set of all formulas in the given first-order language, whether in or outside $T$, is decidable. However, there is no a priori algorithm to determine whether a formula is in $T$. Namely, if a formula $A$ is not in $T$, then it is never proved by any derivation we enumerate, but we can not be sure that this is the case, i.e., that some future derivation does not prove it. And, as Church's theorem shows, predicate calculus is undecidable.

Note that if $T$ is consistent, effectively axiomatized and complete, which means that $A\in T$ or $\not A\in T$ for every formula $A$ in the language, then $T$ is decidable. Asked whether $A\in T$, we search through all derivations and will eventually encounter either $A$ or $\neg A$ because one or the other is in $T$. If $\neg A\in T$, then $A\notin T$ due to consistency.

Does this help?

Very helpful indeed, I appreciate it.