This paper was conceived in reaction to Soare's paper in the Bulletin of Symbolic Logic 1996. From Godel in the 30s, to Gandy, Soare, and many others today, the obvious fundamental importance of Turing's work both for logic and computer science has led to an overemphasis on his paper as the justification for the Church-Turing thesis. It is even said that Turing proved a theorem that every ?function computable by a human being in a routine way? is Turing computable. Though several have endorsed this claim, it is hard for me to see ho w it could really meet modern standards of rigor. Moreover, Gandy worried that Turing's analysis did not cover modern computers, which may use parallel processing. He proved a very complicated result (now much simplified by Byrne and Sieg) to deal with this. My paper argues that an alternative approach {once this subject has been properly analyzed and delimited} allows us to state a simple theorem that covers computations either by machines or by humans. A thesis believed by all contemporary logicians is needed for this theorem to cover all likely future cases. It should be obvious that the theorem covers all computations known hitherto.

The present paper attempts to state and prove a completeness theorem for the system S5 of [1], supplemented by first-order quantifiers and the sign of equality. We assume that we possess a denumerably infinite list of individual variables a, b, c, …, x, y, z, …, xm, ym, zm, … as well as a denumerably infinite list of n-adic predicate variables Pn, Qn, Rn, …, Pmn, Qmn, Rmn,…; if n=0, an n-adic predicate variable is often called a “propositional variable.” A formula Pn(x1, …,xn) is an n-adic prime formula; often the superscript will be omitted if such an omission does not sacrifice clarity.