treppenverstand @treppenverstand@types.pl

Here's the quote justifying my weird username. It's from Dedekind's "Was sind und was sollen die Zahlen" ("What are numbers and what are they good for?").

"But I know that, in the shadowy forms which I bring before him, many a reader will scarcely recognize his numbers which all his life long have accompanied him as faithful and familiar friends; he will be frightened by the long series of simple inferences corresponding to our step-by-step understanding [ger. Treppenverstand], by the matter-of-fact dissection of the chains of reasoning on which the laws of numbers depend [...]"

The term thus characterizes our capability of reasoning to be restricted to discrete steps and is meant to contrast the rather informal, intuition-based proofs that were the norm back in 1888 when the paper was written.

It is also a very funny sounding word.

Gaining some good insights from writing down these proofs. Will I finish in time for the movie night?

Happy World Logic Day, friends!

I have a vague idea using ordinal annotations that might be less weird than this?

My source does the other half of the proof using some extremely cursed looking intersection types? And I'm not sure even sure they prove something analogous to what I need?

Now I feel like a huge dunce...

Turns out, the proof the authors referred to ended up being useful after all...

Finally got half of that proof! Nice!

All these masks putting their bacteria or dust filtration rates on the package in big, bold letters are falsely advertising IMO. Obviously they put it there for people to think they somehow protect them from the virus.

The political compass, but it's typed vs untyped and imperative vs functional instead.

This is me on the way to finally getting that result.

Every tree without infinite branches is well-founded!!! (Assuming dependent choice on finite paths in the tree)

Also, NBE won't even give me the bound I need, so...

Me right now.

I'm not sure I can just throw NBE at this because the syntax is so weird...

Haha, simply compute the bound of the depth of the reduction tree. Surely that can't be that hard...

I might have stumbled ass-backwards into having to do a normalization proof. Turns out, just throwing lambdas into the syntax of your logic is kind of a big deal?

Actually, I can constructivize parts of it. Probably enough to get the things I actually care about to be constructive...

I have awoken to the startling realization that even though I thought I was doing proof theory, I need classical logic for my result already? That's fucked up!