Incompleteness in Linear Time.
Salvatore Caporaso, Giovanni Pani, Emanuele Covino · Zenodo (CERN European Organization for Nuclear Research) · 2000
A class LT 0 of functions computable in a proper sub_class of Lintime is defined, and formalized in a system LT0 of monadic and atomic (quantifier-free) logic. In spite of its poor computational complexity power and logical apparatus, this system has enough power to describe its own proof-predicate. Therefore it might qualify as smallest known system in which Gödel-like diagonalization can be applied. A proof is given that the identically true functions of LT 0 are productive. Hence this incompleteness phenomenon doesn t depend on the technicalities adopted to show it.