09/04/27 22:05:22
>>784
レスどうも。
>>782で気づいた事は、
「理論を拡張するとき、axiom schemeまで引き継いではいけない」
ってことです。
789:785
09/04/27 22:26:53
>>786-787
説明不足で失礼しました。(自分でもあやふやなので、説明以前に根本的に勘違いしてるのかもしれませんが。)
「ゲーデルと20世紀の論理学」や「論理と計算のしくみ」という書籍を利用していて、帰納的関数論と不完全性定理の部分を少し読んでみた程度なんですが、
どうやら標準モデル(自然数論？)上で真なることと、ペアノ算術で証明可能なことの区別をしないといけないみたいだ、と思ったので、もう一度注意しながら読んでいる所です。
そこで「原始帰納的」や「計算可能」、「帰納的可算」等は、自然数論とペアノ算術、どちらの上でのクラスを定義しているのか、と言うのが質問の内容です。
790:１３２人目の素数さん
09/04/27 23:44:56
持ってる本に、syntaxとsemanticsは区別しましょうとか、
そういうことは書いてないかな。書いてないのかもね。
（まあこういう話は中途半端にすると逆に
完全性定理のHenkinの証明あたりで混乱することにもなるんだけど）
syntaxは論理式とか変数記号とかの（形式的な）ことばや記号列に関する話のことで、
semanticsというのはそのことばが指し示す実際の対象（もの）のこと、とでも思っとけば良い。
標準モデルというのはsemanticsの話で、
ペアノ算術はどっちかというとsyntaxの話。
自然数論ってのは自然数に関する（たとえばペアノ算術とかの）理論のこと。
普通は（そうじゃない分野もあるけどそれはさておき）
原始帰納的とか計算可能とかそういうのは、
あまり形式的なことは考えないで、実際に確かに存在する
自然数という対象に関する概念だと思うことが多い。
要するに（標準的）自然数の関数やその集まりであって、
PAみたいに或る形式的な理論を決めてそれに応じて
規定される概念だとは考えていないことになる。
791:１３２人目の素数さん
09/04/28 00:25:04
>>780
早速のレス有り難うございます。「自然数論」の用法を間違えていたようで、失礼致しました。
シンタクスとセマンティクスですが、一応の区別はついているかなと思います。
(シンタクスはシーケント計算・自然演繹・ヒルベルト流、セマンティクスは古典述語論理やクリプキ意味論をやってシーケント計算の完全・健全性や決定可能性(不可能性)まではやりました)
ただ今まで証明論/意味論の二つの区別で話を進めてきた所に、計算可能性という新しい(？)概念が出て来たので、分類しかねて戸惑っているといった状況です。
レスを読むにセマンティクス側で定義されている様ですね。表現定理なんかを読むと「計算可能性」がセマンティクス側で定義されてると見れば自然に理解出来そうですね。
792:１３２人目の素数さん
09/04/28 00:29:07
recursion theoryって微妙なんだよねー
そういう分類にそぐわない分野だと思う
793:785=791
09/04/28 00:29:46
>>790さんでした。失礼しました。
794:１３２人目の素数さん
09/04/28 21:59:11
>>788
はっきりいって、正確な理解に達していないと思います。Axiom も
Axiom scheme も本質的な違いはありません。色々な流儀はありますが、
Axiom, Axiom scheme は閉論理式，閉論理式の集まりととらえるのが
簡明です。自由変数を含むものは、それを束縛変数にして全称にして
閉論理式にしておくのが明解です。
定数記号は、変数記号とは別になっているのですから、同じ役割であ
るというのは semantics におけることで、Axiom scheme と Axiom に
区別をつけるところに関係するようなことではないと思います。
795:770
09/04/28 22:38:20
>>794
いや、理論Tを理論T'に拡張するとき、「シンボルだけ追加する。公理は追加しない。」と決めた場合でも、
もしAxiom scheme を引き継いでしまうと、新しく追加されたシンボルを使ったT'の論理式にそのscheme
を適用してしまえば公理を追加してしまったのと同じことになるということです。
もとの質問で言うと、理論Tが
「文字eで始まる定数についてなんちゃら～」というパターンのAxiom schemeを持っていたら、
どうなるだろう、というのが疑問の元でした。
この「scheme」の適用を理論T'で追加された論理式にあてはめるのは 「Theorem on Constans」
の条件である「公理は追加しない」に抵触する（=スコープを破壊してる）と気づいた、ということです。
semanticsのことは、証明の過程において何の役割も果たしていない定数は変数に置き換え可能
って感じで納得していて疑問は持っていませんでした。
796:１３２人目の素数さん
09/04/29 09:42:37
＞「文字eで始まる定数についてなんちゃら～」というパターンのAxiom schemeを持っていたら
そういうのは一般的なaxiom schemeではないので
（普通の数学でそういう公理とか定義は聞いたこと無いですよね？ありますか？）
単純に公理の無限集合、という風に言うべきかと。
通常、axiom schemeというのはもっと特殊で、
「任意のformulaφiやtermτjの組に対して以下が成り立つ」
みたいな形をしてるのが普通だと思う。
述語論理じゃなくてもっと一般的な記号変形システムなら
普通にそういうのも考えて良いでしょうけど。
Shoenfieldちゃんと見てないけど、たぶん言えるのは、
定理の前提に抵触して証明がそのままでは成立しなくなる（かもしれない）というだけで、
定理の結論自体はほぼそのままの形で成立すると思いますよ。
あと「定数」はconstan"t"sね。typoだと思ってスルーしてたが覚え間違いしてるかもしれないなので。
797:770
09/04/29 11:14:08
>>796
> constan"t"s
おっと、最初の書き込みから間違えてたｗ
普通の数学にそんな公理はない、ってのはそうでしょうね。
> 「任意のformulaφiやtermτjの組に対して以下が成り立つ」
↑この添字iの集合が理論を拡張する際に拡大されていたら、公理は追加しないという条件の解釈は
普通どうなるんでしょうか？
ちなみにShoenfieldでHenkin theoryを構成するときの導入の仕方は酷くて、任意の論理式 ∃xA を
文字 c の「添字」としてくっつけて新しい定数(special constsnt)を無限個作り出すんですよ。
その上で"すべての" ∃xA → Ax[r] （rは上記のspecial constsnt） というパターンの式を
「special axiom for r」 として追加する・・・。
そんな記号の作り方なんてそれまで言及されてないし、無限個の論理式に対して新たな定数を1対1に
対応させられるなんて力の源泉が曖昧じゃないですか。
「実際記号を作ることはできるんだし、special axiomの導入も明確にできるでしょ」と言われればその通りなん
だけど、公理のパターンとして何が認められるのか釈然としない。
そんなこんなで、「Theorem on Constants」 の証明のところで引っかかったという次第です。
798:１３２人目の素数さん
09/04/29 11:41:35
>>795
>「文字eで始まる定数についてなんちゃら～」というパターンの
> Axiom schemeを持っていた
として、もともと矛盾している場合以外に何か具合の悪いことは
起こるのでしょうか？
定数記号に関するほとんどの誤解は、たとえば π という記号
で円周率の性質を使えば、πについての公理を使っていることに
気がつかないという誤解があります。本質的にこれ以外の間違い
というのは想定し難いのですが、、、。
796 に書いてあることにしても、以前ある term の解釈にすれば
よいだけで、何の問題もないと思います。自分で勝手に具合が悪い
と想像しているだけだと思います。
799:770
09/04/29 12:28:53
>>796
> 何か具合の悪いことは起こるのでしょうか？
それはA[e1, ..., en]を証明する過程の途中で定数eiを変数yiに交換することが
できなくなるから「具合の悪い」と誤解していた訳です。
理論を拡張する際のaxiom schemeの適用に間違った理解をしてました。
ところでπはここでいう「定数」にはあてはまりませんよ。
（特定の実数に対する命名に過ぎないし、使う記号も何だって構わない。）
> 796 に書いてあることにしても、以前ある term の解釈にすればよいだけで
「以前ある term の解釈」の意味がわかりません。再度解説してくれませんか。
800:770
09/04/29 12:29:38
アンカー間違い
× >>796
○ >>798
801:１３２人目の素数さん
09/04/29 13:12:05
>>799
Axiom Scheme を含む体系 T に新しい定数記号を付け加えるわけで、T に
ある term を以前ある term と表現しました。
πは定数記号として導入すると解釈するのは極めて普通。特定の実数とは
その存在と唯一性の証明されている実数のことをいうと思うが、それに
定数記号を対応させ、定義式を公理として付け加えるというのは、とても
普通の考え方。
802:770
09/04/29 23:28:45
>>801
> πは定数記号として導入すると解釈するのは極めて普通
> 定義式を公理として付け加えるえるというのは、とても 普通の考え方。
もともとの Theorem on Constants の話でいうと、新たな公理を何も足さない場合の主張なので、
>>799での「πはここでいう「定数」にはあてはまりませんよ。 」に戻ってしまいます。
803:１３２人目の素数さん
09/05/02 21:54:03
>>802
あなたが心配したことはなんだったんでしょうか？
ご自分で述べていないようですから、仕方ないので述べてみましょう。
ある無矛盾な体系 T の Axiom Scheme として「この体系に現れない
定数記号 c について c ≠ c が成立する」という Axiom Scheme
があったとしましょう。すると、equality axiom があれば、T にない
定数記号がつけ加わった途端に矛盾します。
このような例を述べないで、証明ができないから、どうのこうのという
のは、よくわかっているとは言いがたいと感じたのです。この Axiom
Scheme は変なところがあります。しかし、それをあなたが的確に指摘
できたら、、、きっと、あなたはこんなところで、質問しないので
しょう。もし、ちゃんと答えられたら、ちゃんとわかっているという
ことでしょう。だから 794 に正確な理解に達していないはずだと書いた
のです。
804:770
09/05/02 23:53:37
>>803
> このような例を述べないで、証明ができないから
>>795で書いた
> 「文字eで始まる定数についてなんちゃら～」というパターンのAxiom schemeを持っていたら、 ・・・
というのが自分なりの「例」だったんですが、きちんと結論まで述べてませんでしたね。
もともと私が心配していたのは、う～ん。。たとえば以下のような状況です。
述語pと関数f を持つある体系 T に
「文字eで始まる定数e*について p(e*, f(e*)) が成立する 」 という Axiom Scheme があったとする。
・述語pと関数f はTのもの
・文字eで始まる定数はTに存在しない
・拡張した理論T'に定数e1, ... , enが導入された
・拡張した理論T'に公理の追加はない
以上の条件の下に、
理論T'で p(e1, f(e1)) ∧ ・・・ ∧ p(en, f(en))が成立するとしたら、Theorem of constantsを適用して
理論Tで変数 y1, ..., yn について p(y1, f(y1)) ∧ ・・・ ∧ p(yn, f(yn)) が成立することになるが、
これは言えないはず。
<例ここまで>
> この Axiom Scheme は変なところがあります。しかし、それをあなたが的確に指摘できたら、、、
いただいた例について今の自分の理解で述べると、
・この Axiom Scheme に変なところはない
・Tにおける公理はTのスコープ内で確定している。この Axiom Scheme によって生成される公理はゼロ個。
・T にない定数記号がつけ加わった途端に・・・
公理を追加しない、という条件であれば矛盾なし。
Axiom Scheme を適用して公理を再生成していい、という条件であれば矛盾発生
再び今の自分の理解で言うと、Theorem of constants の条件である「公理を追加しない」ってのは
Axiom Scheme を再展開して公理を生成するのはダメってことであり、それが >>788で書いたことです。
805:１３２人目の素数さん
09/05/05 01:49:39
この連休で強制法勉強しようと思ってたけど
ほかの勉強で全然暇無いなあ、
昨年の夏からずっと強制法勉強したいと思ってるのに、、はあ
806:１３２人目の素数さん
09/05/05 14:41:58
>>805
他の勉強を全部捨てるんだ！
807:１３２人目の素数さん
09/05/05 21:38:42
>>804
この後は、何も返答いたしません。やりとりはこれで終わりです。
> 述語pと関数f を持つある体系 T に
> 「文字eで始まる定数e*について p(e*, f(e*)) が成立する 」 という
> Axiom Scheme があったとする。
> ・述語pと関数f はTのもの
> ・文字eで始まる定数はTに存在しない
体系 T にこのような Axiom Scheme があれば、e という文字が T に現れてい
ます。ですから、文字 e は体系 T ではなんなのでしょう?
803 でそれを Axiom Scheme とはいわないだろうというのは、体系 T に現れ
ないものについて、、、といった途端に、その Axiom Scheme はないものと同
じであると解釈されるべきでしょう。これが、Axiom, Axiom Scheme といった
ときの「普通」の理解です。これらについて形式的定義があるわけではないの
ですから、あなたの理解だって一向構わないのかもしれません。ただ、通用し
ないですね。
808:１３２人目の素数さん
09/05/05 22:18:21
おまえら二人して同じ事言ってるがどっちも日本語ダメダメね。
わかりやすく伝えるよろし。