数学基礎論についての質問(極大無矛盾理論について)

いま, 無矛盾な理論T'を取ったとき次を満たすとします.

勝手な論理式Φについて, T' ⊢Φ または T' ⊢ ¬Φ が成り立つ.

この時T'は極大無矛盾理論となるでしょうか?
(極大無矛盾理論の定義は無矛盾な理論Tにたいして, T⊆T' なる無矛盾な理論T'が存在したらT = T'となるです.)

個人的にはT'は極大無矛盾理論にはならないと思っていて, T' ⊢Φ でΦ∉T' となる論理式Φがあれば,
T'' = T' ∪ {Φ}としたら, T' ⊆ T'' かつ T' ≠ T'' となってT' は極大にならないのではないのかと思っています. しかしそのような論理式Φが本当に存在するのかなどの証明ができずに困っております.
どなたか教えていただけないでしょうか?

No.2 ベストアンサー 回答者： stomachman 回答日時： 2020/06/16 15:38

T'は無矛盾でしかも完全なんですよね。

そして、「論理式」とおっしゃっているのは命題のことでしょう。だから、T' ⊢Φとは「この公理系でΦが証明できる」ということであり、Φ∈T'とは「Φは、【この公理系で証明できる命題全体がなす集合】の要素である」ということ。両者ではT'の解釈が違うんですが、結局どっちも同じことを言ってるんであり、だから「 T' ⊢Φ でΦ∉T' となる論理式Φ」はない。
　言い換えると、命題全部の集合をLとして、公理系T'で証明できる命題全体の集合（すなわちT'の定理全体。つまりT'の理論）を U' とすると、U'= {Φ | Φ∈L ∧ T'⊢Φ} となる。このU'を指してT'と（公理系と同じ名前で）呼んでいるんでこんぐらがってる、ということかな。

この回答へのお礼

回答していただきありがとうございます。

お礼日時：2020/07/08 00:40

No.1 回答者： ありものがたり 回答日時： 2020/06/14 14:02

それは、「極大無矛盾理論」の定義に書かれている T = T' の解釈が違うんですよ。

その T = T' は、 T と T' の定理が一致することを示しているであって、
T と T' が公理の集合として一致するという意味ではありません。