gossip from mathland

[gusl]

Proof theory is good at translating infinitary results (ergodic theory) into finitary ones (combinatorics), thanks to Kohlenbach's revolution of the field (few structural proof theorists remain). Terry Tao is interested and published a paper related to this.
source: htowsner

Comments

[htowsner.livejournal.com]

That looks suspiciously like what we discussed this afternoon, so I may as well make that a little more concrete.

Tao has several recent papers toeing the line between ergodic and combinatorial methods of proof.

The third paper, in particular, uses a major proof theoretic technique (the Dialectica translation, the core method used in Kohlenbach-style proof theory) to make a formal connection between high quantifier complexity, non-constructive statements and low quantifier complexity constructive ones. (Tao has a very nice discussion of this on his blog.)

This is a generally applicable technique, so the main part of my thesis research has been taking a particular ergodic proof (the Furstenberg-Katznelson-Ornstein proof of Szemeredi's theorem) and "unwinding" it into a combinatorial proof. In principle, abstract proof theoretic arguments tell us that any ergodic proof (satisfying technical conditions) of a combinatorial statement has a combinatorial proof.

[kvschwartz.livejournal.com]

I didn't know he went by "Terry."