RESEARCH ARTICLE

Some Applications of Lawvere’s Fixpoint Theorem

  • LI Xi
Expand
  • Department of Philosophy, Central South University, Changsha 410083, China

Published date: 15 Sep 2019

Copyright

2019 Higher Education Press and Brill

Abstract

The famous diagonal argument plays a prominent role in set theory as well as in the proof of undecidability results in computability theory and incompleteness results in metamathematics. Lawvere (1969) brings to light the common schema among them through a pretty neat fixpoint theorem which generalizes the diagonal argument behind Cantor’s theorem and characterizes self-reference explicitly in category theory. Not until Yanofsky (2003) rephrases Lawvere’s fixpoint theorem using sets and functions, Lawvere’s work has been overlooked by logicians. This paper will continue Yanofsky’s work, and show more applications of Lawvere’s fixpoint theorem to demonstrate the ubiquity of the theorem. For example, this paper will use it to construct uncomputable real number, unnameable real number, partial recursive but not potentially recursive function, Berry paradox, and fast growing Busy Beaver function. Many interesting lambda fixpoint combinators can also be fitted into this schema. Both Curry’s Y combinator and Turing’s Θ combinator follow from Lawvere’s theorem, as well as their call-by-value versions. At last, it can be shown that the lambda calculus version of the fixpoint lemma also fits Lawvere’s schema.

Cite this article

LI Xi . Some Applications of Lawvere’s Fixpoint Theorem[J]. Frontiers of Philosophy in China, 2019 , 14(3) : 490 -510 . DOI: 10.3868/s030-008-019-0029-6

Outlines

/