Idea for counterexample to Church's thesis
Let's get the idea of constructing a counterexample to Church's thesis. Start with decimal numbers and conventional (imprecise) notation, where small letters a,b,c,… denote number-constants and x,y,z,… number-variables. Primitive recursive functions are given by certain decimal numbers, that are called primitive-codes, they are written as a code number followed by an input of variables in paranthesis, positions are separated by semicolons, e.g. 1(x) or 201(x) or 22011(x;y) . If the preceding number is not a primitive-code the function is taken as the the zero-function, i.e. its value is always 0 , e.g. if 375 is not a primitive-code for all x holds 375(x)=0 .
Given this definition one can also talk about so-called processive function e.g. y(x) where the code-position is filled with a variable (these functions are called processive). Together with compositions that can be done both in code-position and input-position one gets function-schemes, e.g. 22011(x;1(y)) or x(201(x)) or y(x)(y) . The functions that are constructed in this way go far beyond primitive functions, e.g. it is not too complicated to find a code am such that am(x)(x) is the Ackermann-function. Everything can be calculated effectively.
The unary-function schemes are strings that are constructed from 14 characters x ( ; ) 0 1 2 3 4 5 6 7 8 9 and therefore correspond to quadrodecimal numbers. These means that certain quadro-decimal numbers are unary-scheme-codes for unary-function schemes. Now one can define a unary-function for every decimal number whose quadrodecimal is a unary-scheme-code: just translate the unary-scheme-code into the corresponding unary-function scheme and evaluate it by replacing x by the input-number. And one can extend the definition to all decimal numbers simply by putting the value of functions that have not a proper unary-scheme-code to 0 .
In this way one constructs a unary function of x for every decimal number y , which means that one gets a binary-function, let's call it Boojum(y;x) - notice the capital initial. For certain values of y one gets the primitive recursive function, for certain values the processive functions, and overwhelmingly often the zero-function. But this is not the end: one can outdiagonalize them by the function Snark(x)=Boojum(x;x)+1 and this is the proposed counterexample, as it is not primitive and not processive. But it can be calculated effectively.
An analysis of the above idea shows that one needs a precise way of talking both in object-language and metalanguage. This is accomplished in the publications of this section by using the FUME method with Funcish and Mencish.