I didn't like how I blasted through naturals and lists so instead I'm redoing them with "Tees" and adding the ugliest colours because I can

Show thread

re: Corpse Reviver 

Doing some very insightful and thoughtful annotations

Show thread

Today's mood
I really thought Sizes were just going to be inductives and that's that

Show thread

How should I fix that second sentence? ⊡!A⊢Γ and !⊡!A⊢Γ imply each other (by maximality, as it says), I'm trying to figure out what the intent of "for then" was

Oh here's the rules I settled on
The first two "facts" are derivable by induction and the third one is basically a macro for a derivation where you stick those Ds where the ps are in your tree, but I'm not sure about the fourth fact or how it's proven
It makes sense that you can replace a formula by an equivalent one but idk how to get "inside" C to do the replacement
I suppose it must be some proof by induction too

Show thread

Okay I don't get this fourth one
Like I can see why it's invalid because B is just a random arbitrary formula unrelated to A but I don't get why they decided to state this particular schema
Like ?? what's the point of stating it

Show older
types.pl

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