I love posts like this! Make Moar for sure. I'm finding somehow that even reading detailed stories about math I allegedly know about is enjoyable because (a) the pedagogical/story-telling aspects of it are fascinating in their own right and (b) I usually learn a (or am reminded of a forgotten) thing or two anyway.
For instance, I didn't know impredicative strong sums were inconsistent. Do you remember how the proof goes or where it comes from?
During "fast-forward through the 70s and 80s" I have a mental image of John Reynolds standing still and rapidly changing hairstyles and clothes, with a pipe sometimes appearing and disappearing. It is basically the best mental image.
Also:
Historically, Reynolds and Girard didn't discover second-order logic itself, did they? But rather its Curry-Howard analogue? I am actually not sure about this but my gut says higher order logic itself was an early 20th century thing.
Also also:
Obviously with focusing-colored glasses on, strong sums look like the "negative version" of existentials. What is the deal with this? Most recently I tend to believe that Σ just is positive, and blame its unfriendliness of negative-Σ-with-projections with spine form on a focusing error, and the difficulties of strong sums seem to corroborate that. And yet "F-ing modules" works! That is, at least there's an elaboration that makes positive sums look negative. Is this telling us anything interesting about what we can do with other positive types?
no subject
For instance, I didn't know impredicative strong sums were inconsistent. Do you remember how the proof goes or where it comes from?
During "fast-forward through the 70s and 80s" I have a mental image of John Reynolds standing still and rapidly changing hairstyles and clothes, with a pipe sometimes appearing and disappearing. It is basically the best mental image.
Also:
Historically, Reynolds and Girard didn't discover second-order logic itself, did they? But rather its Curry-Howard analogue? I am actually not sure about this but my gut says higher order logic itself was an early 20th century thing.
Also also:
Obviously with focusing-colored glasses on, strong sums look like the "negative version" of existentials. What is the deal with this? Most recently I tend to believe that Σ just is positive, and blame its unfriendliness of negative-Σ-with-projections with spine form on a focusing error, and the difficulties of strong sums seem to corroborate that. And yet "F-ing modules" works! That is, at least there's an elaboration that makes positive sums look negative. Is this telling us anything interesting about what we can do with other positive types?