University of Connecticut

Events Calendar

Connecticut Logic Seminar
Coding overhead and the pitfalls of formalization
Benedict Eastaugh (Munich Center for Mathematical Philosophy)

Monday, April 1, 2019
4:45pm – 6:00pm

Storrs Campus
MONT 214

Reverse mathematics purports to demonstrate what axioms are necessary in order to prove theorems of ordinary mathematics: real, complex, and functional analysis, countable algebra, infinitary combinatorics. This involves formalizing the basic notions of these fields in the language of second order arithmetic, thus limiting what can be formalized to mathematical objects which admit of countable representations or codes. That a formalized counterpart of an ordinary mathematical theorem such as the Heine-Borel covering theorem implies the set existence axiom WKL (weak Konig’s lemma) is usually glossed as “WKL is necessary to prove the Heine-Borel covering theorem”. But to justify the use of this gloss, and indeed the central claim of reverse mathematics to be determining the axioms necessary to prove ordinary mathematical theorems, the coding involved in the formalization of these theorems in second order arithmetic must satisfy certain conditions that ensure their faithfulness. In particular, the coding should not affect what axioms are necessary to prove a given theorem. In this paper we study the coding overhead of additional principles that are necessary to prove the extensional correctness of a coding, and argue that several codings used in reverse mathematical practice fail to be faithful when evaluated in the context of specific theorems from analysis and topology.


Reed Solomon,

Connecticut Logic Seminar (primary), UConn Master Calendar

Control Panel