Anders Lundstedt: Natural induction—a model-theoretic study?

Abstract

I present various notions of inductiveness—the original notion is due to Hetzl and Wong (2018). When suitably formulated, a non-inductiveness statement provides a precise and sensible sense in which a corresponding statement about the natural numbers is unprovable by straightforward induction. Thus by proving a suitable non-inductiveness result, one may show, in a precise and sensible manner sense, that some fact about the natural numbers is unprovable by straightforward induction.

I discuss the conceptual issue of how to formulate suitable non-inductiveness statements—where by ‘suitable’ I mainly mean formulations that actually provide the ‘sensible’ in my use of ‘precise and sensible sense’ above. Then I present techniques for proving non-inductiveness results: these are based on constructing certain kinds of non-standard models of first-order arithmetic.

I conclude by stating some non-inductiveness results that I have proved and some non-inductiveness conjectures that I hope to prove. If the conjectures turn out provable in the way I hope and believe, then that would perhaps justify removing the question mark from the ambitiously sounding paraphrase that is the title of this talk.

REFERENCES

• Hetzl, Stefan, and Tin Lok Wong (2018): Some observations on the logical foundations of inductive theorem proving. In: Logical Methods in Computer Science 13(4), pp. 1–26. (Corrected version of paper originally published Nov 16, 2017.)

My research page  has some very outdated material. Perhaps some new material will appear there in time before the talk.