3 papers
math.LO2009
Hindman's Theorem: An Ultrafilter Argument in Second Order Arithmetic
Henry Towsner
Hindman's Theorem is a prototypical example of a combinatorial theorem with a proof that uses the topology of the ultrafilters. We show how the methods of this proof, including top…
math.LO2008
Priority Arguments and Epsilon Substitutions
Henry Towsner
Kreisel has observed that the termination proof for Hilbert's epsilon-substitution method bears a resemblance to the priority arguments used in recursion theory. We make this preci…
math.LO2008
Functional interpretation and inductive definitions
Jeremy Avigad, Henry Towsner
Extending Gödel's \emph{Dialectica} interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theo…