2023.11.20

https://gyazo.com/36933129f9721623e6e38a06388c5cbc

何してるの？

やった

とりあえずPRをドラフトで出した．

メモ

導出可能性条件を極限まで抽象化したものを考えるべきなのだろうか．

$ \mathbf{D1}_{\Phi} \colon T \vdash \sigma \implies U \vdash \Phi(\ulcorner \sigma \urcorner)

$ \mathbf{D2}_{\Phi} \colon T \vdash \Phi(\ulcorner \sigma \to \pi \urcorner) \to (\Phi(\ulcorner \sigma \urcorner) \to \Phi(\ulcorner \pi \urcorner))

$ \mathbf{D3}_{\Phi} \colon T \vdash \Phi(\ulcorner \sigma \urcorner) \to \Phi(\ulcorner \Phi(\ulcorner \sigma \urcorner) \urcorner)

思った

いくら全世界に公開されているからといってもほとんどの人間はツイッターに関して閉じたコミュニティ（の特定のコンテクストの数人）に向けて発信していているのに普通にそれを拾い上げて勝手に編纂したりコンテクストを付与したりする場を提供するTogetterとかって普通に極悪サービスだと思う

メモ