BHK解釈を採れば排中律批判が出てくるか

石川 @otb_btb

直観主義数学の展開や、古典数学に対する"批判"が、どの程度「直観」や「構成」の概念の内実に依存しているのかという問題設定は面白いかもしれない。

石川 @otb_btb

たとえば非可述的な定義に対する批判とかは、数学的対象が段階的に構成されるということだけしか前提にしておらず、その内実はブラックボックスでいいように見える。あるいは排中律批判なんかはBHK解釈をとれば出てくるわけで、やはり構成や直観の具体的な内実はかなりオープンだと思う

石川 @otb_btb

これに対して、直観主義的解析に登場する「選列」の概念とかは、直観や構成が何をすることなのかについて結構踏み込んでいる気がする

石川 @otb_btb

直観や構成の概念に負荷をかければかけるほど批判としての力が弱まるとも言える(「俺は直観できるもん！」みたいな世界になってくるので)。まあそれはどうでもいいのだが。

yyyy/mm/dd @Zahlangabeheft

@otb_btb えっと，「BHK解釈が数学言語の唯一の正しい解釈であるならば，排中律は成立しない」とは言えるけど，それだけじゃ排中律批判にならなくて，BHK解釈が唯一の正しい解釈だと言わないといけないですよね．「BHK解釈を取る」という言い方にそこまで含めているんですか？

石川 @otb_btb

@Zahlangabeheft 「批判」に強い意味を込めるならそうです。「BHKを取れば排中律は成り立たない」という条件的な話でも弱い意味では批判と言っていいと思います

yyyy/mm/dd @Zahlangabeheft

@otb_btb 弱い意味での批判というのがよく分かりません．例えば「無制限の決定可能性公理を取れば無制限の選択公理は成立しない」は選択公理に対する弱い意味での批判になりますか？

石川 @otb_btb

@Zahlangabeheft 批判と言っていいとは思いますがBHKの話とは意味が違います。特定の解釈を取るとどうなるかという話ではないので。

yyyy/mm/dd @Zahlangabeheft

@otb_btb 「解釈」の話は措いて，「批判」の意味がズレている気がします．「無制限の決定性公理を取れば無制限の選択公理は成立しない」（決定可能性公理は間違い）という主張は，決定性公理に思い入れのない人からはいかなる意味でも選択公理への批判としては受け取られませんよね．

石川 @otb_btb

@Zahlangabeheft そういう風に批判という語を使っても別にいいですけど、「こういう前提をとったらあなたは間違いですよ」という風なものも批判と言っていいと思いますけど。まあ純然たる言葉遣いの問題ではないでしょうか

yyyy/mm/dd @Zahlangabeheft

@otb_btb よく分からなかったのですが，「こういう前提をとったらあなたは間違いですよ」の「こういう前提」が一切の客観的説得力を欠いていても，批判として成立する，と言っているのですか．

yyyy/mm/dd @Zahlangabeheft

@otb_btb あるいは，「こういう前提をとったらあなたは間違いですよ」の「こういう前提」は批判される側にとって説得力を持つ必要はない（が，客観的にはもちろんある程度の説得力が必要），と言っているのですか．

石川 @otb_btb

@Zahlangabeheft そんなにこだわりがないので深く考えてませんがこっちに近いです。

yyyy/mm/dd @Zahlangabeheft

@otb_btb 「こういう前提」には一定程度客観的な説得力が必要だと認めてもらえるわけですね．ではBHKの話に戻りましょう．「BHK解釈を取れば排中律は成立しない」と言うとき，前提を省略せずに言うと「BHK解釈は唯一の正しい解釈である」にならざるを得ないと思いますがどうですか．

石川 @otb_btb

@Zahlangabeheft なぜですか。繰り返しますが、僕は別に「批判」という言葉にそんなにこだわりはないですが。

yyyy/mm/dd @Zahlangabeheft

@otb_btb 「なぜ」というのは何を聞いているんですか．「批判」については，認識にズレはないということで決着したつもりです．

石川 @otb_btb

@Zahlangabeheft そもそも、元ツイートの趣旨は、直観主義の話をするときに構成や直観の概念の内実をどこまでオープンにできるかというものであって、BHKが唯一正しい解釈と仮定しなければならないかどうかという話はこの論点に直接関係あるものでもないかと思いますが、如何ですか

石川 @otb_btb

@Zahlangabeheft 「ならざるを得ない」と仰る理由を聞いたつもりでした。

石川 @otb_btb

@Zahlangabeheft なので、その点に拘るポイントが僕にはよくわかりません。

yyyy/mm/dd @Zahlangabeheft

@otb_btb 「直観主義の話をするときに構成や直観の概念の内実をかなりの程度オープンにできる」という論点は同意できるのですが，「排中律批判なんかはBHK解釈をとれば出てくるわけで」という論点がそれとどう絡むのか分からないし，そもそも「BHK解釈をとれば排中律批判が出てくる」→

yyyy/mm/dd @Zahlangabeheft

@otb_btb →というのが何を言っているのかよく分からないので，質問しました．とりあえず「BHK解釈をとれば排中律批判が出てくる」が何を言っているのかを確かめるのが先だと思って，「構成や直観の概念の内実をかなりの程度オープンにできる」という主張は取りあえず措いてます．

yyyy/mm/dd @Zahlangabeheft

@otb_btb それから付け加えると，「批判」に強い意味や弱い意味がある，と言い出したのは私ではなくて君の方です．私は「えっ，批判にそんな意味合いの違いがあるのか」と思って聞いて行っただけで，「批判」という言葉に元々拘りはないです．

石川 @otb_btb

@Zahlangabeheft A or not AをBHK解釈で読めば、これが証明されるためには、Aの構成かnot Aの構成が必須である。しかし、Aにもnot Aにも構成を用意できないケースがある。

石川 @otb_btb

@Zahlangabeheft 従って、BHK解釈を施すことを前提とすれば、排中律は全面的に妥当ではない。こういう話です。

石川 @otb_btb

@Zahlangabeheft この話で「構成」の概念に掛かっている負荷は、A or not Aの構成がAの構成かnot Aの構成を含んでいるというような、かなり形式的な話だけであり、例えば二一性の直観がどうしたみたいな話は完全に放っておける。そういうことです。