In: Computer Science
We know from Church's Theorem that L_1 is Turing-undecidable. And we now know from Olmsted's theorem that L_0 is Turing-decidable. AI of today, and specifically AI as it relates to the Web, particularly the Semantic Web, is often connected to formal logics "between" L_0 and L_1. Let us define the logic L_1^cdot as first-order logic but with no function symbols allowed, and having relation symbols that are all unary. Your question is: Is theoremhood for L_1^cdot Turing-decidable, or does Church's Theorem apply?
Solution:
It is given that is Turing-unecidable and is Turing decidable from Olmsted's theorem.
= first-order logic but with no function symbols allowed, and having relation symbols that are all unary.
First of all it needs to be understood what a Turing decidable language is -
A language L that is decided by a Turing machine means if there is a Turing machine M such that M halts and accepts on any input w ∈ L, and M halts and rejects on input input w L; i.e., looping cannot happen.
This means the language is closed under union, intersection and other set operations but is not as it is not turing decidable.
Since is turing undecidable, it is confirmed that any set operation on can't be Turing Decidable.
So, the answer is big NO that = first-order logic is not Turing Decidable.
Moreover, Church's theorem can be applied to find whether it is Turing Decidable or not.