Lampert's supposed solution to the Entscheidungsproblem

Question

Here: http://www2.cms.hu-berlin.de/newlogic/webMathematica/Logic/FOLDECISION2.pdf Timm Lampert claims to refute the Church-Turing theorem that first-order logic is undecidable. I'm wondering where the first error is!

Perhaps it would help Thomas Andrews if I gave references to where the unsolvability of the Entscheidungsproblem was first demonstrated. (Though I had supposed this was well known.)

Church, 1936a: 'An unsolvable problem of elementary number theory', American Journal of Mathematics, 58: 345-363.

Church, 1936b: 'A note on the Entscheidungsproblem ', Journal of Symbolic Logic, 1: 40-41.

Turing, 1936: 'On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, 42: 230-265.

Answer 1

It is unclear what the author thinks the "Church-Turing theorem" is. There is a "Church-Turing thesis," which has no formal definition, and does not really apply to decidability, except in the sense that decidability is a question of computability.

More importantly, first order logic with no identity, relations or functions is actually an empty logic - the set of valid "formulas" is empty in the usual definition of first order logic's "terms" and "formulas."

This is because the atomic "formulas" are of the form:

• $t_1=t_2$ where $t_1,t_2$ are terms (only allowed if you have identity)
• $P(t_1,t_2,\cdots,t_n)$ where $P$ is an $n$-ary relation and the $t_i$ are terms.

There are no such formulas in our logic because there is no identity nor any relation $P.$ But all formulas must be built from these formulas.

Since it has no statements, this theory is definitely decidable, in that we can list all true and all false formula, since both sets are empty.

So it is unclear what the author is trying to prove, nor what ("the Church-Turing theorem") the author is trying to disprove.

I suppose you could add $0$-ary relations $P,Q,R,\cdots$ and get a theory that is essentially predicate calculus. The first order quantifier symbols $\exists,\forall$ would essentially be meaningless, and we can reduce this question to the decidability of predicate calculus, which is known to be decidable.

Aside: First order logic with identity (equality) and no (other) relations or functions is known to be decidable.