treppenverstand @treppenverstand@types.pl

I do math because it means I need to do less annoying garbage than when programming. I do Proof Theory because I'm still an annoying garbage doer at heart.

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.

Finishing within the desired timeframe is completely out of question now. Please kill me.

I just found out that what I was working on the last few weeks does not work at all and was a complete waste of time AMA

Also, taking @bruceiv's advice to heart, I made an additive scoring system for the big proof exercise. This saved me tons of time because now I could just spend 3 minutes scanning for the 7 things you had to do to get the points instead of having to spend 10 minutes to parse all of the proof (oftentimes 3-4 pages). At least in the 85% of cases where the proof strategy was somewhat orthodox. Can recommend and will do it like this again!

I think I've seen most (semantic) methods of proving that something is a classical (propositional) tautology. Some of the are weirdly awkward.

Students please don't prove A by assuming ~A and then just proving A without ever using ~A to arrive at a contradiction to ~A challenge 2020

OK, I found something better now. I suppose I can learn all of this in one day. Let's put this aside until the weekend (which is super close already :/)

So, it seems the lecture notes the professor uses are only half finished and in broken English (with some French bits remaining). Less than ideal.

I should start reading up on linear logic, huh?

I guess I'll just massage this long enough to be able to throw König's Lemma at it?

Showing the existence of infinite paths is quite annoying, actually.

*bot reeeee!

Makes me wonder how one actually decides intuitionistic (propositional) tautologies. Tableaux won't work, right? I guess we can just search through the cut-free sequents for a formula? As far as I know, there is no nicely canonical Heyting algebra analogous to "the" Booleans we can check validity on, right?

Excellent idea: Build an "intuitionistic logical tautologies" not but it's just double-negation-translated classical tautologies.

I unironically love it when students put a check mark somewhere in their solution (like "side conditions satisfied ✔"). The enthusiasm in that little symbol is just too nice. Even better in the rare case when they're wrong, which is extremely funny.

Just asking "Hey, do you know someone who still does this that I could talk to?" seems kind of rood.

If somebody has published like one interesting paper in the last 20 years, it probably makes no sense to contact them about a PhD position, regardless of how cool it is, right?

So, I've basically made no progress at all yet, except realizing that I actually made very little progress.