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.

  • $\begingroup$ What "Church-Turing theorem?" Google only turns up the "Church-Turing thesis," which is not a clear statement, and is not about decidability. $\endgroup$ – Thomas Andrews Jun 12 '19 at 16:41
  • $\begingroup$ For example, it is known that first order logic without any symbols other than "=" is decidable. So it is not clear what "Church-Turing theorem" the writer thinks he is violating. en.wikipedia.org/wiki/… $\endgroup$ – Thomas Andrews Jun 12 '19 at 17:45
  • $\begingroup$ 'the Church-Turing theorem that first-order logic is undecidable' is the theorem that the Entscheidungsproblem is recursively unsolvable. $\endgroup$ – Justin Jun 12 '19 at 19:36
  • $\begingroup$ There is no such theorem. There are plenty of first order logics which are known to be decidable, only that the general problem, for all first order logic, is undecidable. There are plenty of minimal first order theories that are known to be decidable. The link I provided above lists some, including the first order theory with equality and no other functions/relations. This was known to be decidable in 1915. In any event, as I point out below, there are no statements in the first order theory without equality or relations. $\endgroup$ – Thomas Andrews Jun 12 '19 at 20:09
  • $\begingroup$ On the other hand, it is know that the first order logic is undecidable if it has equality and one of: a relation symbol of arity no less than 2, or two unary function symbols, or one function symbol of arity no less than 2, established by Trakhtenbrot in 1953. [From the link above.] $\endgroup$ – Thomas Andrews Jun 12 '19 at 20:14

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.

  • $\begingroup$ If you don't know what the Church-Turing theorem is then I don't think you can make useful comments about it. I have edited my question to include citations of the relevant works of Church and Turing. All three of those works are re-printed in Davis (ed.), 1965, The undecidable, basic papers..., Raven Press. $\endgroup$ – Justin Jun 15 '19 at 18:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.