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

yoriyuki @yoriyuki

「5分でわかる直観主義数学」新しいブログ記事です。形式的な公理系よりも「気持ち」について書いてみました。 yoriyukiy.com/2018/09/26/5/

Jimmy Aames @asonosakan

直観主義では「人間が行う証明という活動を離れた命題の真偽というものは意味がない」って言われると，構文論と意味論の区別を前提にする完全性定理のような結果が直観主義論理では無意味になってしまう気がするんだけど，どうなんだろう．

Jimmy Aames @asonosakan

もし直観主義が，ある命題φが「真であること」（任意の解釈によって充足されること）と，φの「証明を構成できること」を同一視する立場なのだとすれば，「φは任意の解釈によって充足される→φの証明を構成できる」という完全性定理のステートメントはトートロジーにならない？

カムショット・マリファナコカイン・ハードコアポルノ @amntksr

@asonosakan 任意の解釈で充足されることの証明には「公理からの演繹」以外の方法があるかもしれないのでトートロジーではないです (或る命題が任意の標数 0 の代数閉体で充足されることを示すには, 複素数体でのみ確認すればよく, そこでは解析学的な手法が使える.)

Jimmy Aames @asonosakan

@amntksr Φを文集合（今の例だと任意の標数0の代数的閉体で充足される文集合），φを文だとして，Φ⊨φを示す方法は，Φ⊢φを示す方法以外にも，別の文集合Φ′（今の例だと解析学の公理系？）からφを証明する方法もあるので，「φの証明を構成できること」は必ずしもΦ⊢φとイコールではない，ということですかね．

yyyy/mm/dd @Zahlangabeheft

@asonosakan 直観主義は「φが任意の解釈によって充足されること」と「φの証明を構成できること」を同一視する立場ではないので大丈夫です。強いて言えば、「φが任意の解釈によって充足されること」が真であることと「φが任意の解釈によって充足されること」が証明可能であることを同一視するだけです。

ディレッタンティズムの倫理と聖霊の働き @PhlebotomeH

@Zahlangabeheft @asonosakan 直観主義と直観主義論理は自然に同一視して良いものなんでしょうか。直観主義論理を採用するからといって可能世界意味論が無意味になるとは思いませんし、しかしながらBrouwerのような思想の持ち主は如何にも無意味と断言しそうな気がします。

yyyy/mm/dd @Zahlangabeheft

@PhlebotomeH @asonosakan もちろん、直観主義と直観主義論理は別物として考えた方がよいです。直観主義論理はあくまで形式体系のベースになってる規則であり、直観主義そのものは数学思想で、どちらかと言えば形式体系の解釈に関わるので。可能世界意味論はメタ論理で古典的推論を使わなければバンバンやって結構でしょう。

Jimmy Aames @asonosakan

@Zahlangabeheft 「φが任意の解釈によって充足されること」が真であることと「φが任意の解釈によって充足されること」が証明可能であることを同一視する，というのはよく分かりません．「『φが任意の解釈によって充足されること』が真であること」は「φが任意の解釈によって充足されること」と同じでしょうし，

Jimmy Aames @asonosakan

@Zahlangabeheft 「『φが任意の解釈によって充足されること』が証明可能であること」，つまり「φは恒真である」が証明可能であることも，結局「φは証明可能である」に帰着する気がします．

yyyy/mm/dd @Zahlangabeheft

@asonosakan その「帰着」はトリビアルですか？

yyyy/mm/dd @Zahlangabeheft

@asonosakan 「φが任意の解釈によって充足されること」と証明できることと、直観主義論理でφが証明できることの一致は、直観主義者であれ誰であれ証明が必要でしょう。あと、「同一視」についてのコメントが混乱を招いてしまったようで失礼しましたが、→

yyyy/mm/dd @Zahlangabeheft

@asonosakan →証明可能性と同一視される真理は、形式言語の式に対して定義される述語「任意の解釈によって充足される」ではなく、有意味な言明に述定される述語「真」だ、という趣旨でした。

