Pinned toot

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.

Pinned toot

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.

engineers be like
2+2=4, 2*2=4
therefore +=*
qed

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

Show thread

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 :/)

Show thread

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.

Show thread

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

Show thread

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

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?

Show thread

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.

Show thread

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.

Show thread
Show older
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.