Alex Simpson: On Proof by Infinite Descent

Abstract: Fermat's method of proof by "infinite descent" is a useful proof technique in number theory. But if a number-theoretic proof is to be formalized in a standard logical theory for arithmetic (such as Peano Arithmetic) then the infinite descent argument has to be recast as a proof by induction. The talk will address the question: are all proofs by infinite descent reducible to proofs by induction?

To turn this into a mathematical question, it is first necessary to formalize the notion of proof by infinite descent. Under a naive formulation, the answer to the question is trivially positive. However, in the talk, I will present an interesting and natural combinatorial notion of proof by infinite descent for which the answer is not trivial.

This talk is partly based on joint work with Brotherston (Proc. LICS 2007, J. Logic and Computation 2010). But the talk will differ from this published work, of which no knowledge will be assumed, in focusing on arithmetic. Also, there will be new content.

Vabljeni!