yyyy/mm/dd @Zahlangabeheft

@asonosakan ×「φが任意の解釈によって充足されること」と証明できること 〇「φが任意の解釈によって充足される」と証明できること でした。

Jimmy Aames @asonosakan

@Zahlangabeheft 健全かつ完全な論理体系だと，「φは恒真」と「φは証明可能」は同値なので，直観主義論理が健全かつ完全なら（これは確かに証明が必要ですが），「φは恒真である」が証明可能 ⇔ 「φは証明可能」が証明可能 ⇔ φは証明可能，とならないですかね．

yyyy/mm/dd @Zahlangabeheft

@asonosakan そりゃそうなりますが（ただし直観主義者にとっての健全性・完全性のステートメントは考える必要があり、述語論理の完全性は問題あり）、完全性定理が無意味にならないかどうかが当初の問題でしたよね。もう「無意味にはならない（証明が必要）」ということで結論が出ているのでは？

Jimmy Aames @asonosakan

@Zahlangabeheft 完全性定理が直観主義論理で成り立つとして，直観主義の立場だとそれはトートロジカルな空文になってしまうのではないか，というのが当初の疑問でした．証明したり，上のように使用できるからといって，それが空文でないことにはならないと思うのですが．

yyyy/mm/dd @Zahlangabeheft

@asonosakan つまり、完全性定理の重要性を、「真である」の意味に基づいて論理規則の正当化することだ、と説明することができなくなる、ということでしょうか。それはその通りだと思います。ただ、だからといって何の重要性もないと言ってしまうのは早計でしょう。

Jimmy Aames @asonosakan

@Zahlangabeheft そうですね，完全性定理を推論規則の正当化に使えなくなってしまうというのもありますし，それが「A → A」という形をしていることが単に気持ち悪いというのもあります．もちろん直観主義者が完全性定理に何の重要性もないと考えているとは思っていないです．

yyyy/mm/dd @Zahlangabeheft

@asonosakan 完全性定理が「A → A」という形をしている、というのがよく分かりません。形の上ではむしろ、意味論的真理と証明可能性は全く作りの違う別の述語で、それは直観主義を取ろうと取るまいと変わらないような。

Jimmy Aames @asonosakan

@Zahlangabeheft そうなんですか．直観主義は意味論的真理と証明可能性を同一視する立場だと思ってました（もちろん一口に直観主義といっても様々な立場があることは承知してますが）

yyyy/mm/dd @Zahlangabeheft

@asonosakan さっきも言いましたが、証明可能性と同一視される真理は、形式言語の式に対して定義される述語（意味論的真理）ではなく、有意味な言明に述定される述語「真」であり、後者の真理概念が意味論的真理概念で捉えられているかどうかは完全性定理を通じて確かめられるべき問題――と考えればよいのでは。

yyyy/mm/dd @Zahlangabeheft

@asonosakan 何となく、話の感じからして、われわれが普通に使っている真理概念をタルスキの定義に代表される意味論的真理の概念と同一視されているような印象を受けますが、あくまで意味論的真理概念はわれわれの真理概念の1つの分析でしょう。

Jimmy Aames @asonosakan

@Zahlangabeheft 「有意味な言明に述定される述語「真」」というのは，私たちが日常的に使う真理概念のことでしょうか．意味論的真理概念があくまでこれの一つの分析だというのはその通りだと思いますが，数学に限って言えば，意味論的真理以外の意味で「真である」という述語が使われることはあるのでしょうか．

yyyy/mm/dd @Zahlangabeheft

@asonosakan いや、真理概念が意味論的真理概念として分析できない、と言いたいわけじゃないですよ。真理概念が意味論的真理概念として分析できるかどうかはノントリビアルだと言っているんです。それさえ言えれば、真理と証明可能性の同一視は、直ちに意味論的真理と証明可能性の同一視にはならないでしょう。