直観主義では完全性定理はトートロジーになる？

yyyy/mm/dd @Zahlangabeheft

@asonosakan それに、直観主義者にとって意味論的真理概念と呼べるものが何なのかはちょっと問題があって、述語論理に対するクリプキ意味論の完全性の普通の証明は直観主義的に問題があり、直観主義者の観点から見て標準的なものはなかったはず。

Jimmy Aames @asonosakan

@Zahlangabeheft 私自身，数学では真理概念を意味論的真理と同一視していた（例えばRiemann予想の主張を形式化した文が「任意の解釈によって充足される」と言うのと，「Riemann予想は真である」と言うのは同じだと思っていた）のですが，それは必ずしも自明ではないんですね．

けーた @ke_ta3

@asonosakan クリプキモデルに関する直観主義論理の完全性定理は有意味ではないですか？

けーた @ke_ta3

@asonosakan BHK解釈を直観主義論理の意味論だと考えた場合、その完全性を考えるのは無意味では、ということでしょうか？

Jimmy Aames @asonosakan

@ke_ta3 BHK解釈というよりは，その背後にある，「証明」や「構成」といった操作的概念によって文の成否を問う立場に則れば無意味になるのではないか，ということです．全然詳しくないのですが，BHK解釈は直観主義論理の意味論なんでしょうか？

けーた @ke_ta3

@asonosakan あくまで形式化された直観主義論理の話に限れば、クリプキモデル等の健全性・完全性が成り立つ意味論が与えられると、例えばある理論が直観主義論理上で無矛盾であることはその理論の具体的なモデルを構築することによってわかりますので、実用的な意味は明白にあるかと思います。

けーた @ke_ta3

@asonosakan BHK解釈はあくまで直観主義論理のインフォーマルな解釈で、完全性・健全性などを考えられるような意味論ではないのでは、と思っていましたが、そちらに関しては私も全く詳しくないので少し調べてみないとわからないですね。

けーた @ke_ta3

@asonosakan 完全性定理の話とは別に、哲学的立場としての直観主義にとって構文論と意味論の区別はどのように捉えられるのか、その区別は受け入れられるのか、というのは面白いトピックだと思います。私は素人なので何も言えませんが。

Jimmy Aames @asonosakan

@ke_ta3 形式化された直観主義論理で完全性定理が実用的な意味を持つことは全く疑問視していないです．私が気になったのは，仰る通り，哲学的立場としての直観主義にとって構文論と意味論の区別がどう捉えられるのかという点です．この問題が現れる一例として完全性定理に言及してみました．

けーた @ke_ta3

@asonosakan なるほど、意図がわかりました。ありがとうございます。哲学的立場としての直観主義（ここではBHK解釈？）とHeytingが形式化した直観主義論理は一旦区別しないと議論が混乱しがちですね。

yyyy/mm/dd @Zahlangabeheft

@asonosakan それが自明だとしたら、タルスキの功績とは一体何だったのか、ということになりませんか？

Jimmy Aames @asonosakan

@Zahlangabeheft Tarskiの真理論は，形式言語における真理概念であれば当然満たすべき条件を明示化したという風に理解しています．なので，数学における意味論的でない真理概念としてどういうものがあり得るのか想像できません．

yyyy/mm/dd @Zahlangabeheft

@asonosakan ええと、たぶん「意味論的真理概念」の意味が私とずれていると思うんですよ。私が「意味論的真理」と言うときは、きちんと定義された形式言語にタルスキ意味論とかクリプキ意味論といった形できちんと定義された真理概念を総称していて、→

yyyy/mm/dd @Zahlangabeheft

@asonosakan →そういう定義が与えられる前に「意味論的真理」というものがあるとは考えていないんですよね。だけど、そういう定義が与えられる前から、「Riemann予想は真」とは言えていたわけで、その場合の「真」は、私の言葉遣いでは「意味論的真理」ではないことになる。→

yyyy/mm/dd @Zahlangabeheft

@asonosakan →だけど阿蘇さんはたぶん、意味論的真理の定義は何かある特定の存在者みたいなものを指していて、定義される前からその存在者はあって、「Riemann予想は真」と言うときにはその存在者に言及している、といった考えを持っているように見える。

Jimmy Aames @asonosakan

@Zahlangabeheft 私は確かにそう考えてます．ただ形式的な意味論が定義される前に「Riemann予想は真」という言明があったとして，その言明にある「真」の概念を，その意味論が適切に捉えていないとしたら，その意味論を導入することで一体何をやっているのか分からなくないですか．

yyyy/mm/dd @Zahlangabeheft

@asonosakan 意味論が直観的な真理概念を適切に捉えることを目指す、というのは誰も否定しないでしょう。ただ、予めきちんと定義された概念があるわけではないので、真理概念が満たしてほしい性質とか条件を適宜取捨選択してそれなりに大事そうな概念が得られれば十分で、意味論的真理概念という存在者は不要かと。

yyyy/mm/dd @Zahlangabeheft

@asonosakan いやあってもよいですが、そういう存在者を最初に措定しないような立場というのも十分考えられると思いますけど。

yyyy/mm/dd @Zahlangabeheft

@asonosakan すみませんさらに続けます。

yyyy/mm/dd @Zahlangabeheft

@asonosakan で、直観的な真理概念を捉えるやり方として、タルスキ意味論とかクリプキ意味論みたいな表示意味論を経由した真理概念の定義もありうるし、証明の存在として真理概念を定義するやり方もある。直観主義の場合に、→

yyyy/mm/dd @Zahlangabeheft

@asonosakan →クリプキ意味論について健全性と完全性が証明できれば（直観主義的にはできないけど）、両方のやり方で捉えた真理概念が一致することが分かってハッピーで、そうなった暁には真理概念を意味論的真理概念としても証明可能性としても捉えられることになる。というので特にミステリーはないような。

yyyy/mm/dd @Zahlangabeheft

@asonosakan あと、そもそも「証明を離れた真偽はない」と言っても、直ちに証明可能性で真理を定義することになるわけではなくて、結果的に証明可能性を越えないような仕方で意味論的に真理を定義したってよいと思います。

Jimmy Aames @asonosakan

@Zahlangabeheft Kripke意味論で健全性と完全性を証明できるとしても，そもそもKripke意味論のような表示的意味論を，直観主義の哲学的立場で受け容れることができるのかという疑問がやはりありますね．「結果的に証明可能性を越えないような仕方で意味論的に真理を定義」するというのはどういうことでしょうか．

yyyy/mm/dd @Zahlangabeheft

@asonosakan クリプキやベートみたいな意味論を与えて、直観主義論理に対して健全性と完全性を証明できたとしたら、「結果的に証明可能性を越えないような仕方で意味論的に真理を定義できた」と言ってよいのでは、という気持ちでした。実現はしていませんし、やっぱし本流はBHK路線だと思いますが。

yyyy/mm/dd @Zahlangabeheft

@asonosakan 表示的意味論そのものが直観主義の哲学的立場からは受け付けられないとは思わないです。表示的意味論など所詮は数学理論ですから、構成主義数学の中で表示的意味論を作ればよいだけです。