Autophagy

In Martin-Löf Type Theory (and also in logic more generally), the concept of autophagy refers to formalizing a logical system in (a slightly stronger variant of) itself.

There are many reasons to try that. For example:

• If your theory is worth its salt, then it should be able to function as a metatheory for the study of other logical systems - possibly including (a slightly weaker version of) itself.
• If your theory is sufficiently well-mechanised (e.g. type theory, higher-order logic), then this should yield a neat way to prove results about (a subset of) it on the computer.
• This is an exercise that stretches the formal theory to its absolute limit, and hence inherently fruitful and interesting in exploring a system.

Isn't that impossible?

Because of Gödel's Second Incompleteness Theorem, it is not possible to both formalize a sufficiently complicated system into itself and obtain interesting metatheoretic results about it (e.g. consistency). Thus, the theory in which we formalize a system (the metatheory) must be slightly stronger than the theory we are formalizing (the object language).

References

• The idea of autophagy is implicitly present in a lot of early work around Gödel's theorems.

• A blog post on autophagy for Homotopy Type Theory (HoTT) by Mike Shulman.

• While implicit in many previous works - e.g. Peter Dybjer's early work on Categories with Families - the programme of autophagy was explicitly articled in an article by James Chapman around 2009.

@article{chapman_type_2009,
	title = {Type {Theory} {Should} {Eat} {Itself}},
	volume = {228},
	issn = {15710661},
	doi = {10.1016/j.entcs.2008.12.114},
	journal = {Electronic Notes in Theoretical Computer Science},
	author = {Chapman, James},
	year = {2009},
	pages = {21--36}
}

• An outline of the various ways of formalising type theory in type theory is included in Ambrus Kaposi's HoTTEST seminar (22 Oct 2020) slides