The Snark, a counterexample for Church's thesis ?

Summary

In 1936 Alonzo Church put forward his thesis that recursive functions comprise all effectively calculable functions. Whereas recursive functions are precisely defined, effectively calculable functions cannot be defined with a rigor that is requested by mathematicians. There has been a considerable  amount of talking about the plausibility of Church's thesis, however, this is not relevant for a strict mathematical analysis. The only way to end the discussion is obtained by a counterexample.

The author has developed an approach to logics that comprises, but also goes beyond predicate logic. The FUME method contains two tiers of precise languages: object-language Funcish and metalanguage Mencish. It allows for a very wide application in mathematics from recursion theory and axiomatic set theory with first-order logic, to higher-order logic theory of real numbers etc. .

The concrete calcule LAMBDA of natural number arithmetic with first-order logic has been defined by the author. It includes straight recursion and composition of functions, it contains a wide range of so-called compinitive functions, with processive functions far beyond primitive recursive functions. All recursive functions can be represented in LAMBDA too. The unary Snark-function is defined by a diagonalization procedure such that it can be calculated in a finite number of steps. However, this effectively calculable function transcends the compinitive functions and presumably the recursive functions. The defenders of Church's thesis are challenged to show that the Snark-function is recursive. Another challenge asks for an example of a recursive function that cannot be expressed as a compinitive function, i.e.  without minimization.

They sought it with thimbles, they sought it with care;

They pursued it with forks and hope;

They threatened its life with a railway-share;