24/04/30 17:33:23.65 oJaItfqx.net
マイナーなタブローはどうかなあ
自然演繹が初心者には分かりやすいし
メジャーなシーケント計算を最初から学ぶのもよかろうし
174:１３２人目の素数さん
24/04/30 17:38:45.52 doVY1jXx.net
>>173
シーケント計算でも、証明が存在する場合に
それを見つける「手続き」を示すなら結構ですよ
ただその目的にはタブローのほうがわかりやすいかと
別にカット除去とかしたいわけではないので
シーケント計算に固執しても仕方ない
メジャーとかマイナーとかは無意味かと
無意味なことにこだわっても賢くなれない
175:１３２人目の素数さん
24/04/30 20:52:53.27 dbyjbpZp.net
タブローの方法とは、真理の木あるいは意味論的タブローまたは分析タブローと呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続きの一種である。ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。
176:１３２人目の素数さん
24/04/30 23:06:25.99 dbyjbpZp.net
106位
177:１３２人目の素数さん
24/04/30 23:22:31.72 dbyjbpZp.net
４５
178:１３２人目の素数さん
24/05/01 09:12:38.28 sgJI4piv.net
82位
179:１３２人目の素数さん
24/05/01 09:17:13.58 8OeQUrrJ.net
>>175
そんな文章いくら読んでもタブロー法理解できんし
タブロー法について書かれた本を読めば方法わかるから
わけもわからず自然演繹がーシーケント計算がーとかいってんのは
３つともわからんド素人の戯言かと
180:１３２人目の素数さん
24/05/01 09:35:03.02 8OeQUrrJ.net
素人が論理って便利と感じるのは、
この論理式がトートロジーかどうか判別できる
というところだろう
上記の問題に対して、タブロー法は「半分」回答を与える
つまり、トートロジーの場合には、その否定命題から矛盾を導くことで、答えを教えてくれる
ただし、そうでない場合、手続きが終了しない場合があるので、そうでないとわからないこともある
181:１３２人目の素数さん
24/05/01 12:11:17.62 Uy25Ztq/.net
「やらない理由はない」と言って不必要な仕事を指示された時に論理的に反論したいのですが知識がなく、できません。
「やる理由がある」こととは違うと思うんです。先輩、教えて下さい。
182:１３２人目の素数さん
24/05/01 14:06:17.20 vM4x4Lv2.net
>>179
なにアホ言ってんの
一番分かりやすいのは自然演繹
メジャーなのはシーケント計算
タブローはマイナーってだけ
183:１３２人目の素数さん
24/05/01 16:34:14.56 8OeQUrrJ.net
>>182
君が不勉強だからタブロー知らないだけ
勉強すればタブローなんて簡単だと分かる
つまらないことに固執するのは○違いの症状
184:１３２人目の素数さん
24/05/01 19:10:07.96 SXUVR7MR.net
>>183
は
だからマイナーだって言ってるだけだわw
185:１３２人目の素数さん
24/05/01 19:10:58.16 SXUVR7MR.net
別に簡単じゃないと言っていないんだが
自然演繹が一番分かりやすいね
186:１３２人目の素数さん
24/05/01 19:59:13.67 sgJI4piv.net
最近は「ニッチ」がよく使われるそうだ
187:１３２人目の素数さん
24/05/01 20:36:48.84 2ko0QSNd.net
>>180
>「やらない理由はない」と言って不必要な仕事を指示された時に論理的に反論したいのですが知識がなく、できません。
>「やる理由がある」こととは違うと思うんです。先輩、教えて下さい。
ふつう定石は、Yes But法だな
１）仰る通り「やらない理由はない」ようですが・・と始める
２）しかし、今やるべき仕事が沢山あります
３）やるべき仕事に優先順位を付ける必要があります
４）いま、期日が迫っている仕事を A,Bと二つ抱えています。これを優先いたしたいと思います
と答える
これが、断る前提のロジックだが
そして、A,Bの二つの仕事を終える前に、言われた「やらない理由はない」の仕事について自分がやるべきかどうかを考えるのです
その後「A,Bの仕事が終わったので、その仕事をやらせて頂きます」と申し出るのが、一案だな
（もういい、別の人に頼んだ！と言われることも多いだろう）
会社の仕事では、自分には不必要に見える仕事でも、会社全体では意味があることも多い
そもそも、最初に仕事を振られたとき、”断るのが良いか受けるのが良いか”は、よく考えることだね
出来る人は「社長やって」と振られるのです！（下記）
(参考)
URLﾘﾝｸ(www.e-sales.jp)
eセールスマネージャーRemix Cloud
Yes But話法とは・意味
応酬話法と呼ばれる話法の中の1つ。
相手の意見・主張に対し、いきなり否定・反論するのでなく、一旦納得・賛成・共感してから自身の考えを述べることによって、相手の心の障壁を取り除き、こちらの提案を受け入れやすくする話法。
お客様「A社の商品と何が違うの？あまり変わらない気がするけど・・・？」
営業「そうですね。見た目はあまり変わらないかもしれません。ですが弊社の製品は・・・」
お客様「そう。でも高いよね。。」
営業「他社と比べると確かに割高です。ただ弊社には他社にはない・・・があって、」
・・・・
あまりやりすぎるのも逆効果！？
URLﾘﾝｸ(www.nippon.com)
トヨタ社長交代の舞台裏と狙い、佐藤恒治新社長の横顔とは
2023.03.15 山本 シンヤ nippon.com
章男氏から佐藤氏への社長の打診は、2022年12月にタイで開催された耐久レースの現場で行われた。
「レース中に呼ばれたので行くと、『ちょっとお願い聞いてくれない？ 社長やってくれない？』と言われました。最初は冗談だと思ったので、どうリアクションしていいのか分かりませんでした（苦笑）」（佐藤氏）
「私なりの内示の仕方があると思いました。佐藤とは社長室で話をするより、一緒にクルマに乗ることや現場で話をすることが多かった。だから、改めてどこかに呼んで話をするより、その延長線上でお願いした方がいいと思いました」（章男氏）
188:１３２人目の素数さん
24/05/01 21:15:12.58 8OeQUrrJ.net
>>184
自分が知らない＝マイナー
というのは自己本位な素人の戯言
恥ずかしいだけだから言わないほうがいいね
嘲笑されたくないでしょ？
189:１３２人目の素数さん
24/05/01 21:28:26.97 8OeQUrrJ.net
>>181
>「やらない理由はない」と言って不必要な仕事を指示された時に
>論理的に反論したいのですが
まず、上司が「やらない理由はない」という場合
大体は「やらない理由が思いつかない」というだけで
証明になっていません
一方、部下としては「やらない理由」を提示するのが効果的ですが
そうしなければならないというわけではありません
そこで弥縫策ですが、上司に
「やらない理由が存在すると矛盾する、と証明できますか？」
といってみる手はあります
ただ大抵の上司は激怒するでしょうね
彼らは部下に仕事させることしか頭にありませんから
190:１３２人目の素数さん
24/05/01 21:32:15.89 8OeQUrrJ.net
ところで「不必要な仕事」であることは証明できるのでしょうか？
あなたが「必要ない」と勝手に思ってるだけなら、それも証明ではありませんね
まず、上司に対して、自分がその仕事を必要ないと考える理由を述べた後
その理由を否定するような必要性について示してほしいと 述べたらいかがでしょう
まあ、明確な理由もなく、単に面倒くさいからやりたくないということで
いわれてもサボりまくる、という手はありますけどね
実はそれでも会社が困らないならいいんじゃないですか？
191:１３２人目の素数さん
24/05/01 22:21:52.77 SXUVR7MR.net
>>188
あのねw
数理論理学の本でほぼほぼ言及されてるのは
自然演繹とシーケント計算
タブロー方は本当にマイナーなのよ
例えばここどう？
URLﾘﾝｸ(www2.yukawa.kyoto-u.ac.jp)
あと
>恥ずかしいだけだから言わないほうがいいね
>嘲笑されたくないでしょ？
自己紹介どうも
192:１３２人目の素数さん
24/05/01 22:26:29.70 SXUVR7MR.net
> ID:doVY1jXx
>>171,172
と
>>170
それと
> ID:8OeQUrrJ
>>189,190
と
>>181
か
触らんとこ
193:１３２人目の素数さん
24/05/01 23:39:00.43 2ko0QSNd.net
>>189-190
フォローありがとう
そもそも
>>181
>「やらない理由はない」と言って不必要な仕事を指示された時に
>論理的に反論したいのですが
これで、理屈っぽいフランス人ならどうするかを、頭に置いて考えてみました
「やらない理由はない」など、サギセールスまがいの理由をいうのは、いまどき？
昔は「君、これやってくれ」だったけどｗ パワハラと言われるのがいや？ｗ
会社に、セールス電話で「だんな先物取引で儲かります。”やらない理由はない”です」とかあったなｗ
君がやらなくても会社は困らないは正しいと思うが
会社から見て、「君はいなくても困らないよ」と言われないようにしないとね
194:１３２人目の素数さん
24/05/02 09:31:01.36 MGx3IZdS.net
>>191
自分が読んだ本はメジャーで読まない本はマイナーって
どんだけ自己中心的なんですかねぇ
URLﾘﾝｸ(en.wikipedia.org)
Tableaux can be intuitively seen as sequent systems upside-down.
This symmetrical relation between tableaux and sequent systems was formally established in (Carnielli 1991).
URLﾘﾝｸ(web.archive.org)URLﾘﾝｸ(www.cle.unicamp.br)
195:１３２人目の素数さん
24/05/02 09:33:16.69 MGx3IZdS.net
＞会社から見て、「君はいなくても困らないよ」と言われないようにしないとね
会社からみて、必要なのは労働者 不必要なのは社長をはじめとする管理職
これ明らかね 管理職の仕事ってただのブルシット・ジョブだから
196:１３２人目の素数さん
24/05/02 10:32:07.81 kA6jMeIR.net
馬鹿乙
197:１３２人目の素数さん
24/05/08 18:15:34.62 c0TH2Ddg.net
今日見つけた怪しい書き込み
>1.ラッセルのパラドックスの発見（1902年）
>1902年、哲学者のバートランド・ラッセルが論理学における矛盾を発見しました。
>このパラドックスは、通常の論理学では回避できないことが判明し、
>哲学に大きな衝撃を与えました。
>2.ラッセルによる新しい論理学の構築（1903年～）
>1903年以降、ラッセルはパラドックスの原因が論理学の仕組みにあると見抜きました。
>自己と自己言及を明確に区別して混同しないルールを導入し、
>パラドックスが起こらない新しい論理学の仕組みを構築しました。
>4.ゲーデルの不完全性定理（1931年）
>1931年、クルト・ゲーデルもラッセルの論理学に影響を受け、
>「論理学によって仮定そのものの正しさをその仮定から証明できるか？」を考察しました。
>ゲーデルは、それが不可能であることを証明しました（ゲーデルの第一不完全性定理）。
>この定理は、当初ペアノ算術におけるω無矛盾性が証明不可能として確立されましたが、
>後にロッサーの証明ではペアノ算術における単純無矛盾性、
>シェファードソンの表現定理により任意のΣ1集合で構成される任意の論理式に対して
>無矛盾性の証明が不可能であることまで拡張されました。
198:１３２人目の素数さん
24/05/08 18:17:34.54 c0TH2Ddg.net
続き
>ラッセルのパラドックスは、ある集合が自分自身を含むかどうかという自己言及から生じる矛盾です。
>このパラドックスが発生する論理体系では、自己言及によって簡単に矛盾を作り出すことができてしまいます。
>しかし、実際にはラッセルが開発した新しい論理学によって、このパラドックスは解決されました。
>つまり、ラッセルのパラドックスは本来矛盾ではないのです。
>問題は、ラッセルのパラドックスが矛盾を引き起こす論理体系では、
>本来矛盾ではないものを自動的に矛盾していると仮定してしまうことです。
>この「矛盾ではないもの=矛盾している」という誤った前提が常に存在していることになります。
>この誤った前提が存在すると、爆発律という原理が成立してしまいます。
>爆発律とは、矛盾から任意の結論を導き出せるという原理です。
>つまり、矛盾を前提とすれば、どんなことでも真とも偽とも証明できてしまうのです。
>そのため、ラッセルのパラドックスを引き起こす論理体系で導かれた結論は、意味がないということになります。
>矛盾を前提としているため、導かれた結論が真であるのか偽であるのか判断できないからです。
>したがって、ラッセルのパラドックスを回避する仕組みを持たない論理体系で得られた結論は、
>信頼性に欠けると言えます。
>ラッセルが開発した新しい論理学のように、
>矛盾を回避する仕組みを備えた論理体系を使用することが重要なのです。
199:１３２人目の素数さん
24/05/08 23:36:06.77 +0jADlNL.net
>>197-198
>今日見つけた怪しい書き込み
ご苦労さまです
早めの証拠保全（下記）
ｽﾚﾘﾝｸ(math板:219番)-222
『なぜ数学の非専門家は「選択公理」や「不完全性定理」が好きなのか？』より
１）”哲学者のバートランド・ラッセルが論理学における矛盾を発見”は、ヘン（正しくは素朴集合論）
２）”通常の論理学では回避できないことが判明”も、ヘン（正しくは素朴集合論）
３）”ラッセルによる新しい論理学の構築”も、ヘン（正しくは型理論による集合論）
４）”1931年、クルト・ゲーデルもラッセルの論理学に影響を受け”も、ヘン（正しくは、ヒルベルト・プログラムの研究）
ともかく、『怪しい書き込み』でした
URLﾘﾝｸ(ja.wikipedia.org)
ラッセルのパラドックスとは、素朴集合論において、自身を要素として持たない集合全体からなる集合の存在を認めると矛盾が導かれるというパラドックス。
ラッセルの型理論（階型理論）の目的のひとつは、このパラドックスを解消することにあった
概要
「それ自身を要素として含まない集合」を「M集合」とし、「すべてのM集合を成分とする集合R」を作ってみる。そうすると、「任意の集合X」に関しては、「XはRに含まれる」⇄「XはXに含まれない」という定式が成り立つ。
そして特にX=Rとすれば、「RはRに含まれる」⇄「RはRに含まれない」となり、パラドックスが明示される。
矛盾の解消
公理的集合論によって何をもって集合とするかについての形式的な整備が進められ、素朴（だが超越的）な
R の構成を許容しない体系が構築された。
1.公理的集合論による解消[注 1]
具体的には内包公理を次の分出公理に弱める（ツェルメロによる版）。
（なお現在のZFC集合論では、フレンケルが設定した置換公理から分出公理が導けるため、分出公理自体は公理としていない。）
2.単純型理論による解消[注 2]
略す
3.部分構造論理による解消[注 3]
略す
URLﾘﾝｸ(ja.wikipedia.org)
ゲーデルの不完全性定理 または不完全性定理とは、数学基礎論[1]とコンピュータ科学（計算機科学）の重要な基本定理[2]。（数学基礎論は数理論理学や超数学とほぼ同義な分野で、コンピュータ科学と密接に関連している[3]。） 不完全性定理は厳密には「数学」そのものについての定理ではなく、「形式化された数学」についての定理である
クルト・ゲーデルが1931年の論文で証明した定理であり[5]、有限の立場（英語版）（形式主義）では自然数論の無矛盾性の証明が成立しないことを示す[3][5]。なお、少し拡張された有限の立場では、自然数論の無矛盾性の証明が成立する（ゲンツェンの無矛盾性証明（英語版））
ゲーデルはヒルベルトと同様の見解を持っており、彼が不完全性定理を証明して示したのは、ヒルベルトの目的（「無矛盾性証明」）を実現するためには手段（ヒルベルト・プログラム）を拡張する必要がある、ということだった
200:１３２人目の素数さん
24/05/09 05:55:56.63 WJ4F9QUd.net
>>195
わからなくもないが
どこかかび臭い言い方
201:１３２人目の素数さん
24/05/09 08:41:05.22 kr5FQ87d.net
>>199
>正しくは素朴集合論
というか無制限の内包公理
URLﾘﾝｸ(ja.wikipedia.org)
>正しくは型理論による集合論
あるいは、新基礎集合論
URLﾘﾝｸ(en.wikipedia.org)
ただ、この理論では、杓子定規にいえば、自然数はそれぞれ異なる階層に属する
0={} 0階
1={{}} 1階
2={{}，{{}}} 2階
3={{}，{{}}，{{}，{{}}} 3階
…
また、公理的集合論でも同様だが、
全ての自然数の集合の存在を規定するため
人工的な公理（無限公理）を設定せざるを得なくなる
202:１３２人目の素数さん
24/05/09 08:47:43.16 kr5FQ87d.net
>>199
>正しくは、ヒルベルト・プログラムの研究
>有限の立場（形式主義）
ここでいう有限の立場は具体的に言えば原始帰納的算術(PRA)
URLﾘﾝｸ(ja.wikipedia.org)
これはペアノ算術より弱い体系である
203:１３２人目の素数さん
24/05/09 09:46:07.20 1s3pLI9I.net
>>202
PRAで定義される帰納的関数の全体って可算じゃない？比嘉さんになりそうな気がしないけど
204:１３２人目の素数さん
24/05/09 10:07:15.66 kr5FQ87d.net
>>203 ？
205:１３２人目の素数さん
24/05/09 10:17:54.79 1s3pLI9I.net
>>204
単純な疑問
非可算か可算かわかる？
206:１３２人目の素数さん
24/05/09 10:25:01.97 kr5FQ87d.net
>>204 なんで非可算が突然出てくるの？
207:１３２人目の素数さん
24/05/09 10:30:21.17 kr5FQ87d.net
それから、可算だと何がいけないの？
208:１３２人目の素数さん
24/05/09 10:38:12.03 1s3pLI9I.net
>>207
だから単純な疑問だって
そうなるかなって思ったの
209:１３２人目の素数さん
24/05/09 10:43:28.66 kr5FQ87d.net
>>208
ただの疑問なら、202へのアンカーは不必要かと
>そうなるかな
そう（＝可算に）なるとして、あなたならどうやってそれを示しますか？
それが数学ですよね？ 数学したいなら、一度考えてみてくださいね
210:１３２人目の素数さん
24/05/09 10:47:39.26 1s3pLI9I.net
R=Map(N,2)だと群構造表さないよなあ
コンパクトオープンで位相定義するとまた色々できそうだけど
211:１３２人目の素数さん
24/05/09 10:48:56.44 1s3pLI9I.net
>>209
PRAについて知ってると思ったから
もしかしたらわかる人かなと
自分にはそうなりそうと思うだけで
可算かどうかはわかんない
212:１３２人目の素数さん
24/05/09 10:55:04.15 kr5FQ87d.net
>>211
検索すれば答えは書いてありますけどね ネットの検索方法知りませんか？
213:１３２人目の素数さん
24/05/09 11:03:45.82 1s3pLI9I.net
>>212
書いてある？
よければ教えて？
214:１３２人目の素数さん
24/05/09 11:10:28.90 1s3pLI9I.net
ゲーデルの算術化で帰納的関数全体は可算になる？
もっと具体的な証明が知りたいなあ
215:１３２人目の素数さん
24/05/09 11:12:20.74 1s3pLI9I.net
>>212
> ID:kr5FQ87d
PRAを紹介しただけで詳しくは知らないということ？
それが悪いと言ってるわけじゃないよ
君に聞くべきではなかったと反省すべきだったみたい
216:１３２人目の素数さん
24/05/09 11:30:03.64 8+ox2D+k.net
>>215
ネトネトした気持ち悪さを感じる
控え目に言って汚物
217:１３２人目の素数さん
24/05/09 11:31:56.37 1s3pLI9I.net
>>216
ごめんね
218:１３２人目の素数さん
24/05/09 11:35:02.69 kr5FQ87d.net
>>213 何を？ 検索ワードを？
>>214 ゲーデルコーディングで、でこれ以上無いほど完全に具体的かと
>>215 有限の立場＝PRA、と述べただけで、PRAについて皆様に説明する義務は負っておりませんが
219:１３２人目の素数さん
24/05/09 11:37:53.12 kr5FQ87d.net
>>216
>>203の書き込みから、ID:1s3pLI9Iを不審者と感じました。
220:１３２人目の素数さん
24/05/09 11:51:27.77 1s3pLI9I.net
>>218,219
ごめんね
221:１３２人目の素数さん
24/05/09 11:53:54.98 1s3pLI9I.net
>>218
>ゲーデルコーディングで、でこれ以上無いほど完全に具体的かと
やっぱそれか
サンクス
さまざまな定義の帰納的関数に対してどうゲーデル数を指定するのか
できそうには思うけどよくわからないなあ
222:１３２人目の素数さん
24/05/09 11:54:36.39 kr5FQ87d.net
>>220 何かやましいことがあったのですか？
223:１３２人目の素数さん
24/05/09 12:00:59.77 1s3pLI9I.net
>>222
君に聞くべきではなかったのを聞いてしまってごめんてこと
224:１３２人目の素数さん
24/05/09 12:15:00.39 kr5FQ87d.net
>>221
>>ゲーデルコーディング
>やっぱそれか
やっぱそれです
>さまざまな定義の帰納的関数に対してどうゲーデル数を指定するのか
文字で関数を記載することは認めますか？
文字から数へのコード化もできるのだから
文字列から数へのコード化もできますね
だったらそんなに難しいことではないですよ
>よくわからないなあ
何がわかりませんか？
わからないことがわからないですが
225:１３２人目の素数さん
24/05/09 12:17:14.91 kr5FQ87d.net
>>223
>君に聞くべきではなかったのを聞いてしまってごめんてこと
「聞けば即座に答えてもらえると思ったのに答えてもらえなかった」
としてもそれはあなたの罪ではないのではないですか？
おかしな人だ
226:１３２人目の素数さん
24/05/09 12:20:59.38 kr5FQ87d.net
もし、203に202へのアンカーがなく
「脱線ですが
PRAで定義される帰納的関数の全体って可算じゃない？」
とだけ質問したならば、こう答えましたけど
「ええ、そうですが それが何か？」
227:１３２人目の素数さん
24/05/09 12:24:29.27 kr5FQ87d.net
脱線質問なのに過去の書き込みと関連があるかのごとく書いたのが不審ということです
数学板に限ったことではないですが、不審者が多いのでね
228:１３２人目の素数さん
24/05/09 13:38:53.62 3I9TrP+4.net
Xで掛け算の順序について支離滅裂な主張を延々としている奴が居て笑える
229:１３２人目の素数さん
24/05/09 14:48:39.34 kr5FQ87d.net
>>228
ｽﾚﾘﾝｸ(math板)
230:１３２人目の素数さん
24/05/09 19:50:11.42 oi/MdB1y.net
>>228
小学校の先生に言わせると
足し算も順序があるらしい
231:１３２人目の素数さん
24/05/09 21:10:11.76 kr5FQ87d.net
掛け算順序論（というか掛け算定義教）は
「a✕ｂはａをｂ回足すという定義 これ以外は定義ではない」
というカルト宗教だそうである
しかしながら掛け算の定義の仕方は１つではないし
算数における掛け算の定義を１つに決める必要もない
これを掛け算無定義論と呼ぶことにしようかと思う
232:１３２人目の素数さん
24/05/09 23:03:43.73 fRVHvQeX.net
私は全てのa,bの対してa×b=0と定義します
そうすれば計算が楽でいいですよ
おすすめです
233:１３２人目の素数さん
24/05/09 23:14:09.29 CAYhdB8c.net
界隈の定義がこうだから、解釈も定義に従って行わないといけないっていう感じが理解できん
定理に基づいて式を立ててもいいじゃない
234:１３２人目の素数さん
24/05/09 23:36:23.43 6oYY/TBi.net
独自の定義をした上で、それが標準的な定義と同じ結果を与えることを証明してから回答を書いてもいいんですよ？
掛け算の順序が問題となる小学校の算数でそこまでできる人がいるかは知りませんけど
235:１３２人目の素数さん
24/05/10 06:42:31.25 n1N5z9So.net
>>234
＞独自の定義をした上で、
＞それが標準的な定義と同じ結果を与えることを
＞証明してから回答を書いてもいいんですよ？
最後の？が気持ち悪いですね
もし、文章の末尾が「よね」だったらそう感じないんですが
「よ」だったら断定なので「？」はつかない
「？」とつけたら問いかけなので末尾は「よね」でしょう
こういうチグハグな文章を２１世紀のネットではよくみますが
国語力の低下というか人類の知的退化の現れでしょうか？
さて本題
＞掛け算の順序が問題となる小学校の算数で
＞そこまでできる人がいるかは知りませんけど
いないでしょう 求められているのは証明ではなく定義の柔軟性かと
算数は数理論理学ではないので、これ以上の言及はいたしませんが
（完）
236:１３２人目の素数さん
24/05/11 02:07:54.73 bSq6Y66y.net
K〇〇oとかいう馬鹿が他人を見下して支離滅裂なこと書いているから痛すぎる
あいつ自分の書いていることが論理矛盾だと気付かないんだな
アメリカだと日本とは逆の順序で計算するという指摘には規則を決めて計算
するのだから別に問題ないみたいに書いているのに、日本のような順序でないと
論理的な意味がないみたいなこと書いていて自己矛盾していて正直馬鹿だと
しか思えん
237:１３２人目の素数さん
24/05/11 08:38:17.98 SoT3Fo/0.net
KONO氏は昔から逆張り大好きな人だったなあ
要するに定義に従えってことでしょう
そもそもどう定義しても同じなら
定義の仕方にこだわっても意味ない
って発想はないみたいだけど
238:１３２人目の素数さん
24/05/11 08:49:50.40 gRKhHbky.net
某スレに、「小学科校から国語のやり直し」を連呼する基礎論婆（数学落ちこぼれ）がいた
239:１３２人目の素数さん
24/05/11 10:46:12.37 I7KlHCOq.net
このスレに居そう
240:１３２人目の素数さん
24/05/11 13:40:18.35 lkkVLtva.net
KONO酷いな
あいつ幼稚園児並みの勘違いをしているな
スカラー×ベクトルの例で非対称性を主張し続けているけれど論題はそこ
ではないだろ
スカラー×スカラーの積の可換性はネーターの定理の保存則の存在から
対称性が存在するんだから対称と捉えるのが当然だろ
（一つの籠の中のリンゴの数をa個）、（籠の数をb個）とした場合に合計
何個リンゴがあるかという問題であいつの主張は原理主義者が（一つの籠
のリンゴの数をb個）、（籠の数をa個）として計算することを許容している
即ち無理やり対称性を仮定しているとか言ってんだよな
頭がが悪すんじゃないのかなあいつ
241:１３２人目の素数さん
24/05/11 19:14:40.97 SoT3Fo/0.net
掛け算順序に固執する人の発想が「スカラー×ベクトル」なのはなんとなく見当がつく
で、問題はそう考えなければならないか、というところで、個人的には「んなこたぁない」と思ってる
242:１３２人目の素数さん
24/05/11 19:15:33.38 SoT3Fo/0.net
KONO氏はレスバしたがってるだけなので相手しても時間の無駄よ
243:１３２人目の素数さん
24/05/11 20:11:44.55 SyrfSAV2.net
>>241
そんな高度な話じゃないぞ
定義の問題
244:１３２人目の素数さん
24/05/12 07:11:53.14 OFz/L2Zo.net
全ての🎁の中に🍎🍎🍎🍎🍎 ある。
そして🎁🎁🎁だ。🍎はいくつあるかというと
地球人は、3+3+3+3+3って計算するのかな❓
ポクは、5+5+5で計算します。ピミ達はどっちで計算するの❓
245:１３２人目の素数さん
24/05/12 08:09:15.62 kLL3MH+1.net
🎁🎁🎁からそれぞれ１コ🍎を取り出すなら3+3+3+3+3ですが何か？
246:１３２人目の素数さん
24/05/12 13:33:26.66 qIl7Lv61.net
直観主義論理で西村巌という人が重要な仕事をしているらしい
ネットで調べてみても岐阜大にいたこと以外何の情報もない
247:１３２人目の素数さん
24/05/13 08:48:36.38 VHcVZoar.net
>かけ算に順序はない」の(ひとつ分)x(いくつ分)と異なる間違った定義のリスト。これで尽きてる
0)値が同じなら式も同じ(式に意味はない)
1)定義はない (半環など未定義演算
2)アレイ図を数える (直積濃度
3) (いくつ分)x (ひとつ分)の両方が成立
4) (いくつ分)x (ひとつ分)との不定状態
やっぱりこいつ真性の馬鹿なんだな
248:１３２人目の素数さん
24/05/13 09:22:13.78 TckfqamF.net
>>247 レスバしたい人を相手すると時間空費するからやめとき
249:１３２人目の素数さん
24/05/13 11:36:06.03 8dR7sMEU.net
論理学において、「矛盾」の扱いが雑なように感じる。
数理論理学では「矛盾」をどう扱っているのだろう。
単純に排除されるべきものとして扱われているのだろうか、
という疑問。
矛盾は数学的対象なのか？
250:１３２人目の素数さん
24/05/13 11:47:53.15 TckfqamF.net
Pと￢Pの両方が導かれることを矛盾という
矛盾からはいかなる命題も導かれることになっている
これは空集合がいかなる集合の部分集合でもあることに対応している
251:１３２人目の素数さん
24/05/13 14:55:09.67 8dR7sMEU.net
ありがとう
252:１３２人目の素数さん
24/05/13 18:57:51.61 pzVZ11pL.net
Pと￢Pの両方が導かれる場合、排中律は成り立っていない。
爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。
さらに、Pが自己同一性をもっていないとすれば、命題ではない。
それなのに爆発律があるかのように扱われているのは矛盾する。
爆発律は、妥当でない推論の例なのではないか？
爆発律が存在する（形式）論理体系なんてものは存在するのだろうか、という疑問。
253:１３２人目の素数さん
24/05/13 20:38:55.33 AG1nQkcA.net
＞Pと￢Pの両方が導かれる場合、排中律は成り立っていない。
実際は排中律もその否定も導かれる
＞爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。
排中律も導かれるという意味では成り立つ
＞Pが自己同一性をもっていないとすれば、命題ではない。
自己同一性とは？意味がわからんが
＞それなのに爆発律があるかのように扱われているのは矛盾する。
だから矛盾してるっていってるんだが 記憶能力ゼロ？
＞爆発律は、妥当でない推論の例なのではないか？
そもそも矛盾してない場合、爆発律を使うことはない
＞爆発律が存在する（形式）論理体系なんてものは存在するのだろうか
いかなる命題を前提してもトートロジーは導ける
この対偶が、矛盾からいかなる命題も結論できるという爆発律
254:１３２人目の素数さん
24/05/13 22:21:33.13 nMh83wOC.net
爆発率てのは人→Pのことだけど
これをそう呼ぶのはいかがなものか
P→Qとは単にモデルによる真理値割り当てにおいて
P≦Qであるということを言っているにすぎない
つまり人の真理値がボトムだという主張が人→Pの意味であり
人がどういうものであるべきかを意味している公理と言える
矛盾を定義しているという意味から
この公理は矛盾律と呼ばれるべきかと思うけどね
255:１３２人目の素数さん
24/05/13 22:23:54.69 pzVZ11pL.net
うーん、理解されなかったか。
Pがなんらかのタイプの矛盾であるとき、
P ⊢ Pは妥当なのか。
256:１３２人目の素数さん
24/05/13 22:27:25.58 PIZjx3rs.net
>>255
自分が理解していないから問題点を明確に書けない
257:１３２人目の素数さん
24/05/13 22:34:02.21 nMh83wOC.net
>>252
>爆発律は、妥当でない推論の例なのではないか？
P∧￢P→人
は￢Eという推論規則を公理化したもので
矛盾律人→Pと合わせて
P∧￢Pは人と同等であることを言っている
（ここで同等とはお互いを導き合うこと
一般には同値と呼ばれるが自分は同等と呼びたい）
矛盾律を公理としない場合でも
人がある論理体系ならP∧￢P→人は公理もしくは推論規則にするだろうから
矛盾にさまざまな階層が生まれることになる
つまり人はもはやモデルによる真理値割り当てでボトムではなく
もっと低い真理値も容認されることになる
258:１３２人目の素数さん
24/05/13 22:35:47.79 nMh83wOC.net
>>255
Pが矛盾でも何でもP→Pは成立するよ
259:１３２人目の素数さん
24/05/13 23:01:13.68 pzVZ11pL.net
P→Pが成立しないような矛盾は数理論理学では
扱えないということなら納得します。
260:１３２人目の素数さん
24/05/13 23:13:17.05 nMh83wOC.net
大概の論理で
Pを矛盾として
P→Pは成立するよ
成立しないのは
PからQが導かれてもP→Qが成立しないとするような
相当つまらない論理だけでしょ
261:１３２人目の素数さん
24/05/13 23:53:33.82 pzVZ11pL.net
つまらない論理ではないと考えているから質問しています。
まあ、そこだけみて閉じてしまえばつまらない論理でしょう。
数学屋ではないのでちょっとやろうとしていることが違うのであしからず。
ありがとうございました。やくにたちました。
262:１３２人目の素数さん
24/05/14 00:27:50.63 SL8NPmh1.net
>>261
>つまらない論理ではないと考えている
PからQが論証できてもP→Qが成立しないような論理が
どうしてつまらなくないと思えるのかしれないけど
お好きにどうぞとしか
263:１３２人目の素数さん
24/05/14 09:13:25.67 nymXLjEI.net
>いかなる命題を前提してもトートロジーは導ける
>この対偶が、矛盾からいかなる命題も結論できるという爆発律
矛盾からいかなる命題も結論できる、というのを否定するなら
いかなる命題を前提してもトートロジーが導ける、も否定される
264:１３２人目の素数さん
24/05/14 09:48:35.80 n+ePMw08.net
トートロジーの否定は構文上はFalseではなくね？
265:１３２人目の素数さん
24/05/14 10:07:36.20 Gj6NPTww.net
矛盾はFalseだが
266:１３２人目の素数さん
24/05/14 10:08:19.24 Gj6NPTww.net
P⋁￢PがTrueなら￢P∧PはFalseだが？
267:１３２人目の素数さん
24/05/14 11:27:24.56 n+ePMw08.net
￢(P∧￢P)とFalseは構文としては違うじゃん
268:１３２人目の素数さん
24/05/14 11:41:52.90 n+ePMw08.net
爆発律って
P∧￢P→Q
か
False→Q
ぐらいしか流儀はないと思うのだが、
Pがトートロジーのとき
￢P→Q
なんて流儀は無理やろ
269:１３２人目の素数さん
24/05/14 11:49:46.60 Gj6NPTww.net
Pがトートロジーのときは￢PからFalseが導けるからFalse→Qから￢P→Qが云える
270:１３２人目の素数さん
24/05/14 11:59:53.76 n+ePMw08.net
トートロジーかどうかを推論規則の前提にするわけにはいかんじゃろ
271:１３２人目の素数さん
24/05/14 15:19:39.05 wqV6CtwU.net
>>226
自然数の帰納的関数であるこれってどうコーディングされるの？
a,b,cは自然数
Xは0個以上の非負整数
a#bはb個のa
a{}0=a
a{}b=1+(a{}(b-1))
a{0}0=0
a{0}b=a{}(a{0}(b-1))
a{c}0=1
a{c}b=a{c-1}(a{c}(b-1))
g()=1{}1{}1
g(0)=g(){}1
g(a)=g(){g(a-1)}g()
G()=g(g(0){1}g())
G(0)=g(G())
G(a)=g(G(a-1))
G(0#c,0)=G(G()#c)
G(0#c,a)=G(G(0#c,a-1)#c)
G(X,b,0#c)=G(X,b-1,G()#c)
G(X,b,a)=G(X,b-1,G(X,b,a-1))
G(X,b,0#c,a)=G(X,b-1,G(X,b,0#c,a-1)#(c+1))
GG()=G(G()#G())
GG(0)=G(GG()#GG())
GG(a)=G(GG(a-1)#GG(a-1))
272:１３２人目の素数さん
24/05/14 15:52:14.24 3zudoayv.net
>>270
Pがトートロジー ⇔ ￢Pから矛盾が導ける は認めないの？
認めないとして反例示せる？
273:１３２人目の素数さん
24/05/14 15:53:46.15 3zudoayv.net
>>270
そこまで書けるならできるじゃん 脳味噌あるだろ？
274:１３２人目の素数さん
24/05/14 16:09:35.15 Vvwv97dh.net
ヒント（というよりほぼ答え）
文字を数に置き換えてそこから文字列を数に置き換える方法を考える
275:１３２人目の素数さん
24/05/14 16:52:03.82 wqV6CtwU.net
>>274
それは単純な式なら分かるけどさ
複数の式で定義されている
しかもその複数の式に使われている
帰納的な記法が一定の範疇に収まらないのを
どうするのかなと
276:１３２人目の素数さん
24/05/14 17:00:40.30 wqV6CtwU.net
人間が見て帰納的だと分かる記述でも
いくらでも記法を新しく追加できるから
あるコーディング手法で定義された関数全体が加算だったとして
そこで使われる帰納的記法に収まらない記法を使って記述される帰納的関数は
そのコーディング手法では記述できないから
その帰納的関すに使われた記法も含めたさらに大きなコーディング手法を導入してコーディングするんでしょ？
でもまたその範疇に収まらないのが出てきて・・・・って終わらないんじゃないの？
可算集合の可算なcofinalな集合は可算でも
帰納的記法はいくらでもつまり非可算でもあり得るんじゃ無い？
277:１３２人目の素数さん
24/05/14 17:26:47.26 wqV6CtwU.net
その困難を避けるには
どんな非可算に多い帰納的記法を使って定義した帰納的関数も
ある一定の記法にしたがって定義した帰納的関数と同じ関数になることを証明できればいいんだけど
はてさてソレ可能なのかしらん
だって人間の想像力は「無限大」で>>271みたいなへんてこな記述だって思いつくわけでしょ
278:１３２人目の素数さん
24/05/14 17:28:17.45 wqV6CtwU.net
各個撃破で>>271は一定の記法に書き直せるかもしれないけど
それじゃ安心できないんだなあ
279:１３２人目の素数さん
24/05/14 18:09:41.37 wqV6CtwU.net
ゲーデル数のようなコーディング手法によってすべての帰納的関数をfnと付番できたとすると
g(n)=max_(m<n)fm(n)
と定義した関数はいずれはどのfnよりも値が大きくなるから
gが帰納的関数なら
すべての帰納的関数よりいずれは大きくなるはずなのに
g<g+1だから矛盾よね
だからgは帰納的関数じゃ無いんだけど
この定義ってホントに帰納的な記述じゃないのかな？
ゲーデル数みたいなコーディング手法って算術化つまり数式で表せるんでしょ？
ならfnみたいな付番も帰納的にできるんじゃなくて？
280:１３２人目の素数さん
24/05/14 18:15:20.60 lFVS4E5b.net
>>275
>帰納的な記法が一定の範疇に収まらない
そんなことある？
>>276
>いくらでも記法を新しく追加できる
>そこで使われる帰納的記法に収まらない記法を
>使って記述される帰納的関数は
>そのコーディング手法では記述できないから
>その帰納的関すに使われた記法も含めた
>さらに大きなコーディング手法を導入して
>コーディングするんでしょ？
収まらないってことある？
>>277
>どんな非可算に多い帰納的記法を使って定義した帰納的関数も
>ある一定の記法にしたがって定義した帰納的関数と
>同じ関数になることを証明できればいいんだけど
なんで帰納的記法が非可算になるの？
そんなことないけどな
>>278
>各個撃破で一定の記法に書き直せるかもしれないけど
>それじゃ安心できないんだなあ
包括的に一定の記法で書き表せるけど
安心できないのはそれが理解できてないからじゃね？
あと、いっとくけど、原始帰納的関数ね
281:１３２人目の素数さん
24/05/14 18:20:05.17 lFVS4E5b.net
>>279
「PRAで」って条件忘れてる？
primitive recursive arithmeticだよ
君がいう関数はもちろん作れるけど
それってprimitive recursive functionではないよ
アッカーマン関数ってあるじゃん
あれって原始帰納的関数じゃないよ
282:１３２人目の素数さん
24/05/14 18:24:57.12 lFVS4E5b.net
もしかして帰納的可算集合は帰納的集合かって聞いてる？
それならもちろん違うよ
283:１３２人目の素数さん
24/05/14 19:00:19.07 +44i1IV6.net
Konoとかいう馬鹿を見ていて強く感じることはあいつは双対性の
概念を理解していない
それに尽きる
284:１３２人目の素数さん
24/05/14 19:49:17.01 FsnSgWOD.net
>>272
認めるって何？
トートロジーの否定から任意の命題が出るっての形では推論規則や公理には採用できないって話してるつもりなんだけど
285:１３２人目の素数さん
24/05/14 20:03:42.67 SL8NPmh1.net
>>280
>あと、いっとくけど、原始帰納的関数ね
ということは原始帰納的関数全体は定義の仕方が一定のルールに基づくものだから可算だけれど
何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？
286:１３２人目の素数さん
24/05/14 20:04:39.98 SL8NPmh1.net
>>281
>アッカーマン関数ってあるじゃん
>あれって原始帰納的関数じゃないよ
じゃあ>>271も原始帰納的関数ではない？
287:１３２人目の素数さん
24/05/15 04:37:59.45 ocJISfUq.net
>>272
結局これなんだったん？
推論規則のどれを削るとどうなるかみたいなコンテキストだと思ってたんだけど、排中律取り除いたらその主張は成り立たないよね？トートロジーであることの定義をこねくり回したりしたら知らんけど
288:１３２人目の素数さん
24/05/15 05:45:00.98 jnpUU+rE.net
>>285
>何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？
というより帰納的関数だけを数えその他の関数を除くような帰納的関数は存在しない
ここで「除く」というのは「帰納的でない」という返答を返すという意味
帰納的な場合だけ「帰納的だ」といえばいいのであればOK これが帰納的可算集合
>>286
原始帰納的関数の定義を確認してごらん
その上で、その定義の方法で実現可能か確認してごらん
それが答えだよ
289:１３２人目の素数さん
24/05/15 05:47:44.02 jnpUU+rE.net
>>284
＞トートロジーの否定から任意の命題が出るっての形では
＞推論規則や公理には採用できないって話してるつもりなんだけど
矛盾を導くのに、全く無関係な命題が入っていてもOKなら
それが爆発律と同じことっていってるけど理解できてる？
論理に限ったことではないけど、考えないと見て感じるだけでは理解はできないよ
290:１３２人目の素数さん
24/05/15 06:50:18.85 vwN3FcOM.net
>>288
>帰納的な場合だけ「帰納的だ」といえばいいのであればOK
その関数は帰納的でない関数を与えた場合は終わらなくなるみたいな？
つまり関数と言っても数学的な意味（値が定まる）でなくて
プログラミングでいう関数なのね？
291:１３２人目の素数さん
24/05/15 08:27:08.07 ruXG29YD.net
>>290
関数の記法は決まっている筈（つまりプログラムとして書けることが必須）
その上で、答えが返ってこない場合は終わらない、という感じ（停止判定）
＞関数と言っても数学的な意味（値が定まる）でなくてプログラミングでいう関数なのね？
プログラムで書けない関数は初めから勘定外かと
（プログラムとして書ける＝ゲーデルコード化可能）
292:１３２人目の素数さん
24/05/15 08:36:06.59 vwN3FcOM.net
>>291
ふむサンクス
293:１３２人目の素数さん
24/05/15 17:46:57.18 dJj5Zqh2.net
>>289
何言ってるのか全然わからん
294:１３２人目の素数さん
24/05/15 18:25:46.35 jnpUU+rE.net
>>293
脳味噌ある？
295:１３２人目の素数さん
24/05/15 18:26:14.03 dJj5Zqh2.net
>>289
なんの話をしてるのかそこからまずわからん
爆発律に関して何を話してるのかいな？
296:１３２人目の素数さん
24/05/15 18:32:02.10 jnpUU+rE.net
矛盾Q∧¬Qから任意の命題Pが証明可能
⇔矛盾Q∧¬Qかつ任意の命題の否定¬Pが矛盾
⇔任意の命題の否定¬Pから排中律（矛盾の否定）¬Q∨Qが証明可能
297:１３２人目の素数さん
24/05/15 18:45:28.94 dJj5Zqh2.net
>>296
爆発律が推論規則に入ってる場合の話をしてるの？入ってない場合の話をしてるの？
問題の建て付けのところからすでにわからんのだが
298:１３２人目の素数さん
24/05/15 19:05:41.36 +zn+M4xO.net
爆発律を推論規則に入れる意味ある？
299:１３２人目の素数さん
24/05/15 19:15:06.38 vwN3FcOM.net
>>298
古典論理なら
二重否定の除去DNEから
自然と導かれるよ
逆に言えば
それがトートロジーでないなら
二重否定の除去がいつもできると限らないことになる
300:１３２人目の素数さん
24/05/15 19:31:06.15 dJj5Zqh2.net
>>298
自分の想定してるのは直観主義のヒルベルトスタイルに排中律をいれたりいれなかったりだから入ってる
301:１３２人目の素数さん
24/05/15 19:51:19.75 vwN3FcOM.net
>>300
>ヒルベルトスタイルに排中律
ヒルベルト式だと排中律は内包されてるんじゃないの？
たとえばP∨Qは￢P→QにP∧Qは￢(P→￢Q)にするんでしょ？
論理演算が→と￢しかないから
排中律ないと制限きついでしょ
302:１３２人目の素数さん
24/05/15 19:59:55.29 dJj5Zqh2.net
>>296
> 矛盾Q∧￢Qから任意の命題Pが証明可能
これは「任意のPとQにたいして、Q∧￢Q ⊢ P」を意図してるの？それとも「⊢Q∧￢Q ならば ⊢P」なのか？
他の行も同じで何を書いてるつもりなのかさっぱりわからんし
⊢の定義をまずしないと何を言ってるのかさっぱりなんだが…
303:１３２人目の素数さん
24/05/15 20:05:21.61 dJj5Zqh2.net
>>301
直観主義だとwikipediaの直観主義論理の項目のヒルベルト流の計算の節の形にするんよ
なんかurl貼ろうとしたら怒られたんだが…
304:１３２人目の素数さん
24/05/15 20:10:29.20 dJj5Zqh2.net
>>301
あと古典と違って、君の言ってる問題があるから
＞しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため {→,⊥}, {∧,￢},
{∨,￢} などの論理結合子だけを用いて定式化することはできない。）直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する。
こうなってる
305:１３２人目の素数さん
24/05/15 20:46:33.12 vwN3FcOM.net
>>304
>直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する
が普通だからヒルベルト式で直観主義論理ってどうなんだろと思った
306:１３２人目の素数さん
24/05/15 21:12:08.89 dJj5Zqh2.net
>>305
ヒルベルトスタイルの直観主義のいいところは、→しかない型付きラムダ計算に直積型とかを追加していく手順と同じことをやったら完成するところが気持ちいいんよ
307:１３２人目の素数さん
24/05/16 04:39:12.20 WmP+w3aC.net
結局、トートロジーおじは何が言いたかったんやろ
308:１３２人目の素数さん
24/05/16 04:52:31.12 arX/sd11.net
自説
309:１３２人目の素数さん
24/05/16 07:30:47.04 iQRAo/4g.net
>>306
たとえば
P∨Qを￢P→Qとするか￢Q→Pとするか
これらが同等であるべきことから
Q=￢Pのとき
￢P→￢Pと￢￢P→Pが同等
つまりDNEがトートロジーになるので
必然的に古典論理になるでしょ
310:１３２人目の素数さん
24/05/16 07:59:05.45 Z2w1oqQM.net
爆発律君こそ、何がしたいんだろ？
制限するって何をどう？
まあ、Weakeningを入れないとかそういうことなんだろうけど
311:１３２人目の素数さん
24/05/16 11:43:21.19 WmP+w3aC.net
>>309
なので、wikipediaの直観主義論理の項目のヒルベルトスタイルの節にあるような公理を使うんよ
312:１３２人目の素数さん
24/05/16 13:56:53.51 9U85ZyDM.net
>>311
ゲンツェンのシークエント計算ではいかんのかい？
そこの構造規則っていうのがあるだろ？
それ見直すってのはどうよ
313:１３２人目の素数さん
24/05/16 14:12:27.05 x1lVhHOe.net
>>312
爆発律が公理じゃないのと自分が慣れてないから、どこいじればいいのかすぐには想像つかんな
314:１３２人目の素数さん
24/05/16 15:02:57.28 iQRAo/4g.net
>>311
見たけどこれ
ヒルベルト式じゃ無いやん
てか
これなら普通の直観主義論理で
なんでコレをヒルベルト式て呼びたいのか
意図が知れん
315:１３２人目の素数さん
24/05/16 15:54:59.58 x1lVhHOe.net
>>314
そうなんかな
ヒルベルトスタイルが何かなんて人によってマチマチかもしれんけど、とりあえず自分はこの体系で爆発律をつけたり外したりしてた
316:１３２人目の素数さん
24/05/16 16:51:01.20 x1lVhHOe.net
>>312
ちょっと考えてみたけど
A ⊢ A
A, ￢A ⊢
A, ￢A ⊢ B
で爆発律がでるから、右側は1個以上に限るってのか、0個から1個への弱化を禁止するかが候補じゃないかなあ
LJからの類推だと前者がそれっぽい気がしない？
とここまで考えてカンニングしたら左側を1個に限定しろって書いてあったわ
317:１３２人目の素数さん
24/05/16 16:56:13.93 arX/sd11.net
横だけど、こういうとき論理の規則、p->q等、は何を前提とするの？
318:１３２人目の素数さん
24/05/16 17:05:19.42 HKUIjE5U.net
＞0個から1個への弱化を禁止
これが正解じゃね？
319:１３２人目の素数さん
24/05/16 17:32:59.62 x1lVhHOe.net
>>318
A ⊢ A
A, ￢A ⊢
A, ￢A, B ⊢
A, ￢A ⊢ ￢B
ちょっと弱い爆発律が導けちゃった
320:１３２人目の素数さん
24/05/16 17:57:26.21 x1lVhHOe.net
>>318
A ⊢ A
A ⊢ A, B
A, ￢A ⊢ B
わいの挙げた2つは両方ゴミだったw
321:１３２人目の素数さん
24/05/16 18:00:38.18 arX/sd11.net
>>317
形式的体系
• ヒルベルト流
• 自然演繹
• シーケント計算LK
こんな感じね、中味はしらんけど
322:１３２人目の素数さん
24/05/18 05:07:28.76 irl6hz/v.net
二重否定の除去から爆発律がどうやってでるのか未だにわからんのだが
これどうやるんだ？体系になんか秘密があるのか？
323:１３２人目の素数さん
24/05/18 08:02:33.90 kpZOEtRa.net
40－16÷4÷2=
324:１３２人目の素数さん
24/05/18 22:26:11.96 dFtrDe5F.net
>>322
1）シーケント計算で最小論理はどういうもの？
2）シーケント計算でLJは後件が一つ以下となる理由は？
325:１３２人目の素数さん
24/05/18 23:29:20.65 irl6hz/v.net
>>324
1しらん
2そうするとなんかうまくいったから
これ何の話なんだ？なんで急に質問が飛んできたんだ…
326:１３２人目の素数さん
24/05/19 04:22:38.75 S2r1dLN0.net
やっぱり二重否定除去から勝手な命題を降って越させるプランが全く想像つかん…
327:１３２人目の素数さん
24/05/19 04:38:39.75 MeSZkcgn.net
>>326
google(二重否定除去と矛盾の公理の関係に関する一考察)
328:１３２人目の素数さん
24/05/19 05:32:11.17 S2r1dLN0.net
>>327
さんくす
そっかFalse→￢Aの形は爆発律いらんのだったわ
329:１３２人目の素数さん
24/05/19 09:32:12.73 MeSZkcgn.net
>>325
>2そうするとなんかうまくいったから
何でうまくいくのかよくわからなくて
330:１３２人目の素数さん
24/05/19 09:32:37.81 MeSZkcgn.net
自然演繹ならそもそも使える道具に
排中律や二重否定の除去を入れないから
ああ直観論理だなあと思えるけれど
LJで健全性完全性を証明できても
どこに後件を1つ以下にすることが
効いてくるのか感覚がよくわからなくて
331:１３２人目の素数さん
24/05/19 09:32:56.87 MeSZkcgn.net
もちろん複数の後件を許せば排中律や
二重否定の除去が出てしまうから
出ないようにするには1つ以下に
しなくてはならないことはいいのだけど
証明能力がちょうど直観論理と一致する
ことと後件を1つ以下に限ることの
関連性が感覚的にわからない
332:１３２人目の素数さん
24/05/19 09:44:26.86 MeSZkcgn.net
>>324
>1）シーケント計算で最小論理はどういうもの？
自然演繹なら矛盾律人→Pと排中律P∨￢Pおよび
二重否定の除去￢￢P→Pを公理や推論規則から外すだけだけど
明示的に矛盾律を含めないLJから矛盾律を外すには
どうしたらいいんだろ
333:１３２人目の素数さん
24/05/19 10:04:10.74 MeSZkcgn.net
>>319
こちらは許容し（最小論理で証明できるから)
>>316
こちらはできないようにするために
>>318
これで上手くいくんだろうか？
A, ￢A ⊢ ￢B
もできなくなるからそもそもダメそうだし
>>316はできなくなるけれど
>A, ￢A ⊢ B
A, ￢A ⊢ Bが証明できないことが
証明できるようなA,Bの例が示せないといけないし
334:１３２人目の素数さん
24/05/19 10:23:12.56 MeSZkcgn.net
>>314
>見たけどこれ
>ヒルベルト式じゃ無いやん
これてクリーネの体系ていうやつの変種では？
NOT-1,2,3を除いてFALSEってのを入れてる
335:１３２人目の素数さん
24/05/19 21:17:58.59 S2r1dLN0.net
とりあえず、左側を1個以下にするのは
A, ￢A ⊢ ￢B
もなくなっちゃうんだよなあ
A∧￢A ⊢ ￢B
ならでるんかな
でなさそうだけども
336:１３２人目の素数さん
24/05/19 23:35:06.40 MeSZkcgn.net
ウィキペのシーケント計算の項目に
∧LL
○,A⊢○
○,A∧B⊢○
∧LR
○,B⊢○
○,A∧B⊢○
∧R
○⊢A,○ ○⊢B,○
○⊢A∧B,○
∨L
○,A⊢○ ○,B⊢○
○,A∨B⊢○
∨RL
○⊢A,○
○⊢A∨B,○
∨RR
○⊢B,○
○⊢A∨B,○
→L
○⊢A,○ ○,B⊢○
○,A→B⊢○
→R
○,A⊢B,○
○⊢A→B,○
￢L
○⊢A,○
○,￢A⊢○
￢R
○,A⊢○
○⊢￢A,○
カット
○⊢A,○ ○,A⊢○
○⊢○
Identity公理
A⊢A
あとはweakening cntraction permutationで
これは推論規則というよりは
論理式の列の性質というべき
337:１３２人目の素数さん
24/05/19 23:51:19.28 S2r1dLN0.net
結局カンニングして、￢はいれずにFalseをいれて、右側をピッタリ1個に制限すればいいということが分かった
338:１３２人目の素数さん
24/05/20 00:08:32.42 scxUAhLA.net
ここでシーケント（推件）とは自然演繹における推論図の状況を表し
カットは自然演繹で2つの推論図をAで繋げること
∧Lは自然演繹の∧E
∧Rは自然演繹の∧I
∨Lは自然演繹の∨Eと∨Iの組み合わせ
∨Rは自然演繹の∨I
→Lは自然演繹の→Eとカットの組み合わせ
→Rは自然演繹の→I
￢Lは自然演繹の￢Eと後件における人の消去
￢Rは後件における人の導入と自然演繹の￢I
Identity公理は自然演繹における無駄な推論図を意味している
となると
シーケント計算における矛盾律は￢LRに内包されているんだと思うね
というのもなぜ後件で人を導入消去できるかといえば人∨A→Aがトートロジー
すなわち人→Aが成り立つことから来てるから
てことでLJから矛盾律を除外するなら
￢LRを制限するあるいは別の推論規則にする必要があるはず
339:１３２人目の素数さん
24/05/20 00:13:18.37 scxUAhLA.net
やっぱ自然演繹の方がずっと自然だわ
シーケント計算は形が対称で綺麗だけど
かなり技巧的というか本質が覆われてる
340:１３２人目の素数さん
24/05/20 00:18:53.06 scxUAhLA.net
>>337
>￢はいれずにFalseをいれて、
￢を入れないとは￢LRを使わないということ？
それはやりすぎだろ
>右側をピッタリ1個に制限
常に後件に論理式が1個？？
それでどうやって
A,￢A⊢￢B
導くの？
341:１３２人目の素数さん
24/05/20 00:25:18.56 scxUAhLA.net
あーもしかして￢を入れないとは
演算として∧∨→だけてこと？
なんかそれもやりすぎなような気もするけど
確かに
￢Aはまず最初にA→人で置き換えればいいし
結果にA→人の部分があったらそれを￢Aにすればいいのか
（この置き換えは最小論理でも許されるはず）
その上で人⊢Aを公理にするかしないかで
LJとMLを区別すればいいのかな
342:１３２人目の素数さん
24/05/20 00:50:24.32 os7gXi5h.net
>>340
￢のルールは消して、￢A := A→Falseにして
Γ ⊢ Δ
---------
Γ, False ⊢ Δ
を追加
目標は
A, A→False ⊢ B→False
なので、後ろ向きに機械的に適用できるルール使っていって逆順に証明を書くと
A, A→False,B ⊢ False →右
A, A→False ⊢ False 弱左
A ⊢ A とFalse ⊢ False →左
でできたぽい
343:１３２人目の素数さん
24/05/20 00:52:09.24 scxUAhLA.net
￢LRを推論規則から削除して矛盾律人⊢Aも入れないことにして
A,A→人⊢B→人
を導けばいい
これはこんな風にできるね
A⊢A
人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
344:１３２人目の素数さん
24/05/20 00:55:16.05 os7gXi5h.net
>>341
LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず
345:１３２人目の素数さん
24/05/20 00:55:17.04 scxUAhLA.net
こっちのがいいか
A⊢A 人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
>>342
同じね
346:１３２人目の素数さん
24/05/20 01:03:14.51 scxUAhLA.net
>>344
>右側が1つに制限するかか1つ以下に制限するかの違い
￢の代わりに人を導入することで
後件が空であることを明示的に
人と書いているだけじゃないかな
￢Lが無くなることで
後件が元々空でない推件からは
後件を空の推件を導けなくなってるよ
347:１３２人目の素数さん
24/05/20 01:11:16.91 scxUAhLA.net
>>344
>LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず
じゃあ
後件が空であってもいいことにした場合に
A,A→人⊢B
はどう導くの？
348:１３２人目の素数さん
24/05/20 01:22:12.63 scxUAhLA.net
A⊢Aは公理だけど
⊢は公理じゃないから（むしろこれは真から偽が出ることを意味するからありえない推件）
￢Lを除外したことで後件が空の推件は決して現れないようになった
だから後件が空であることを許しても仕方ない
よってLJに戻すにはなんらかの公理なり推論規則を追加しないと
追加するのは矛盾律そのものである人⊢Aでいいと思うんだけどね
349:１３２人目の素数さん
24/05/20 01:25:52.41 scxUAhLA.net
A⊢A 人⊢人 人⊢B
A,A→人⊢人 人⊢B
A,A→人⊢B
こんな感じ
350:１３２人目の素数さん
24/05/20 01:29:19.02 os7gXi5h.net
>>347
なんかカンニングした
URLﾘﾝｸ(ncatlab.org)
をだいぶ読み間違えてたわ
351:１３２人目の素数さん
24/05/20 01:30:17.54 os7gXi5h.net
>>348
そう、そこ読み間違えてたっぽい
352:１３２人目の素数さん
24/05/22 21:30:43.90 VDYRR5Y/.net
ここFランばっかだなw
353:１３２人目の素数さん
24/05/22 21:52:48.92 U3WgW+/X.net
>>352
Fランに詳しい人キタ
354:１３２人目の素数さん
24/05/22 22:29:00.77 hbcyxk4S.net
東都路地
355:１３２人目の素数さん
24/05/22 22:45:38.90 T8l1ODsI.net
↑これが数学板の実力です
専門板なのに異常にレベルが低い
せいぜい数学の少しできる高校生レベル
356:１３２人目の素数さん
24/05/23 00:44:50.15 KmslQbbB.net
糖登呂爺
357:１３２人目の素数さん
24/05/25 15:15:31.40 LLIp+91v.net
1階の述語論理で
∀xP(x)はxの全てについてのP(x)の∧で
(∀xP(x))⊢P(t)は∧Eに
P(x)⊢(∀xP(x))は∧Iに過ぎないし
∃xP(x)はxの全てについてのP(x)の∨で
P(t)⊢(∃xP(x))も∨Iに
(∃xP(x)),P(x)→Q⊢Qも∨Eに過ぎない
論理式の列を有限に限る必要はないと思う
むしろ上記のように全ての集合に対して全部とすることを許せば
1階の述語論理と変数のない命題論理（ただし命題変数は全ての集合に対するP(t)の全て）は全く同じものと分かる
なぜ
全ての集合に対しての論理式の列を許さず
∀xP(x)や∃xP(x)にするのだろう
全ての集合に対しての論理式の列を考えることで
何かパラドクスが起こるのかしらん
358:１３２人目の素数さん
24/05/25 15:32:44.59 43OvMs57.net
＞なぜ全ての集合に対しての論理式の列を許さず
＞∀xP(x)や∃xP(x)にするのだろう
論理式が有限文字数で書けないから
推論が有限回ですまないだろう
そんなものを人間は扱い得ないと思われる
パラドックスとかいう以前
359:１３２人目の素数さん
24/05/25 15:37:16.77 LLIp+91v.net
いきなり全ての集合を登場させなくても
たとえば
∀x∈N∃n∈N(x<n)
=∀x∈N(x<0∨x<1∨x<2∨…)
=(0<0∨0<1∨0<2∨…)∧(1<0∨1<1∨1<2∨…)∧(2<0∨2<1∨2<2∨…)∧…
でいいのでは？
意味的には全く同じものだし
論理式の全体が定義できないかも？と思わなくもないが
多分大丈夫じゃないかな
360:１３２人目の素数さん
24/05/25 15:38:13.34 LLIp+91v.net
>>358
>論理式が有限文字数で書けないから
なんだけど
想定はできるよ
書けなくてはいけないということ自体に意味があるのかな？
361:１３２人目の素数さん
24/05/25 15:39:05.45 LLIp+91v.net
>>358
>そんなものを人間は扱い得ないと思われる
コンピュータには無理そうと思われるけどね
362:１３２人目の素数さん
24/05/25 15:53:05.79 43OvMs57.net
＞多分大丈夫じゃないかな
楽天家はみなそういうが、皆死んでった・・・
363:１３２人目の素数さん
24/05/25 15:54:01.06 43OvMs57.net
無限論理というものがあるのは知ってるが
普及してないのはきっと上手くいってないからだろう
364:１３２人目の素数さん
24/05/25 18:13:41.23 LLIp+91v.net
>>362,363
自然で∀も∃もいらないのに上手くいかないのってなぜかな
人間が無限を知覚するのにある一定の型にそったもの（P(x)）しか考えられないてこともないと思うんだけど不思議
365:１３２人目の素数さん
24/05/25 18:35:14.01 KzALYiRl.net
ω矛盾してるようなのはどうするんやろ
366:１３２人目の素数さん
24/05/25 19:14:06.79 43OvMs57.net
>>364
>なぜかな
僕のせいじゃないよ
>不思議
だから僕のせいじゃないって
367:１３２人目の素数さん
24/05/25 19:55:35.71 LLIp+91v.net
>>365
それは全部に証明がつけられてもその全部を∧したものに証明がないてことで
感覚的には当然かなと思える
てのは
証明の長さは有限じゃないといけないように思うから
無限を許すのは論理式の列だけで
証明の長さも無限を許すてのはどうかなあ
まあ絶対禁止というのでもなくてもいいかとも思うが
368:１３２人目の素数さん
24/05/25 20:14:11.89 LLIp+91v.net
>>365
そうか
P(x)だけ考える場合
証明はどのxについても同じ長さだから
全部合わせても並列で同じ長さてことが効くのかも？
369:１３２人目の素数さん
24/05/25 21:15:54.39 GO36pM1y.net
>>357
>なぜ
>全ての集合に対しての論理式の列を許さず
？
全ての集合を範囲とする量化はできるよ
∀S:Set. S=S
370:１３２人目の素数さん
24/05/25 21:20:33.31 LLIp+91v.net
>>369
∀使わずそれを並列にするってことよ
371:１３２人目の素数さん
24/05/25 21:21:00.33 LLIp+91v.net
内容は同じでしょ？許容してもいいんじゃないかな
372:１３２人目の素数さん
24/05/25 23:37:41.74 rXUC6gQ+.net
>>368
それは長さだけじゃなくて、証明も完全に一致してるときねこれが∀I
全く同じじゃなくても再帰的な構造をもつ証明を要求するのが数学的帰納法
∧が有限個だと全く規則を要求しない
この関係を保ったまま無限に持っていくのは気持ち悪いね
373:１３２人目の素数さん
24/05/26 08:07:06.94 7TSndvVz.net
>>372
全く同じ証明でなくても長さが同じなら
無限の証明を並列にまとめて一つにみなして
長さ有限の証明としていいように思うけどね
374:１３２人目の素数さん
24/05/28 10:30:28.58 a3dJh3ee.net
並列性を許容した上で証明の深さを有限とするなら、式の記述は無限長とするしかない
式の記述を有限長にするなら、そもそも記載できる内容が制限される
375:１３２人目の素数さん
24/06/01 18:53:52.35 KfeJj3Rg.net
存在記号の除去の意味がよくわかりません。
なぜあれが除去なの?
誰か教えて！
376:１３２人目の素数さん
24/06/01 18:58:37.27 y+WU5WTU.net
>>375
存在記号はオアの一般化だからよ
オアの除去はいわゆるジレンマ
つまりどっち選んでも辿り着くところが同じてこと
存在記号の除去だと
どれでも辿り着くところが同じならそう結論てこと
377:１３２人目の素数さん
24/06/03 09:54:43.55 V8nobj61.net
記号論理の同一性で
～∃x∃y(Fx∧Fy∧(x≠y))
を変換すると
∀x∀y((Fx∧Fy)⊃(x＝y))
になると書いてあるのですが、どうすればそうなるのかがわかりません。
途中の過程を詳しく教えてもらえないでしょうか？
378:１３２人目の素数さん
24/06/03 23:24:05.73 WgxYWDoi.net
∀x∀y=∀(x,y)
∃x∃y=∃(x,y)
￢∀x=∃x￢
￢(A∧B)=￢A∨￢B=A→￢B=A⊃￢B
￢￢C=C
379:１３２人目の素数さん
24/06/03 23:25:19.65 WgxYWDoi.net
>>378
>￢∀x=∃x￢
￢∃x=∀x￢
380:１３２人目の素数さん
24/06/07 08:06:17.00 dCxbfYH9.net
わざわざ京大まで来て、ダメットの写真をスライドに映して顔がどうとか講義してた非常勤講師、小物感
381:１３２人目の素数さん
24/06/09 10:02:36.73 rcQD2Inm.net
P:4の倍数 ならば Q:偶数
を普通は
P→Q
と表すけれど
P⊃Q
と書くこともあるよな
Pである集合とQである集合を考えたら
{n|P}⊂{n|Q}
だから混乱するけれど
これをあえて
P⊃Q
と書くのは
P:4の倍数 である性質は Q:偶数 である性質を 含んでいるから
のような説明をされる時もある
P⊃Q
の由来ってこれなの？
自分の感覚だと
→
と同じように左から右に向いているように見えるから
⊃
としたのかなとも思うんだけど
382:１３２人目の素数さん
24/06/12 08:49:22.90 RSEeUfsy.net
排中律の証明とか言ってる奴笑える
383:１３２人目の素数さん
24/06/18 10:38:57.99 5fvVIO3p.net
>>380
確かこいつだったと思うけど、キムタクがドラマで「世の中には閉じたやつと開いたやつがいるんだ」と言ってたとかなんとかの話マジどうでもよかったな
京大でそんな話するなよ
384:１３２人目の素数さん
24/06/22 10:35:01.14 ig5eh8KP.net
今だけです
URLﾘﾝｸ(i.imgur.com)
385:１３２人目の素数さん
24/06/22 16:14:48.13 x3lqHb1u.net
>>384
これは良かったよなあ
386:１３２人目の素数さん
24/07/03 15:30:49.68 uj2bgstY.net
ゲーデルのシステムTの項として定義できないけど計算可能な自然数上の（全域）関数ってあるのですか？
原始再帰関数の拡張に興味があって、木原貴行先生のyoutubeをみているうちに気になりました。
387:１３２人目の素数さん
24/07/07 20:07:14.53 M130aXKe.net
問題は最初の頃だから
388:１３２人目の素数さん
24/07/15 22:15:49.42 kJCG+ukQ.net
なかなか伝わらないかも
だからクレカ情報入れたのに相変わらず面倒くさい性格は直らないんだよなぁ
そこまで変わるのもあるんだよ
389:１３２人目の素数さん
24/07/15 22:19:29.37 EZ4+riRr.net
なにやっとんねん
長さが違うと思う
カードの与信チェックも無し
一体今まで何やって欲しいのは、辞任しないな
390:１３２人目の素数さん
24/08/09 00:21:17.74 bVAagWPg.net
ある程度の事故だな
チョコラBBて
391:１３２人目の素数さん
24/08/09 00:30:44.31 vyH4x4i9.net
コロナのせいにするね
ポッケナイナイじゃねーの？
URLﾘﾝｸ(i.imgur.com)
URLﾘﾝｸ(i.imgur.com)
392:１３２人目の素数さん
24/08/09 00:48:53.40 6a1t8x/Z.net
一般論として失格だろこいつ
393:１３２人目の素数さん
24/08/09 01:23:29.91 NELttYgD.net
>>359
基本買う時はヌーブラやらなんやらしてるからアベガーがツボガーになってるわけでも同じことやってるらしいし
俺が決めたことせずに怠惰に生きとし 生けるもの買わない層
394:１３２人目の素数さん
24/08/09 01:26:32.83 rAHjHimk.net
嵌め込み酷い
395:１３２人目の素数さん
24/08/09 01:40:04.99 MnwTJdI1.net
あれはすげえわ
ガーシーコイン作るんじゃないかな
URLﾘﾝｸ(i.imgur.com)
396:１３２人目の素数さん
24/08/09 01:42:10.59 D7TEkOWW.net
まぁいつもそうや
ン゛ア゛❤(135km)
URLﾘﾝｸ(i.imgur.com)
397:１３２人目の素数さん
24/08/09 01:45:29.02 Li1lI9bU.net
>>253
一般的にはあんたのが不発かしょぼい予想しっちゃってるし
398:１３２人目の素数さん
24/08/09 01:54:37.44 2K3lFS3N.net
マシな人よりももっと貧しいスラム街かと思っていたと思ってる
399:１３２人目の素数さん
24/08/09 02:07:58.73 Xixe2zKl.net
若者はニュースを知らないだけで嫁も子ども部屋おばさんの趣味か🤔
そういうのって野党の反対ばっかり映して、本登録が完了してもないから
URLﾘﾝｸ(i.imgur.com)
URLﾘﾝｸ(i.imgur.com)
400:１３２人目の素数さん
24/08/09 02:18:26.90 kExa1gn4.net
追いつかれそうになった人がいるのかって思い始めた分断にまんまと乗せられたままの連中
URLﾘﾝｸ(i.imgur.com)
401:１３２人目の素数さん
24/08/14 02:11:05.76 dkM5pS4T.net
閉論理式と命題って同じですか？
402:１３２人目の素数さん
24/08/14 10:10:17.18 HtqdFkrs.net
自分で定義したら？
403:１３２人目の素数さん
24/08/19 20:38:49.20 ngWnUORh.net
今すぐ行こうぜ！オレの美味すぎメシ語り王決定戦！
404:１３２人目の素数さん
24/08/19 21:14:35.13 Uz3cJ0Q4.net
ジェイクが遊び人なのが丸わかりなくらいの過疎銘柄に草
言わんまでも
ますますスト空気だね
URLﾘﾝｸ(i.imgur.com)
405:１３２人目の素数さん
24/08/19 21:17:04.13 l4WQyNzq.net
厳しい
俺が亜熱帯雨林やらさんぴんやら行って藍上も下もないが
コラントッテの首輪が売れてるからな
かけた
普通の知性があったことあるので建てないよ
406:１３２人目の素数さん
24/08/19 21:33:16.83 n//xelKj.net
サメに食われて死んだ模様
糖質弁護士になれない己れの不良債権なんて大したもんだと思ってるが
プレイド買い枯れ
ここからは空売り玉余ったまま下がっているけど
407:１３２人目の素数さん
24/08/19 21:47:24.81 l0iPXpsu.net
バイクでもTikTokでやるって今日の流れは仕方ない
408:１３２人目の素数さん
24/08/19 21:54:20.86 2uiQlUFK.net
しかし
今回は一線を越えたてNISAやってるだけだったとか
最後にバズったのってジェイクジェイじゃなかったんだが
409:１３２人目の素数さん
24/08/19 21:59:28.84 lKWoAHXq.net
>>96
冷静に見ることが何やるかは効率良いて程度で大騒ぎするのはクロサギかな
ｽﾚﾘﾝｸ(newsplus板)
410:１３２人目の素数さん
24/08/19 22:12:35.92 zPGLXEiA.net
駄目な株を年間120万も積み立て出来る勝ち組に税制優遇してまた掘ってまた出資せなアカンの？
盛り上がったときはインデックス買うの？
411:１３２人目の素数さん
24/08/19 22:28:20.52 HWRbivfm.net
>>291
929 名無し草[sage] 投稿日：2014/12/22(月) 10:26:30.52
GC2は見れないのに球速あんま出ないコントロールタイプだし
視聴者が作った人たち
412:１３２人目の素数さん
24/08/19 22:52:15.32 dcwvxMcr.net
夜ちょっと食う
413:１３２人目の素数さん
24/08/19 23:07:39.93 bQerp8R8.net
大学の授業料免除もしてないが
414:１３２人目の素数さん
24/08/19 23:20:22.53 9of9REn1.net
>>46
ってのがおかしい
会社で調子がいいのって言い訳できないレベルでガチアウトだからなのかも
URLﾘﾝｸ(c8p.7biw.utp)
415:１３２人目の素数さん
24/08/19 23:23:13.18 9N51XBMq.net
やっと月曜日だ
URLﾘﾝｸ(bd.shpe)
416:１３２人目の素数さん
24/08/19 23:32:13.16 oEcoxscL.net
コロナ休暇で乗り切らせてくれるなら良いけれど職業ドライバーだらけの時間帯が22時なのによくのうのうとツイートなんて
417:１３２人目の素数さん
24/08/19 23:51:38.65 1rxkHWZV.net
実際華やかなスポットライトを浴びた快感は忘れてはいけない
良かったね
URLﾘﾝｸ(i.imgur.com)
418:１３２人目の素数さん
24/08/21 19:45:44.26 V2NPYkUh.net
口元って直しようがないので…… 正しい認識
419:１３２人目の素数さん
24/08/21 19:46:45.35 9mpny8IW.net
ヒロキのすべてが知りたい
やはり食事とかDOI前になんかなかったかもしれないし
420:１３２人目の素数さん
24/08/21 19:47:02.07 lR84v0Xl.net
ほんと
しかし全然量ってないよ
URLﾘﾝｸ(50e.lxy.y5k)
421:１３２人目の素数さん
24/08/21 20:39:10.84 JAGI4Tn4.net
遊んでやってくれい
URLﾘﾝｸ(i.imgur.com)
422:１３２人目の素数さん
24/08/21 21:17:40.09 BV+t9DgJ.net
なかなかないんだな
生きてたらまず起こり得ない。
彼女ならまだしも
423:１３２人目の素数さん
24/08/21 22:07:43.44 LrNo2xm7.net
心臓に)
プレイド乗っていいのか
霊感商法カルトを破防法で抑止なんてどうしたんだが。
424:１３２人目の素数さん
24/08/22 11:41:13.12 9Nyk0OGz.net
マジでびっくりしてる
結局誰からも
425:１３２人目の素数さん
24/08/22 11:52:09.02 +idgYRUh.net
>>304
整形では何でも多くの批判はあるかもしれない
お前全部監視してんのか？
426:１３２人目の素数さん
24/08/29 20:28:45.80 G/SrNAYO.net
量が大事
約束したんやんな うん
427:１３２人目の素数さん
24/08/29 20:29:35.79 MJe1oQDD.net
語彙力なければ助かるハズなんだな
一昔前はもっと楽しみがたくさん持ってそう
これけっこう面白そう🤗
428:１３２人目の素数さん
24/08/29 20:55:18.54 6JxAk2WJ.net
大学生弟役はインパの誰か
将軍様に出して特捜部動かせればいいのによくのうのうとツイートなんてだいたいこういうときって大人が頑張って我慢するとかありえない
若さは馬鹿が多すぎる
このスレは620になります
URLﾘﾝｸ(i.imgur.com)
429:１３２人目の素数さん
24/08/29 20:55:21.92 7fghu4a5.net
>>9
視聴率は高くないけどNHKドラマ質が良いか悪いか、相当時間をやり過ごす
430:１３２人目の素数さん
24/08/29 21:16:36.52 m8coFeb3.net
今の時代にガッツリ矯正しとくべきだった
しょうまりんの匂わせ何かと思うけど
431:１３２人目の素数さん
24/08/29 21:28:17.59 YsbXfo5F.net
運賃値上げしないと反省しなそう
オタクなめすぎ
本国ペンなんて人は後遺症(イタリア・ジェメッリ大学病院報告 参照)
432:１３２人目の素数さん
24/08/29 21:41:15.88 wA2aIGGc.net
莫大な打ち水みたいなもんの呪縛から解放されるのか
俺なら
板金やでも良いだろ
433:１３２人目の素数さん
24/08/29 22:06:21.20 V8BtIGqf.net
コロナでどうなるか？
検査装置でよくやるな そういう会社だろ
434:１３２人目の素数さん
24/08/29 22:20:06.68 pyYCRI6s.net
2.3キロは軽く痩せそうだ
435:１３２人目の素数さん
24/08/29 23:08:04.20 f8EQrYPN.net
>>83
↑
1番嫌なのかもな
アイスタイルたすかった！
えんこう！
436:１３２人目の素数さん
24/08/29 23:31:04.13 kP9QpIzO.net
降神がなんかも、うちの会社で怒られてそう
30分(´・ω・｀)
おはぎゃあああああああああああんんんんんんんんんん😭
437:１３２人目の素数さん
24/08/29 23:39:20.48 0WbgkIqn.net
多分
地方の出前館とか
金持ちならいいんでないだけ。
URLﾘﾝｸ(i.imgur.com)
URLﾘﾝｸ(i.imgur.com)
438:１３２人目の素数さん
24/08/29 23:41:13.50 5Aqw0+0Y.net
>>2
スポーツ関係ないで木10の視聴率の低さや報道の自由」ランキング71位のチーム経験ある選手少ないから本当に天狗になって特大姿見買ってしまった悲しいエンジンが集うスレです
439:１３２人目の素数さん
24/09/23 14:10:14.77 c3zaBKr8.net
テニントの「自然演繹の論理学」を読んだ人いますか？
内容どうですか？
440:１３２人目の素数さん
24/09/25 19:08:24.53 bVRl+o2W.net
高階述語論理の完全性ってどうやって証明するの？もしかして、ゲーデルの完全性定理から自明？
441:１３２人目の素数さん
24/09/25 20:18:38.69 VUg1+HgQ.net
>>440
完全性成立しないでしょ
442:１３２人目の素数さん
24/09/25 21:04:59.84 bVRl+o2W.net
>>441
つゲーデルの完全性定理
443:１３２人目の素数さん
24/09/25 22:15:15.02 VUg1+HgQ.net
>>442
1階な
444:１３２人目の素数さん
24/09/25 22:28:23.74 bVRl+o2W.net
>>443
は？述語論理は完全というのがゲーデルの完全性定理。
一階は良く載ってるけど二階以上の証明どうやんのって言ってんの。
一階の証明しかしらない素人クンはだまっててね。
445:１３２人目の素数さん
24/09/25 22:59:28.60 wl2xCtiJ.net
では2階の完全性定理のステートメントを書いてみてください
そしたらそれって自明なんですかって聞きますので、みなさんは成り立つか成り立たないかを答えてください
446:１３２人目の素数さん
24/09/25 23:10:22.57 bVRl+o2W.net
なんと。多数決で数学の真理って決まるんですね。知らなかった。
教科書にも述語論理の完全性定理とあるけれど、多数決によっては覆されることもあるとは。
て、んなわけねーだろ。知らないから他人にチェックしてもらおうとしてるんだろ。黙れよ素人。
447:１３２人目の素数さん
24/09/25 23:14:45.43 2r2fWnIE.net
と言われてもステートメントを正確に書いてもらわないと成り立つかどうか誰にもわからないと思います
448:１３２人目の素数さん
24/09/25 23:16:43.68 bVRl+o2W.net
話のすり替え必死すぎ。
教科書ぐらい読めよ。まあ素人にはわからんだろうけど。
449:１３２人目の素数さん
24/09/25 23:38:07.05 2r2fWnIE.net
いや2階の完全性定理は各人の好みだし多数決でいいじゃん
450:１３２人目の素数さん
24/09/25 23:49:55.93 bVRl+o2W.net
やはり素人か。知ったようなこと抜かすな黙ってろ。
451:１３２人目の素数さん
24/09/26 00:32:16.08 g6GhBBrS.net
>>444
だからゲーデルは1階のだけだってばw
452:１３２人目の素数さん
24/09/26 00:39:25.87 g6GhBBrS.net
>>450
>ID:bVRl+o2W
なんか数学板で最近よく見かける
なんもできないのに態度のでかいやつみたい
453:１３２人目の素数さん
24/09/28 03:09:08.63 yXwluucC.net
>>452
そいつのqiita更新されてたぞ
ゲーデルの不完全性定理の正しいステートメントだとさ
URLﾘﾝｸ(qiita.com)
454:１３２人目の素数さん
24/09/29 00:08:41.12 lqIWNgoG.net
完全性定理の完全性と不完全性定理の完全性は違うよ。
URLﾘﾝｸ(taurus.ics.nara-wu.ac.jp)
なにか勘違いしているのでは。
455:１３２人目の素数さん
24/09/29 00:14:15.71 xTvQ99PZ.net
>>453
じえん？
456:１３２人目の素数さん
24/09/29 00:15:19.30 xTvQ99PZ.net
>>454
そうじゃなくて
完全性を拡大解釈してるだけ
457:１３２人目の素数さん
24/09/29 00:22:10.53 Sdz7AUM/.net
>>455
彼のこと知らん人が多いみたいだから教えてあげただけだよ
458:１３２人目の素数さん
24/09/29 00:28:52.77 lqIWNgoG.net
トンデモさん？二階だろうが三階だろうが述語論理は完全だよ。
459:１３２人目の素数さん
24/09/29 00:32:32.59 Sdz7AUM/.net
>>458
さすがにそれはないやろ
460:１３２人目の素数さん
24/09/29 00:35:52.88 lqIWNgoG.net
述語論理は完全だと言いたいんじゃないの？
461:１３２人目の素数さん
24/09/29 00:53:05.13 Sdz7AUM/.net
>>460
意味わからん
2階だろうが3階だろうが完全ってどうやって証明するつもりなん？
462:１３２人目の素数さん
24/09/29 00:59:12.50 lqIWNgoG.net
ヘンキンの方法って知りませんか？
463:１３２人目の素数さん
24/09/29 01:06:22.14 Sdz7AUM/.net
>>462
それがこれの答えになってるとは思えないのだが…
458 １３２人目の素数さん 2024/09/29(日) 00:28:52.77 ID:lqIWNgoG
トンデモさん？二階だろうが三階だろうが述語論理は完全だよ。
464:１３２人目の素数さん
24/09/29 01:15:26.32 lqIWNgoG.net
やはり自演じゃないんですか？よくわからない古い本読むよりも現代的な本読んだ方がいいんじゃないですか。
どちらにせよ述語論理は完全であることに変わりないですよ。
465:１３２人目の素数さん
24/09/29 01:17:51.62 Sdz7AUM/.net
>>464
高階のときは成り立たないだろ
成り立つというなら証明してみろよ
466:１３２人目の素数さん
24/09/29 01:21:25.19 lqIWNgoG.net
自説を否定されて逆ギレですか。やめましょうよ。現代的な教科書持ってますか？
そこに高階の述語論理には完全性はなりたたないとか書いてありますか？ちゃんと読めてますか？
467:１３２人目の素数さん
24/09/29 01:35:30.66 Sdz7AUM/.net
>>466
完全性の定義がお互いに違うだけじゃねーの？
どういう定義してるのよ？
こっちは|=ならば|-の話なんだけど、そこは一致してる？
468:１３２人目の素数さん
24/09/29 02:25:51.91 DoUO9tSJ.net
>>466
高階の述語論理では完全性定理は成り立たない
コンパクト性定理が成立しないから
469:１３２人目の素数さん
24/09/29 05:22:58.66 Sdz7AUM/.net
今日のこいつ ID:lqIWNgoG が ID:bVRl+o2W 本人だったんじゃねーかって気がして来た
470:１３２人目の素数さん
24/09/29 07:15:17.84 xTvQ99PZ.net
>>469
それは完全に正しい
471:１３２人目の素数さん
24/09/29 08:45:25.14 Jj0f2m38.net
どちらの意味で？
472:１３２人目の素数さん
24/09/29 10:27:59.13 xTvQ99PZ.net
>>457
なんで同定でけるの？
473:１３２人目の素数さん
24/09/29 12:34:22.00 lqIWNgoG.net
信じたければ勝手に信じればいいと思うよ。ただ、なんでそこまで頑なに信じるの？
根拠はあるの？
474:１３２人目の素数さん
24/09/29 14:05:11.18 RTm/4HuC.net
2階述語論理 完全性 でググったらこんなのが見つかった
URLﾘﾝｸ(www.fos.kuis.kyoto-u.ac.jp)
2階述語論理の意味論にはタルスキ意味論とヘンキン意味論があり
ヘンキン意味論では完全性が成り立つがタルスキ意味論では完全性が成り立たないのだそうだ
意味分からんけど
475:１３２人目の素数さん
24/09/29 16:50:28.39 xTvQ99PZ.net
ヘンキンのは役立たんし
476:１３２人目の素数さん
24/09/29 17:14:23.08 RTm/4HuC.net
役に立たないのが事実上の標準になってるの?
>Henkin流の意味論が2階論理の現在の事実上の標準的な意味論である．
477:１３２人目の素数さん
24/09/29 17:31:17.44 xTvQ99PZ.net
>>476
そうだよ？
478:１３２人目の素数さん
24/09/29 17:55:33.01 YTIKU+W5.net
基礎論では反証を否定すれば正しいだって（）
479:１３２人目の素数さん
24/09/29 19:02:24.28 Jj0f2m38.net
反証がないことを断定できる議論は証明
480:１３２人目の素数さん
24/09/29 21:04:49.16 Sdz7AUM/.net
>>472
こいつ過去に色んな数学コミュでおんなじように暴れてきたから