We know from Church's Theorem that L_1 is Turing-undecidable.And we now know from Olmsted's theorem that L_0 isTuring-decidable. AI of today, and specifically AI as it relates tothe Web, particularly the Semantic Web, is often connected toformal logics \"between\" L_0 and L_1. Let us define the logicL_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'sTheorem apply?
