The discussion centers on the distinction between effectively enumerated theories and effectively decidable theories in formal logic. An effectively axiomatized theory T allows for the enumeration of its well-formed formulas (wff's), but it does not guarantee effective decidability of membership for arbitrary formulas. The inability to determine whether a formula A is in T stems from the undecidability of predicate calculus, as articulated by Church's theorem. However, if T is consistent, effectively axiomatized, and complete, it becomes decidable.
PREREQUISITESLogicians, mathematicians, and computer scientists interested in formal theories, decidability, and the foundations of mathematical logic will benefit from this discussion.
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.agapito said: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.
Evgeny.Makarov said: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?