メタ定理の証明はどこでなされているか？
-
- いいね！0
y.
@waidotto
@Rits_math_3rd メタレベルで「ZFCの公理に相当することはすべて正しい」と仮定すれば，メタ定理としてのコンパクト性定理・完全性定理が従う，という認識でいいんでしょうか
2016-06-17 04:43:05
D1マン
@11029_8904
@waidotto いえ、私の認識としては1階述語論理といったものはZFCなどを議論するための土台になっているもので、ZFCなどの形式的公理系を考える以前に論理体系自体の性質としてメタレベルで証明できるという具合です（形式的公理以前に認めるので形式的証明はあっても無意味に思えます
2016-06-17 04:52:48
D1マン
@11029_8904
ZFCによって公理化して嬉しいのは証明体系ありきの話であって、証明体系の話をするのにZFC等の形式的公理を考えるのは無意味に思えるという感じです。
2016-06-17 04:55:46
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto 「普通の数学」の枠組みで非形式的に証明しています. ただし, 普通の数学はZFCやNBGなどの形式的体系の中で形式化可能ですから, それらの形式的体系をメタ理論として証明していると考えて構いません.
2016-06-17 05:04:21
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto 形式的体系の上に形式的な数学が展開される以上, 形式的体系そのものの性質について形式的な証明を与えるのは無意味, という認識は誤りです.
2016-06-17 05:09:57
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto 例えば第2不完全性定理は第1不完全性定理という形式的体系に関する定理の証明が, 当の形式的体系の中で形式化可能であるとのアイデアのもとで証明されます.
2016-06-17 05:12:11
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto 逆数学は数学の種々の定理を証明する為に必要な2階算術(や集合論)の部分体系の強さを測ります. そもそも形式的体系に関する定理も「通常の数学の定理のひとつ」ですから, どれくらいのメタ理論で証明できるか考えるのは有意味です
2016-06-17 05:14:38
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto 例えば弱い完全性定理はRCA_0という極めて弱い体系で証明可能です. ZFでも証明可能です. 選出原理が不要なわけです. 他方でコンパクト性定理やフルの完全性定理の証明にはWKL_0という体系が必要です. 集合論でいうと
2016-06-17 05:21:08
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto ブール素イデアル定理, ハウスドルフ空間に対するチコノフの定理, ウルトラフィルターの存在定理, 無限人の個人を仮定した際のArrowの不可能性定理の反例の存在などと同値です.
2016-06-17 05:25:44
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
Arrowの定理の反例と対応するというのはどういうことかというと, UD(無制限定義域), WP(全会一致原則), IIA(二項独立性)を満たすSWF(社会的厚生関数)は, 有権者集合上のフィルターと対応していて, ND(非独裁制)は非単項性に対応する.
2016-06-17 08:16:59
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
(但し選択肢は3つ以上) もし有権者が有限であれば非単項超フィルターは存在しないので, UD, WP, IIA, NDを満たすSWFは存在しない. これがArrowの定理. もし有権者が無限であれば非単項超フィルターが存在する(超フィルター定理)ので, Arrowの定理が破れる.
2016-06-17 08:24:54
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto 数学に確固とした基礎付けを与えようという基礎付け主義的な考え方のもとでも, メタ定理の証明に必要な体系の強さを考えることには意味があります. 算術(実数論)や自然数論の無矛盾性は通常の数学の枠組み(つまり集合論)で証明できますが
2016-06-17 05:29:02
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto これは基礎付け主義的には意味がありません. というのは, 自然数論や実数論などより集合論の方が遥かに超越的な存在原理を含んでいて, 無矛盾性の信頼性が低いからです. 叶うなら厳格な弱い体系から証明したい(ある意味で不可能ですが).
2016-06-17 05:32:45
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto 弱い体系(例えば自然数論の部分体系)にどれくらいの原理を追加すれば無矛盾性が証明できるようになるかという問いはゲンツェンによる自然数論の無矛盾性証明(ある順序数までの超限帰納法を仮定)を発端として順序数解析という分野を生みました
2016-06-17 05:37:40
y.
@waidotto
@functional_yy @Rits_math_3rd 「全数学は形式化できる」という形式主義の立場に立てば，形式的体系に関するメタ定理も"普通の数学"の定理の一つであるので，その証明はある適切な公理系のもとで形式化され，(続)
2016-06-17 05:28:47
y.
@waidotto
@functional_yy @Rits_math_3rd (続き)ゆえに初めから形式的議論によってメタ数学を遂行することは数学的に十分に有意味である，と考えてよいでしょうか？
2016-06-17 05:30:25
y.
@waidotto
@functional_yy @Rits_math_3rd こういうことがきちんと述べられている文献等ありましたら教えていただきたいです．手許のどの本を見ても議論の前提が不明瞭なものばかりに感じられます．
2016-06-17 05:38:39
D1マン
@11029_8904
@functional_yy @waidotto メタに前提としていることが形式的体系の中では嘘かもしれないのでそれに形式的な証明を与えることには価値がある、というこでよいでしょうか。
2016-06-17 05:16:31
カムショット・マリファナコカイン・ハードコアポルノ
@amntksr
@Rits_math_3rd @waidotto 例えば選択公理を否定する数学の枠組み(決定性公理など)でロジックを含む数学をするとき(Mr.Konnが詳しい), 既存の定理の証明に選択公理が必要かどうかは重要です. その定理の中には完全性定理やウォッシの定理なんかも含むわけです
2016-06-17 05:43:09
y.
@waidotto
@functional_yy @Rits_math_3rd メタ理論としてZF+¬ACをとり，その中で数理論理学を展開するとたとえば完全性定理が成り立たなかったりするわけですか(つまりそこでは無矛盾だがモデルが存在しない公理系が存在しうるということでしょうか？)．恐ろしいですね．
2016-06-17 05:50:23