17/07/21 15:12:30.15 .net
>>771,772
直観主義論理は一例としてあげただけでしたが、とにかく詳細なレスありがとうございます（入門書レベルの私には理解が全然追いついていませんが）。
810:１３２人目の素数さん
17/07/26 19:15:20.77 .net
>>769です。殆ど似たような質問ですが、メタな立場からの選択公理(もしくはそれと同値な定理)の使用についても、
論理体系を分析する人が選択公理を認めているなら、メタな立場でも自由に使用してもいいという見解でいいんですか？
「そもそも論理体系という土台の上に集合論の公理ZFCがあって、そこからツォルンの補題や整列可能定理などが導出されるのに、その大本の論理体系の分析に選択公理（もしくはそれと同値な定理）を使うのは、ある種の本末転倒っぽくないだろうか？」という印象は持ってしまいます。
（私の記憶が正しければ、何かの書籍でメタ証明を行う際に選択公理(もしくはそれと同値な定理)が使われたことがあった気がします)
811:１３２人目の素数さん
17/07/27 05:50:03.33 jq3p7c5+.net
>>778
>>771ですが、選択公理のように非論理的な数学の公理となると確かにご指摘の通り微妙な気はしますね。
少なくともメタ命題の証明にそういうのを用いた場合にはいちゃもんを付けてくる人が居ても仕方ない気が個人的にはします。
一般連続体仮説を当人がいくら信じているからと言って、
812:メタ命題の証明に連続体仮説を公理として使うのは憚られるように。 個人的には何も制限のない通常の選択公理ACは…ZFに加えた場合の無矛盾性の観点からは全く問題ないのは了解していますが…信じがたいですね。 可算選択公理や従属選択公理ならば信じられますが。（そしてフルバージョンのACと違ってこれらの弱いバージョンは奇妙な命題を導いたりしないのが良い）
813:１３２人目の素数さん
17/07/27 09:31:46.47 .net
>>779
ありがとうございます
メタ証明に用いて良い公理が論理公理か数学公理かでやはり微妙な違和感の存否が分かれるんですね。
814:１３２人目の素数さん
17/07/29 09:49:33.13 KzE/1bUj.net
>>772
そこに様相論理を入れるのもおかしいだろ
815:１３２人目の素数さん
17/07/29 16:55:07.90 MzWZWzzp.net
>>638
P∨￢Pは定理ではなく公理だよ
証明不能
816:１３２人目の素数さん
17/07/29 22:40:51.14 5cAX+bti.net
後継者のみの単項二階論理S1S分かる人おる？
集合の濃度が等しいことはS1Sで書けないみたいなのだけど、どうやって証明したらいいのですかね？
他スレにはそもそも基礎論に精通してる人が皆無なので
817:１３２人目の素数さん
17/07/30 14:01:23.03 ImguYSEg.net
>>782
> P∨￢Pは定理ではなく公理だよ
> 証明不能
排中律 Ｐ∨￢Ｐ を公理とするか否かは古典命題論理の形式化をどうするかによって決まるので、一概に証明不能とは言えない。
例えば、古典命題論理の形式化を直観主義命題論理の形式化 NJ の拡張として行う場合に、
追加すべきものとして排中律を公理として採用せずに、二重否定除去則
￢￢Ｐ
――
Ｐ
を推論規則として追加しても良いわけだが、この場合には排中律 Ｐ∨￢Ｐ は公理でなく定理となり証明されるべき論理式となる。
ついでに言えば二重否定除去則と排中律とは矛盾からは任意の論理式が導ける（Law of Absurdityって言ったっけ）
⊥
―
Ｐ
という推論規則の存在下では同等だが、この規則がなければ同等ではなくなる。
（この規則がなくても、一方から他方は導けるがその逆はできなかった筈。興味ある人は自分で確かめてくれ）
818:１３２人目の素数さん
17/08/10 22:18:16.15 Fsq/G0XU.net
やはり論理そのものに対しては無から構築できないと本来の姿とは言えないよな
819:１３２人目の素数さん
17/08/10 22:31:26.34 UKPSHXWx.net
本来の姿って何？
820:１３２人目の素数さん
17/08/10 22:40:52.91 Fsq/G0XU.net
わからんが、本来の目的に沿った姿？
821:１３２人目の素数さん
17/08/10 22:54:50.01 Fsq/G0XU.net
メタな立場からの言及って、結局は「常に成り立つとは限らない」という目で見ながら扱わざるをえないんでしょ？
822:１３２人目の素数さん
17/08/13 22:39:20.99 oQ62JPFB.net
言語を無から構築すべしと言うのと同レベルの妄言やな
823:１３２人目の素数さん
17/08/13 23:51:06.52 KS8xHldg.net
元々は無から出来ているんだからしょうがないよね
この世の初めから人間の知性があったとでも？
824:１３２人目の素数さん
17/08/13 23:59:45.88 oQ62JPFB.net
>>790
あなたはまず存在の種類を問い質すことから始めるべき
825:１３２人目の素数さん
17/08/14 06:26:49.59 jBgQw2AD.net
>>791
存在の種類として以下の～通りが考えられる。
・・・なんて論を展開してもそれはかなり恣意的なものになってしまうと思うんだ。
826:１３２人目の素数さん
17/08/14 11:43:10.09 ILhcyhMN.net
具体的な数学の証明がメタ的な数学に依存してるわけじゃないならどうでもいいんだけどね。
827:１３２人目の素数さん
17/08/14 19:42:02.28 up/BnRiJ.net
教えてください。
「自分自身の矛盾性 not Con(T) を証明する無矛盾な理論Tが存在する」というのが
数セミ８月号にあったのですが、それは本当に正しいのでしょうか？
828:１３２人目の素数さん
17/08/14 19:59:05.31 xxV/n5K8.net
>>778
てゆーか矛盾がなければ
メタレベルがどんな論理でも別に構わんよ
面白いと思ってくれる人が多ければそれが
存在意義
829:１３２人目の素数さん
17/08/14 20:14:11.55 xxV/n5K8.net
>>784
>（この規則がなくても、一方から他方は導けるがその逆はできなかった筈。興味ある人は自分で確かめてくれ）
最小論理上で
DNE=LEM+POE
830:１３２人目の素数さん
17/08/14 20:57:47.33 t1WO9/Ia.net
メタ論理として無限論理を使っても構わんよ、なんて普通は言わんよ
831:￥
17/08/14 21:29:49.22 gAJfNsT/.net
￥
832:￥
17/08/14 21:30:08.72 gAJfNsT/.net
￥
833:￥
17/08/14 21:30:27.08 gAJfNsT/.net
￥
834:￥
17/08/14 21:30:45.15 gAJfNsT/.net
￥
835:￥
17/08/14 21:31:03.25 gAJfNsT/.net
￥
836:￥
17/08/14 21:31:21.87 gAJfNsT/.net
￥
837:￥
17/08/14 21:31:42.58 gAJfNsT/.net
￥
838:￥
17/08/14 21:32:02.01 gAJfNsT/.net
￥
839:￥
17/08/14 21:32:21.68 gAJfNsT/.net
￥
840:￥
17/08/14 21:32:41.26 gAJfNsT/.net
￥
841:１３２人目の素数さん
17/08/14 21:53:33.26 uno8m9t8.net
>>797
なんで？
信者が多くて矛盾がなくて批判できないんならそれでいいじゃん
842:￥
17/08/14 23:33:25.61 gAJfNsT/.net
￥
843:１３２人目の素数さん
17/08/15 14:45:23.57 Ki0TOx+h.net
最新トップYoutuberの年収は10億円、1億円の時代はもう古い
URLﾘﾝｸ(www.himatubushisp.com)
Youtuberヒカルが月収を明らかに!!おはよう朝日です出演
URLﾘﾝｸ(www.youtube.com)
第１回案件王ランキング！YouTuberで１番稼いでるのは誰だ！
URLﾘﾝｸ(www.youtube.com)
ユーチューバーの儲けのカラクリを徹底検証！
URLﾘﾝｸ(www.youtube.com)
【給料公開】チャンネル登録者4万人突破記念！YouTuberの月収公開！
URLﾘﾝｸ(www.youtube.com)
誰も言わないなら俺がYouTuberのギャラ相場を教えます
URLﾘﾝｸ(www.youtube.com)
最高月収5000万円だとさ。年収じゃなくて「月収」な
おまえらもyoutubeに動画投稿したほうがいい
手っ取り早く視聴数稼ぐには有名ユーチューバーへの物申す系動画がオススメ
しばたーやよりひとやkunやぽんちやモンスタージョンなどを真似すればいい
844:￥
17/08/15 14:59:04.56 eWiOROST.net
￥
845:￥
17/08/15 14:59:22.67 eWiOROST.net
￥
846:￥
17/08/15 14:59:39.23 eWiOROST.net
￥
847:￥
17/08/15 14:59:55.92 eWiOROST.net
￥
848:￥
17/08/15 15:00:11.74 eWiOROST.net
￥
849:￥
17/08/15 15:00:27.21 eWiOROST.net
￥
850:￥
17/08/15 15:00:43.91 eWiOROST.net
￥
851:￥
17/08/15 15:01:02.02 eWiOROST.net
￥
852:￥
17/08/15 15:01:18.54 eWiOROST.net
￥
853:￥
17/08/15 15:01:36.56 eWiOROST.net
￥
854:１３２人目の素数さん
17/08/15 15:38:28.69 zYTTEGnW.net
>>797
無限論理はコンパクト性を喪失しちゃってるから普通の感覚からすると奇妙なことが起こり得るからね
でもまあ、メタ論理として何が許されるかに関しては、>>808が主張しているのが正しい、
つまりメタ論理は数学者や論理学者（あるいは物理学者などの科学者も含めて）たちのコミュニティでの
（今までもそうだったし今後もそうだろうけど、明示的である必要はなくて単に暗黙の）コンセンサスによって決まる問題なのは確かだ
要するに、メタ論理は最後は理屈でなく人間集団における力関係で決まるものだからね
メタ論理としてこれは絶対にダメというのはある（矛盾している体系とか量子論理のように論理として実質的に使い物にならない体系とか）はあるが
それ以外には制約はないから、もちろん直観主義原理主義者がメタ論理も直観主義論理でなければならないとして数学や論理学を展開するのはアリ
855: 現実にメタ論理でも直観主義論理に限定している人々の成す研究者コミュニティは存在して力を持っているわけで だから直観主義論理でなく無限論理をメタ論理として使いたい連中が学会を立ち上げ学術誌や教科書も出して、 直観主義原理主義者たちのようにそれなりに力を持ち新しい人材が定常的に入ってくるようになれば無限論理もメタ論理として実質的な力を持つ 研究者コミュニティが確立したと言えることになる、少なくとも建前上はね ただコンパクト性の喪失とかに現れているように、普通の感覚に最も近いであろう古典論理よりも「強い」論理をメタ論理として用いると 何がしか感覚的に不自然で奇妙なことが起こり得る （その点、直観主義論理のように古典論理より「弱い」論理をメタ論理とする世界は不便なことはあっても感覚的に奇妙と感じることは起こらない） そこが現実にメタ論理として使用実績のある直観主義論理と無限論理なんかのような「強い」論理をメタ論理として使用する場合との違いで >>797が無限論理をメタ論理として使わないだろうという例として持ち出した際にイメージしていた理由だろうと個人的には推測している
856:￥
17/08/15 16:18:00.34 eWiOROST.net
￥
857:￥
17/08/15 18:19:55.06 eWiOROST.net
￥
858:￥
17/08/15 18:20:12.52 eWiOROST.net
￥
859:￥
17/08/15 18:20:28.91 eWiOROST.net
￥
860:￥
17/08/15 18:21:04.90 eWiOROST.net
￥
861:￥
17/08/15 18:21:20.69 eWiOROST.net
￥
862:￥
17/08/15 18:21:36.62 eWiOROST.net
￥
863:￥
17/08/15 18:21:54.15 eWiOROST.net
￥
864:￥
17/08/15 18:22:09.78 eWiOROST.net
￥
865:￥
17/08/15 18:22:30.16 eWiOROST.net
￥
866:１３２人目の素数さん
17/08/15 18:24:45.59 pJNhAgNK.net
メタ論理なんてものを使っちゃダメだよ
867:￥
17/08/15 19:08:03.53 eWiOROST.net
￥
868:１３２人目の素数さん
17/08/19 00:14:37.01 CWax1bwG.net
>>794
正しい。不完全性定理が成り立つ為に理論が
満たすべき条件が無矛盾性以外にも2つくらいある。
その条件を満たしていなくて良ければ
割と簡単に例が作れる。
869:１３２人目の素数さん
17/09/01 16:19:55.61 .net
圏論って形式論理の立場から議論されてるんですか？
870:１３２人目の素数さん
17/09/13 00:15:32.10 GsLJr73d.net
木村先生がロジックヤクザに絡まれてる･ﾟ･(ﾉД`;）･ﾟ･
871:１３２人目の素数さん
17/09/20 16:01:00.72 WCXLOS6A.net
圏論なんて、笑ちゃうよ。
872:１３２人目の素数さん
17/09/21 07:04:12.23 .net
>>837
何その分野のランク付けみたいな勝手な価値観は？
873:１３２人目の素数さん
17/10/03 16:27:09.26 .net
ゲーデルの第2不完全性定理の証明を概略じゃなく、詳細に証明している本ってありますか？
第2不完全性定理の証明は、冗長な証明部分については「○○の議論の流れを形式的数論の論理式に置き換えることにより～～」って省略しているのが多いんで。
874:１３２人目の素数さん
17/10/04 11:10:07.58 BU7Nij2+.net
コンピューターによる何万行もある完全な証明ならネット上でダウンロードできる。
875:１３２人目の素数さん
17/10/04 11:43:08.08 .net
>>840
面白いですね
URL教えてもらえますか？
876:１３２人目の素数さん
17/10/11 03:25:08.63 8YJNJlss.net
別スレに投稿されていたものですが本スレの読者にも有用な情報と思われるので転載しておきます
371 名前：現代数学の系譜 工学物理雑談 古典ガロア理論も読む[sage] 投稿日：2017/10/10(火) 23:29:34.65 ID:N5wCp15o [7/7]
突然ですが、検索でヒットしたので貼る
URLﾘﾝｸ(klapaucius.web.fc2.com)
オンラインで入手できる数理論理学・数学基礎論のテキスト
数理論理学、数学基礎論の教科書的に使えるテキスト（講義ノート、サーヴェイ、モノグラフ等）のうち、オンラインで入手できるものを集めました。
・入門的概説
・論理一般
高階論理と型理論
直観主義論理
コンビネータとラムダ計算
時相論理および時制論理
様相論理
適切さの論理
自然言語の論理
空間論理
・モデル理論
安定性理論
無限論理
・計算可能性理論および再帰理論
・集合論
pcf理論
記述集合論
実数の集合論
選択公理
強制法と内部モデル
連続体仮説
NF
・証明論と構成的数学
順序数解析
算術の体系と不完全性
証明可能性論理
線形論理
構成的数学
・代数的論理と圏論
ブール代数
普遍代数
量子論理
圏論
・歴史
877:１３２人目の素数さん
17/10/11 04:28:34.41 .net
アーこれ知ってる
でも>>840に対する回答にはなっていない？
878:１３２人目の素数さん
17/10/11 04:30:44.14 .net
ちょっと知りたいんですが、
ゲーデルの不完全性定理レベルのビッグな定理って数理論理学(数学基礎論)で何かありますか？
定理の主張する内容のインパクトがビッグなのでもいいですし、定理の証明の長さ・定理を証明するまでに掛かる下積みの長さがビッグなのでもいいです
879:１３２人目の素数さん
17/10/11 04:33:54.57 .net
カット除去定理もビッグでいいですけどもっとビッグなのが知りたいです
自然数論の無矛盾性はビッグでいいですね
AC,GCHの相対無矛盾性もいいですね
880:１３２人目の素数さん
17/10/11 06:02:46.95 jCBLN8wh.net
カリーハワード同型対応…は定理？
881:１３２人目の素数さん
17/10/11 18:05:11.34 8YJNJlss.net
>>843
ごめんなさい、841は839, 840とは無関係で単に本スレの読者に有用な情報と思ったので投稿しただけです
882:１３２人目の素数さん
17/10/19 10:24:28.43 N4ismAjn.net
論理学を少しかじってみたのだけど
数理論理学と相当違うのでビックリ
883:１３２人目の素数さん
17/10/19 10:39:11.13 N4ismAjn.net
>>771
メタに古典論理だけを使って古典論理の健全性完全性は証明できるんでしょ？
メタに直観論理だけを使って直観論理の健全性完全性は証明できるのかな
何かその辺（meta-self-contained?）に正当性の根拠が置けないものかしら
数学的に面白いというだけではあんまり説得力ないような気がしないではない
884:１３２人目の素数さん
17/10/19 11:30:36.11 nv529/Ab.net
そりゃ健全性は証明できるに決まってるだろ
885:１３２人目の素数さん
17/10/19 12:33:21.27 9vEp7GT4.net
最初は無からなにもかも証明しなきゃならないから大変だな
886:１３２人目の素数さん
17/10/20 07:45:16.29 1dD0kJwQ.net
>>850
え？そうなの？ハイチング代数でやるのよね？
887:１３２人目の素数さん
17/10/22 23:59:25.00 sMM5+fid.net
論理式を構成する際は、命題記号や述語記号や関数記号の区別は要らずに関数記号だけで十分なそうなんですが、本当ですか？
本当だとすれば、それはなぜですか？
888:￥
17/10/23 23:15:47.06 Dl6USvMt.net
￥
889:￥
17/10/23 23:16:08.02 Dl6USvMt.net
￥
890:￥
17/10/23 23:16:30.26 Dl6USvMt.net
￥
891:￥
17/10/23 23:16:53.26 Dl6USvMt.net
￥
892:￥
17/10/23 23:17:12.58 Dl6USvMt.net
￥
893:￥
17/10/23 23:17:30.61 Dl6USvMt.net
￥
894:￥
17/10/23 23:17:48.16 Dl6USvMt.net
￥
895:￥
17/10/23 23:18:05.44 Dl6USvMt.net
￥
896:￥
17/10/23 23:18:22.15 Dl6USvMt.net
￥
897:￥
17/10/23 23:18:39.32 Dl6USvMt.net
￥
898:１３２人目の素数さん
17/10/24 15:17:12.16 DeEq5lwh.net
>>840>>841
どなたかダウンロード先のURLを教えていただけませんか。
899:１３２人目の素数さん
17/10/29 22:32:32.60 C2CLcqqJ.net
incompleteness theorem proof coq
もしくは
incompleteness theorem proof isabelle
で検索
900:１３２人目の素数さん
17/10/30 15:45:38.09 yWrKam6g.net
てっきり数学的対象は論理→集合→自然数って言う順に定義していくものだと思ってたんだが、論理の定義の段階で集合や自然数が出てくるのはなぜなんだぜ？
901:１３２人目の素数さん
17/10/30 15:57:27.47 g4HULUTx.net
それらはメタレベルのものであって、数学内で定義されるものでも定義できるものでもありません
902:１３２人目の素数さん
17/10/30 15:57:32.54 QdrF8bUb.net
直観主義論理においては、排中律B∨￢Bは公理でないわけですが、
では何かB∨￢Bの形の簡単な述語論理の論理式で、証明できない例を
教えていただけないでしょうか。そうすれば、直観主義でも無矛盾で
あれば￢(B∨￢B)
903:は証明できないのですから、証明も反証もできない例 になりますよね。 というか、直観主義命題論理においてはB∨￢Bは決定不能命題 ということでしょうか。直観主義ではゲーデルの不完全性によるまでも ないということでしょうか。
904:１３２人目の素数さん
17/10/30 16:06:19.65 g4HULUTx.net
神は存在するか存在しないかのどちらかである
直観主義では、このような命題は証明できません
存在する、もしくは、存在しないと言える具体的な証明を要求します
具体的な証明手段を要求すること、これが直観主義の本質です
905:１３２人目の素数さん
17/10/30 16:13:32.36 yWrKam6g.net
>>867
そこで出てくる集合だの写像だの点列だのは定義すらされていないものなわけ？
906:１３２人目の素数さん
17/10/30 16:14:31.66 g4HULUTx.net
メタのレベルにおいてのみ定義可能です
客体としての数学内で定義することはできません
907:１３２人目の素数さん
17/10/30 16:47:40.81 HjfPA/6s.net
>>868
決定不能の定義を誤解しているように思われる。
908:１３２人目の素数さん
17/10/30 16:49:06.20 bUcJlf9x.net
>>872
決定不能という用語の多義性を知らないと思われる
909:１３２人目の素数さん
17/10/30 16:53:23.68 xZw5uuIN.net
>>873
それは>>868に対して言ってるんだね？
910:１３２人目の素数さん
17/10/30 16:57:42.24 bUcJlf9x.net
>>874
んなわけないだろ
911:１３２人目の素数さん
17/10/30 23:06:22.88 HNynrBDd.net
>>866
論理の定義というか
数学の対象としての数理論理学ね
数理論理学の中で数学が展開されるわけじゃないよ
912:１３２人目の素数さん
17/10/30 23:11:27.65 HNynrBDd.net
>>868
>直観主義命題論理においてはB∨￢Bは決定不能命題
ほぼ当然ながら証明されない（結論として出てこない）よ
真偽で言いたいなら真偽どっちにも決まらないとも言える
913:１３２人目の素数さん
17/10/31 07:45:39.79 0sMM/oG1.net
その「メタのレベル」とやらを一から構築するさまを見たことがない
914:１３２人目の素数さん
17/10/31 08:40:58.53 AWvvD6HU.net
そんなことはできませんよ
915:１３２人目の素数さん
17/10/31 08:44:36.39 0sMM/oG1.net
それじゃダメだよね
ちゃんと構築しなきゃ
916:１３２人目の素数さん
17/10/31 08:48:12.32 AWvvD6HU.net
我々はメタのレベルに住んでいますから、メタの存在としての我々が主体となってメタの思考を行う限り、メタを排除することはできません
917:１３２人目の素数さん
17/10/31 08:49:18.89 0sMM/oG1.net
それを証明できるの？
918:１３２人目の素数さん
17/10/31 08:50:48.56 AWvvD6HU.net
できませんよ
919:１３２人目の素数さん
17/10/31 08:51:32.65 AWvvD6HU.net
でもメタのレベルにおいてなら明らかですよね
920:１３２人目の素数さん
17/10/31 08:57:54.33 AWvvD6HU.net
完全にメタを排除した形式的な数学をメタレベルにおいて構成できるか？
メタのレベルでは明らか、というのは嘘でしたね
メタに対するメタのレベルで明らか、でした
921:１３２人目の素数さん
17/10/31 09:43:26.08 0sMM/oG1.net
それほど明らかじゃないし、やっぱりちゃんと構築しなきゃダメだ。
無から有を産み出すことが不可能だ、というのがドグマ的なものになっているのではないか？
922:１３２人目の素数さん
17/10/31 10:09:13.12 growKt3y.net
できるものなら、やってみればいいです
メタを排除するということは、添え字の自然数すら使えなくなりますからね
923:１３２人目の素数さん
17/10/31 10:52:09.44 0sMM/oG1.net
「ちゃんと構築しよ」
↓
「自然数すら使えなくなる」
なぜなのか
924:１３２人目の素数さん
17/10/31 11:55:28.04 LRRz/Gr+.net
単に難癖付けたいだけの人か
925:１３２人目の素数さん
17/10/31 12:03:38.15 0sMM/oG1.net
哲学的なドグマに関わらないように心がければ、「メタ」というものにどう対処すべきかは、それなりに明らかだとは思うがね。
「メタだから」とか「メタに対するメタのレベルだから」とかやっててもどうしようもない
926:863
17/10/31 12:21:53.18 +o/nBH1H.net
>>865
ありがとうございます
927:１３２人目の素数さん
17/10/31 12:22:05.13 LRRz/Gr+.net
始めからそうやって話せばいい
リアルでもその態度と口調で話してたのか？
928:１３２人目の素数さん
17/10/31 12:32:37.77 kub3utI3.net
>>890
で、メタ要素を一切排除した形式論理の定式化はまだですか？
929:１３２人目の素数さん
17/10/31 12:36:35.51 0sMM/oG1.net
>>893
まだですね
そう簡単にできたら世話はない
実際の数学の証明がメタな要素に直接依存してる訳じゃないから、排除を急ぐ理由はあまりない
930:１３２人目の素数さん
17/10/31 12:38:56.28 vkvNClH5.net
チューリングマシンでも組めば？
931:１３２人目の素数さん
17/10/31 12:38:59.27 kub3utI3.net
>>894
あなたがメタを排除しようと言い出したんですよ？
急ぐ理由はないとはどういうことですか？
932:１３２人目の素数さん
17/10/31 13:12:33.77 LRRz/Gr+.net
形式的数学と非形式的数学が全く同じ証明能力を持つと仮定すればメタレベルの連鎖は終わる
そしてそんな大胆な仮定は置けないので、ここが理性の限界、後は個人の好みの問題
明らかと言えるような何事もない
933:１３２人目の素数さん
17/10/31 14:31:56.17 .net
直観主義（命題）論理学において、A∨￢Aが定理ではない事についての具体例については
前原昭二の｢復刊 数理論理学序説｣を見るといい
具体的なモデル？みたいなのを作って、その下でA∨￢Aが定理にはなっていないことを確認してた記憶がうっすらある
934:１３２人目の素数さん
17/10/31 14:36:52.97 .net
今、スマリヤンの「スマリヤンの決定不能の論理パズル」ってのを読んでますが、これ本格的な様相論理入門書なんですね
タイトル的に寝ながら読めると思って読み始めましたが｢信じる｣述語が出てきたあたりからノート取らないと全く理解が追いつかなくなる
935:１３２人目の素数さん
17/10/31 19:19:33.97 0sMM/oG1.net
>>897
「証明能力」か...
その言葉を使うなら、
メタレベルは形式的証明の正しさを確認することに使われるのみで、
それ自体はなんらの証明能力を持たない、ってのが僕の主張ってとこかな。
これ自体は至極普通だよね。
936:１３２人目の素数さん
17/10/31 19:53:32.56 FOCXqJhR.net
ブール代数でええやん
937:１３２人目の素数さん
17/10/31 19:53:54.50 LRRz/Gr+.net
>>900
つまり、
現に目の前の紙に書かれた形式的証明に対して、その正しさをチェックする場がメタレベルと呼ばれるものである
ということかな
それって、普通に非形式的な証明の正しさをチェックするのと何が違うのかな
モデルを構成して独立性を証明したり、超限帰納法で無矛盾性を証明したりする能力は認めないわけでしょ
何のために形式系を考えるのか分からないよね
むりやり意義を見出すとすれば、非形式的な証明も可能な限り形式的に書くべきという主張？
938:１３２人目の素数さん
17/10/31 21:54:22.32 0sMM/oG1.net
>>902
物理的に形式化して書けるかどうかは別としても、 証明の意味は一意だ。
『原理的に形式化できないけれども証明可能』などという概念は成立しえないので、
形式化の道筋さえ見えないのであればそれは実質的に疑わしい。
つまりメタの世界に自然数全体はなさそう。
939:１３２人目の素数さん
17/10/31 21:57:59.24 LRRz/Gr+.net
＞形式化の道筋さえ見えないのであればそれは実質的に疑わしい。
形式化できるかどうかは今は考えていないけど、何の話をしてるの？
940:１３２人目の素数さん
17/10/31 22:03:41.37 LRRz/Gr+.net
ひょっとして、非形式的な証明を可能な限り形式的に書くことの効用を説明してるのかな
それがどうしてメタの世界に自然数全体がないことに繋がるのか分からん
あなたの目的を達成するためにはメタの世界に自然数全体は必要ない、ということなら理解できるけど
941:１３２人目の素数さん
17/10/31 22:10:40.08 0sMM/oG1.net
>>904
上の方であなたとは違う人が
「メタを排除することはできません」とか
「でもメタのレベルでは明らかですよね」とか言っている。
つまり形式化できなくても成立する世界がある、という主張なんだろう。
それに対しての話さ。
942:１３２人目の素数さん
17/10/31 22:28:18.79 LRRz/Gr+.net
＞つまり形式化できなくても成立する世界がある、という主張なんだろう。
メタレベルで使われる議論は算術とか集合論だから、当然それは形式化の対象でもある
ID:AWvvD6HUが言ってるのは、
メタレベルで使う議論の範囲を厳密に確定させようとするとメタ言語を用いざるを得ない
ということかと
＞形式化の道筋さえ見えないのであればそれは実質的に疑わしい。
＞つまりメタの世界に自然数全体はなさそう。
ID:AWvvD6HUの主張に沿えば「メタレベルを用いなければ形式化の道筋が見えない」ということ
あなたは「メタレベルは存在しない（使わない）のでメタレベルに自然数全体はない」と無意味なことを言ってる
943:１３２人目の素数さん
17/10/31 22:38:00.64 0sMM/oG1.net
>>907
いや、
ID:AWvvD6HUはまず、>>879において
「メタのレベルを一から構築するなんてできない」と言っている。
それでもメタな世界においてこれこれのことが成り立つと主張をするなら、
彼は「形式化できなくても成立する世界がある」と言っているんだろう。
違うかねえ？
944:１３２人目の素数さん
17/10/31 22:42:30.31 4U98kUyg.net
>>879は、メタをレベルにおいて定義されるものを、客体としての数学内で一から構築する�
945:ｱとはできない、という意味でした
946:１３２人目の素数さん
17/10/31 22:49:39.53 LRRz/Gr+.net
>>908
そうだね
ただし、あなたの考えてる意味とは違うと思うけどね
>>907をちゃんと読んでくれたかな？
947:１３２人目の素数さん
17/10/31 22:58:47.29 0sMM/oG1.net
>>909-910
よくわからん。原点に戻りたい。
メタだろうがなんだろうが、一から構築しましょう。形式的に証明できなくても成立する世界なんてない。
それが僕の主張だ。
それを「証明できませんよ」とか「メタに対するメタなレベルで明らか」とか言うなよ。
948:１３２人目の素数さん
17/10/31 23:01:43.72 AWvvD6HU.net
>>911
だからそれを構成してみせてください
具体的に試してみれば、わかります
対象とメタを区別する意味が
949:１３２人目の素数さん
17/10/31 23:06:54.36 LRRz/Gr+.net
>>911
例えば
a∈bが正しい論理式であり、a∈∈bが正しくないのは何故か
と考えるときメタレベルで自然数を使う
a∈bが正しいことは実際に論理式を構成する手順に従って得られることから分かる
問題となるのはa∈∈bが正しくないこと
手順に従い論理式を構成しても4文字の論理式の中にa∈∈bが含まれないことはすぐ分かる
ただし、このとき文字の数を数えて4文字以下や4文字以上という条件に注目した
正しいことを列挙するだけならメタレベルで自然数は必要ないかもしれない
しかし、何が正しくないのか、言い換えれば理論の範囲を確定させたいとき自然数がどうしても必要になる
950:１３２人目の素数さん
17/10/31 23:18:35.07 0sMM/oG1.net
>>912
「それ」の意味が不明
構成を要する主張は最初にあなたがしたはず
>>913
「a∈∈b が論理式ではない」という主張が出来ないならしない、という立場ですよ僕は。
実際出来ないかもしれないし。
出来なくてもたとえば集合論の定理を証明していければ支障ないんだろうし。
951:１３２人目の素数さん
17/10/31 23:20:10.39 AWvvD6HU.net
>>914
メタを一切排除した形式論理の体系を構成してみせてください
952:１３２人目の素数さん
17/10/31 23:25:46.85 LRRz/Gr+.net
>>914
そして>>902に戻る
953:１３２人目の素数さん
17/10/31 23:31:33.81 0sMM/oG1.net
>>916
ああ、>>902に対する答えは「YES」
さ。
だけど「何のために形式系を考えるのか分からない」っていう意見には頷けない。
954:１３２人目の素数さん
17/10/31 23:35:10.65 LRRz/Gr+.net
>>914
＞出来なくてもたとえば集合論の定理を証明していければ支障ないんだろうし。
メタ議論で算術や集合論を使うときも同じだよ
理論の範囲を確定させないまま正しいことだけを列挙する中で、独立性証明や無矛盾性証明が行われる
今更気付いたけど、あなたは形式系を「数学を一から構築するための手段」だと根本的に勘違いしてたんだね
それ違うよ
独立性証明や無矛盾性証明のように、まず理論の範囲を確定しないとできない議論のための手段だから
955:１３２人目の素数さん
17/10/31 23:38:36.91 LRRz/Gr+.net
>>917
＞だけど「何のために形式系を考えるのか分からない」っていう意見には頷けない。
また>>902に戻るけど、普通に非形式的な証明の正しさをチェックするのと何が違うのかな
956:１３２人目の素数さん
17/10/31 23:50:10.02 .net
>>902
非形式的な証明って何ですか？
957:１３２人目の素数さん
17/11/01 00:00:45.01 VCwpMl0X.net
>>918
あなたの目的は知らない
あまり一方的なことを言うなよ。
自分は形式体系をそのように認識している。
数学は一から構築する必要があるし、非形式的な手段というものはそもそも存在しえない。
958:１３２人目の素数さん
17/11/01 00:04:47.80 gL9JwERl.net
通常の数学は全てメタレベルの話で形式的な数学の要素は一切含まれていない、ということはわかりますか？
959:１３２人目の素数さん
17/11/01 00:15:53.16 VCwpMl0X.net
>>922
それは嘘だよね
960:１３２人目の素数さん
17/11/01 00:20:38.66 gL9JwERl.net
たとえば、背理法を用いて何か証明するとき、わざわざ推論規則に当てはめてシークエント式の書き換えをしたりしてないですよね？
論理構造を形式化できていないということです
961:１３２人目の素数さん
17/11/01 00:20:51.40 VCwpMl0X.net
>>922
定理が非形式的な記述によってなされていたとしてもそれは表面的なことで、
実際に証明できたのは形式的な定理。
「非形式的な定理」なんてものはないし、あったとしてもそれは未だ証明されていないもの。
962:１３２人目の素数さん
17/11/01 00:22:13.69 VCwpMl0X.net
>>924
「できていない」と「やっていない」、をわざと混同しているのでは？
963:１３２人目の素数さん
17/11/01 00:26:52.39 ixoveejx.net
>>913
数える必要は無いよ
具体的に構成していくことをメタで見たら数えているように見えるというだけ
964:１３２人目の素数さん
17/11/01 00:27:31.74 gL9JwERl.net
正しくは、できない、です
推論規則をいじるの
965:は、メタレベルにおいての操作です 普通の数学を形式化した時点で、メタから見ての対象と成り下がりますから、形式化されたそれは、あくまで、形式的な数学であり、普通の数学それ自体にはなれません
966:１３２人目の素数さん
17/11/01 00:28:29.25 lmUof8lk.net
面白いね。
967:１３２人目の素数さん
17/11/01 00:36:18.59 ScFh/IWE.net
>>927
俺は
具体的に構成していった中にa∈∈bが含まれないことを確かめる
と言ったんだよ
968:１３２人目の素数さん
17/11/01 00:52:31.24 VCwpMl0X.net
>>928
メタレベルを経由したかもしれないけど、出来上がった証明の正しさは（個別に）形式的にチェックできるのであろう。
しかしそのことの一般化はあきらめよう。
969:１３２人目の素数さん
17/11/01 06:29:35.44 ixoveejx.net
>>930
∈の左右は集合じゃなくちゃいけないから∈の右に∈bは来ないと指摘するだけ
970:￥
17/11/01 07:49:35.52 cSPyhj3J.net
￥
971:￥
17/11/01 07:49:54.98 cSPyhj3J.net
￥
972:￥
17/11/01 07:50:12.03 cSPyhj3J.net
￥
973:￥
17/11/01 07:50:29.50 cSPyhj3J.net
￥
974:￥
17/11/01 07:50:47.81 cSPyhj3J.net
￥
975:￥
17/11/01 07:51:07.37 cSPyhj3J.net
￥
976:￥
17/11/01 07:51:28.19 cSPyhj3J.net
￥
977:￥
17/11/01 07:51:47.92 cSPyhj3J.net
￥
978:￥
17/11/01 07:52:07.93 cSPyhj3J.net
￥
979:￥
17/11/01 07:52:34.25 cSPyhj3J.net
￥
980:１３２人目の素数さん
17/11/01 08:16:22.77 ScFh/IWE.net
>>932
その場合、集合の左端に∈が現れないことを（数学的帰納法で）示しておかないと駄目
981:１３２人目の素数さん
17/11/01 11:16:42.38 uNaz/Y1J.net
>>943
不要
982:１３２人目の素数さん
17/11/01 11:17:29.96 uNaz/Y1J.net
特に数学的帰納法は不要
983:￥
17/11/01 12:19:28.72 cSPyhj3J.net
￥
984:￥
17/11/01 12:19:50.95 cSPyhj3J.net
￥
985:￥
17/11/01 12:20:07.93 cSPyhj3J.net
￥
986:￥
17/11/01 12:20:23.67 cSPyhj3J.net
￥
987:￥
17/11/01 12:20:39.23 cSPyhj3J.net
￥
988:￥
17/11/01 12:20:56.05 cSPyhj3J.net
￥
989:￥
17/11/01 12:21:13.16 cSPyhj3J.net
￥
990:￥
17/11/01 12:21:29.62 cSPyhj3J.net
￥
991:￥
17/11/01 12:21:46.97 cSPyhj3J.net
￥
992:￥
17/11/01 12:22:07.06 cSPyhj3J.net
￥
993:１３２人目の素数さん
17/11/01 12:40:50.74 .net
>>913
その具体例…論理式を表す記号列の解釈が一意に確定すること…に関する議論は｢論理学を作る」の前半部分で議論されていた記憶がうっすらとあります
994:１３２人目の素数さん
17/11/01 13:11:13.35 ScFh/IWE.net
>>944
外延記法や和集合の記号を追加していったとき、
集合一般に関して左端に∈が現れないことを示すには、論理式の長さもしくは論理式の構成に関する帰納法が必要
そこまで一般的な主張をせず、「∈ ＋ 変数記号」が集合でないことを示すだけに留めるとしても、
>>913と同様に文字数に関する考察が必要
995:１３２人目の素数さん
17/11/01 13:26:11.98 ScFh/IWE.net
有限の長さを持つ任意の文字列というものを考えるとき
a_1 a_2 …… a_n
を頭に思い浮かべることと思うが、
……で省略された部分があるにも関わらず、直感的に有限列の性質を把握することができる
それ以前に有限の長さが何を意味するかも何故か知っている
メタレベルにおけるこの得体の知れない直感を（論理法則と同様に）そのままの形で受け入れるか、
自然数の性質に起因するものであると見なすか
どちらか選ぶとすれば俺なら後者だね
996:867
17/11/01 14:46:49.14 iHEq1qM3.net
>>877
そりゃそうですね。証明されない論理式見つけるのに、最初はゲーデル文
見つけるくらい大変だったんですからね。でも直観主義者って、B∨￢B
の形の論理式を公理にしてはいけないって言うんだから、つまりは
B∨￢Bの形の論理式でも正しいとはいえない論理式があると信じている
んですよね。というわりには、じゃあそういう形の（述語論理の）論理式
を見せてみろっていうと、見せれないんですよね。直観主義者の人って存在
すると言ったら実際に見せることができないと気がすまない人たちなんじゃ
あなかったのかなあ。
997:１３２人目の素数さん
17/11/01 14:59:08.89 ScFh/IWE.net
>>959
Bが原始論理式のとき直観主義論理でB∨￢Bが証明可能でないことが
カット除去定理よりただちに分かる
998:１３２人目の素数さん
17/11/01 17:59:08.10 DNDHRFTY.net
直感主義者は板から出てけ うざい
999:１３２人目の素数さん
17/11/01 18:04:29.61 cyvcTwxs.net
>>959
直観主義においてB∨¬Bとは、Bまたは¬Bが証明できる、ということを意味します
もし仮に、B∨¬Bという論理式が証明可能だとすると、Bもしくは¬Bが証明可能ということになり、公理系にBや¬Bが入っている(もしくは定理として導ける)ことを意味します
ですから、任意の論理式やその否定が前提としてない限り、B∨¬Bは証明することができない、ということです
1000:１３２人目の素数さん
17/11/01 18:21:48.91 Gr+Xy0/3.net
>>957
うんにゃ
全然要らない
1001:１３２人目の素数さん
17/11/01 18:24:08.30 Gr+Xy0/3.net
>>961
直観主義者じゃないかもだけど
公理化至上主義者かもな
いずれにせよ絶滅危惧種だ
1002:１３２人目の素数さん
17/11/01 18:43:11.16 ScFh/IWE.net
>>964
「直感主義者」って君のことだろ
1003:１３２人目の素数さん
17/11/01 19:38:07.96 VCwpMl0X.net
>>962
「Bが証明できるかまたは¬Bが証明できる」という意味だとすると、
通常論理における（B∨¬B）に相当する概念はどう書くの？
1004:￥
17/11/01 22:30:03.84 cSPyhj3J.net
￥
1005:￥
17/11/01 22:30:25.59 cSPyhj3J.net
￥
1006:￥
17/11/01 22:30:41.92 cSPyhj3J.net
￥
1007:￥
17/11/01 22:30:59.68 cSPyhj3J.net
￥
1008:￥
17/11/01 22:31:20.50 cSPyhj3J.net
￥
1009:￥
17/11/01 22:31:38.07 cSPyhj3J.net
￥
1010:￥
17/11/01 22:31:56.75 cSPyhj3J.net
￥
1011:￥
17/11/01 22:32:14.65 cSPyhj3J.net
￥
1012:￥
17/11/01 22:32:34.27 cSPyhj3J.net
￥
1013:￥
17/11/01 22:32:55.29 cSPyhj3J.net
￥
1014:１３２人目の素数さん
17/11/02 00:18:11.28 kb3Y9mL5.net
>>966
「B∨￢Bが証明できる｣ということが「Bが証明できる」または「￢Bが証明できる」という意味
なお
ここで言う｢証明できる｣は｢形式的に証明できる｣ということね
1015:１３２人目の素数さん
17/11/02 00:18:36.64 kb3Y9mL5.net
>>965
ぷ
1016:１３２人目の素数さん
17/11/02 00:22:36.54 Rv2iV+x2.net
>>977
無理して回答しようとしなくていいよｗ
1017:１３２人目の素数さん
17/11/02 00:30:24.24 t3jIOnxn.net
>>977
それは「直観主義における（B∨￢B）」の意味でしょ。
そうじゃなくて、
「通常論理における（B∨￢B）」
に相当する概念はどう書くのかを聞いてる。
∨ を使ったらダメなんでしょ？
1018:￥
17/11/02 01:13:25.79 23MnTxXU.net
￥
1019:￥
17/11/02 01:13:47.56 23MnTxXU.net
￥
1020:￥
17/11/02 01:14:05.64 23MnTxXU.net
￥
1021:￥
17/11/02 01:14:23.78 23MnTxXU.net
￥
1022:￥
17/11/02 01:14:39.44 23MnTxXU.net
￥
1023:￥
17/11/02 01:14:57.19 23MnTxXU.net
￥
1024:￥
17/11/02 01:15:19.42 23MnTxXU.net
￥
1025:￥
17/11/02 01:15:40.15 23MnTxXU.net
￥
1026:￥
17/11/02 01:16:00.30 23MnTxXU.net
￥
1027:￥
17/11/02 01:16:18.48 23MnTxXU.net
￥
1028:１３２人目の素数さん
17/11/02 07:13:12.80 kb3Y9mL5.net
>>980
>それは「直観主義における（B∨￢B）」の意味でしょ。
違うよ
直観主義における「B∨￢Bが証明できる」の意味だよ
B∨￢Bの意味は「BまたはBでない」でいいけど
真偽の2値で考えることができないというだけ
3値論理だと
Bが真または偽ならB∨￢Bは真だけど
Bが第3の論理値ならB∨￢Bは第3の論理値
1029:１３２人目の素数さん
17/11/02 09:01:11.76 /fC06Pyx.net
ん
1030:１３２人目の素数さん
17/11/02 14:56:03.91 .net
直近50レスの流れ的に、学部生ですかな？
1031:867
17/11/02 15:03:26.03 j55Wc5r5.net
>>960
例えばPAの公理からはじめて、排中律を使わなくても(1=3∨￢1=3)は簡単に証明
できますよ。
>>962
だから、証明できない論理式があるなら具体的に教えてほしかったんです。
そうすれば、例えば
「PAの公理からはじめて、排中律を使わない場合に
B∨￢B(具体的な形)は証明できません
当然￢(B∨￢B)も証明できません
ということで、直観主義論理にこだわるなら証明も反証もできない論理式
が簡単に見つかるんだ。」
と結論したかったんです。
でもここのレス>>877のおかげで、結局はそう簡単にはいかなさそうだとわかりました。
1032:１３２人目の素数さん
17/11/02 15:13:50.39 CxkP7QYO.net
B∨¬B自体が証明できない論理式そのものなんですよ
具体的な論理式とかではなく、B∨¬B自体が対象としての論理式なのです
Bはワイルドカードとしても捉えることができますが、対象としての原子論理式たる命題そのものとも捉えられます
1033:１３２人目の素数さん
17/11/02 15:18:02.58 CxkP7QYO.net
直観主義では|-B∨¬Bを示すことはできません
B|-B∨¬Bや¬B|-B∨¬Bは示せます
1034:１３２人目の素数さん
17/11/02 15:21:34.83 CxkP7QYO.net
B∨¬Bがあなたの知りたい具体的な論理式だということです
1035:１３２人目の素数さん
17/11/02 19:38:28.78 gkHUdXs2.net
＞証明できない論理式
古典論理でもＡは証明できないよ
1036:１３２人目の素数さん
17/11/02 20:24:16.56 kb3Y9mL5.net
>>998
そこは古典論理で証明できて直観論理で証明できないと意訳すべし
1037:１３２人目の素数さん
17/11/02 20:25:09.93 kb3Y9mL5.net
直観論理で
B∨￢B
は証明できないけど
￢(B∧￢B)
は証明できるのよね
1038:１３２人目の素数さん
17/11/03 00:51:20.59 i9930jhu.net
>>1000
直観主義論理に於いては、∧と�
1039:ﾉと、あるいは∀と∃とはもはや双対ではなく 従ってド・モルガンの法則は成り立たないから なお一言注意しておくと、「直観論理」という言葉は存在しない 正しくは「直観主義論理」です 英語だと“intuitionistic（“intuitionism”の形容詞形で“-ism”なので「－主義」） logic”であって “intuitive（“intuition”：「直観」の形容詞形） logic”じゃないからです
1040:1001
Over 1000 Thread.net
このスレッドは１０００を超えました。
新しいスレッドを立ててください。
life time: 2134日 3時間 34分 0秒
1041:過去ログ ★
[過去ログ]
■ このスレッドは過去ログ倉庫に格納されています