内包記法についての考察
発端
@tenapyon f(A) = {f(x)|x∈A}, f(B) = {f(x)|x∈B} としたら f(A)∩f(B) = {f(x)|x∈Aかつx∈B} = {f(x)|x∈A∩B} = f(A∩B) というのは誤りでしょうか。
— 結城浩 (@hyuki) January 6, 2015
https://twitter.com/kagami_hr/status/552436576576602113
https://twitter.com/kagami_hr/status/552428467711926273
疑問
- 《省略記法》は間違いやすいとしたら、その理由は何か
- 《省略記法》は本当に誤りなのか
なぜ間違えたのか
しかし
ここでもし《正式な内包的記法》を用いるなら
となり、間違いは起こらない。
公理と記法
素朴に考えれば という記法(集合の内包的記法)は、が真となるようなを集めた集合を表す記法となるが、このような集合の作り方を許すと、パラドックスが生じてしまう。(集合論 - Wikipedia)パラドックスを避けるため、公理によって集合を得る操作を限定する。(公理的集合論 - Wikipedia)
公理系の各公理は、記法の根拠を与えることになる。例えば、空集合の公理は記法 の根拠となるし、対の公理は記法 の根拠となる。《正式な内包的記法》 は、分出公理が根拠となっている。この時、縦棒の左側にある は、《正式な内包的記法》の一部であって命題ではない。
分出公理の代わりに、置換公理を公理とすることができる。置換公理を根拠として という《別の内包的記法》を定義する。この時、縦棒の右側にある は、この《別の内包的記法》の一部であって命題ではない。《別の内包的記法》は置換公理が根拠となっている記法であるから、《正式な内包的記法》の省略記法になっているわけではない。
《正式な内包的記法》を《別の内包的記法》を使って定義することもできる。
ここで
内包的記法が2つあるのは面倒なので、1つにまとめた記法があると便利だ。《別の内包的記法》は、Haskellのリスト内包記法と同じ書き方になっているので、モナド内包記法の構築方法で拡張できる。
適宜組み合わせて のような記法も、意味を定義できる。