[過去ﾛｸﾞ] 集合論について (615ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
110(1): 2014/02/28(金)15:41 AAS
ゲーデル数の小さい定理から順に自動生成するアルゴリズムとか？
111: 107 2014/02/28(金)16:34 AAS
スレ違いスンマセン
論理学スレはどれも荒れていて
こちらのスレの雰囲気が良かったので
そういうようなアルゴリズムがあったら教えて
あるいは、関連する研究があったら教えて
という意図での質問でした
誰かしら研究はされてるはずと思っているのですがなかなか見つからない
ゲーデル数を使ったアルゴリズムは読んでいる教科書で軽くスケッチされているけど
細かい部分がよくわからないのでレシピがあったら読みたい
省2
112: 2014/03/01(土)01:39 AAS
>>110
"順に"っていうならゲーデル数で考えたくなりますけど,ゲーデル数は理屈上の概念であって
実用上あんな巨大な数はまず計算が間に合わないでしょうから っていうのが私の印象
113: 2014/03/01(土)01:51 AAS
変数記号を無限個 {x1、x2、x3、x4、……} 用意するんじゃなくて
{x'、x''、x'''、x''''、……} で代用してコード化すると有限文字（N文字）しか要らないから、
それぞれの文字を0〜N-1と対応させてそのまま読むと
m文字の論理式はN進法でm桁のゲーデル数を対応させられる。
つまり N^m くらいしか要らない。
スマリヤンの本にあるゲーデル数化の方法だけど
m文字以下の論理式はある定数c、kに対してc^(m/k)程度はあるから、
このコード化は割と良い線言ってると思うよ。
114: 2014/03/01(土)02:35 AAS
それって,ｍを固定した時の議論に過ぎない気がします
115(1): 2014/03/05(水)11:46 AAS
WangのアルゴリズムでLKの証明は作れるから
LKとヒルベルトスタイルの同等性の証明をじっと見つめれば
116(2): 107 2014/03/05(水)20:56 AAS
Wang のほうの資料は見つかったけど
同等性のほうの参考文献みつけられません…
同等性はセマンティクスを経由せずに証明できますか？
Deduction Theorem や完全性定理を仮定せずに証明できそうですか？
３つの公理スキーマについては、どの３種類を選ぶかは固定しておりませんが
その手法はそれでも適用できそうですか？
117(4): 107 2014/03/07(金)22:24 AAS
セマンティクスを経由しないでという意味が分かりづらかったので説明します
３つの公理スキーマ
（Ａ１） Ｂ⇒（Ｃ⇒Ｂ）
（Ａ２） （Ｂ⇒（Ｃ⇒Ｄ））⇒（（Ｂ⇒Ｃ）⇒（Ｂ⇒Ｄ））
（Ａ３） （¬Ｃ⇒¬Ｂ）⇒（（¬Ｃ⇒Ｂ）⇒Ｃ）
とＭＰからなる公理系から出発すると、Deduction定理などを経由して完全系定理を示すことができて
この公理系はトートロジーの集合と一致することが示せます
一方、ルカシーヴィッツの公理系
（Ｌ１） （¬Ｂ⇒Ｂ）⇒Ｂ
（Ｌ２） Ｂ⇒（¬Ｂ⇒Ｃ）
省9
118(1): 2014/03/07(金)22:56 AAS
二つの体系S1、S2が同等であることを確かめるには
S1の公理がS2で証明できることと、S1の推論規則がS2の推論を（何回か）使ってできること
S1とS2を入れ替えて上と同じこと
を確かめればよい
119: 107 2014/03/07(金)23:13 AAS
(A1)〜(A3) が定理であることが示せれば
それを使って完全性定理を示せ、
逆に完全性定理を示せるなら
(A1)〜(A3) が定理であることが示せるので、
>118 の条件と >117 の条件は同じ意味になると思います
その >118 での確かめるアルゴリズムがあったらいいのですが…
120: 2014/03/08(土)01:52 AAS
このスレはちょっと活発そうなので,ここで聞いてみたいんですけど,
公理的集合論･数理論理学･証明論･モデル理論と 代数･幾何･解析を扱う方の数学をまたぐ分野ってありますか？
そういう分野,研究にかなり興味あるんですけど。
数学基礎論の理論を代数･幾何･解析の土俵で扱うことが出来るような研究にも興味あります(逆も勿論興味あります)
何で現在,こんなにも｢情報数理と純粋数学｣って住み分けが進んでいるんだろうなっていう気分です。
121: 2014/03/08(土)02:07 AAS
超準解析はモデル理論の応用
122: 2014/03/08(土)02:15 AAS
その言葉聴いた事ある・・・でも知らない・
特殊な微積分を構築するんですか・・
123(1): 2014/03/08(土)07:21 AAS
ここに行ってくるんだ
外部ﾘﾝｸ:www.math.wisc.edu
124(1): 2014/03/08(土)11:38 AAS
外部ﾘﾝｸ[html]:library.msri.org
MSRI Publications -- Volume 39
Model Theory, Algebra, and Geometry
Edited by Deirdre Haskell, Anand Pillay, and Charles Steinhorn
125: 2014/03/08(土)12:40 AAS
>>123,124
詳しい方々どうもです
126: 2014/03/08(土)12:48 AAS
MSRIって凄いですな 日本で言えば,京大のリポジトリで過去のRIMS研究集会の講演内容を公開してる感じなのかな
127(1): 2014/03/08(土)16:26 AAS
>>107と>>117でだいぶ言ってることが違ってる気がするけど。
>>116までを読む限り、公理系が完全なのは前提みたいな書き方だから
2^n通りを虱潰しに調べりゃ良いじゃないか、ということになる。
なんで命題論理の公理図式は一般に3つだと思うようになったのか知らないけど
その体系の公理図式が3つであるのは偶然で、大した意味は無いよ
メレディスの図式みたいに一個からトートロジーを全て導き出せるようなものもある
ウカシェヴィチの公理系から上の三つを頑張って示すか、
ウカシェヴィチの公理系が完全であることの証明が載ってる文献を探すのが一番近道だと思う。
＞ヒラメキなして自動的に判断するアルゴリズムが必要
そんなアルゴリズムあるのかなあ。そもそも無い可能性もある気がするけど。
128(2): 2014/03/08(土)17:49 AAS
>>117
＞ルカシーヴィッツの公理系も同等の性質を持つ公理系らしい
違うと思う
117の公理系では重複する前提を１つにまとめられないと思う
129(1): 2014/03/08(土)17:55 AAS
>>128のつづき
例えば(L1)〜(L3)で
（Ａ⇒（Ａ⇒Ｂ））⇒（Ａ⇒Ｂ）
を証明できる？
上下前次1-新書関写板覧索設栞歴
あと 486 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.012s