数理論理学（数学基礎論）　その14

1 ：１３２人目の素数さん：2019/03/22(金) 11:55:47.59 ID:oVa5RLRo.net

数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも
若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化などを参照）

前スレ
数学基礎論・数理論理学　その13
https://rio2016.5ch.net/test/read.cgi/math/1532721493/

148 ：１３２人目の素数さん：2020/03/31(火) 18:45:46 ID:+LMTnMxG.net

>>147
x=2のとき　f(2)=2
x=3のとき　f(3)=3
……

149 ：１３２人目の素数さん：2020/03/31(火) 18:51:38 ID:+LMTnMxG.net

このように

すべての数値に対してあるxが存在する

の翻訳は

xがfで，ある値を取るときに，fによって出力される値のすべてが，fの値域である

と読む

つまり左から書くが右から読むのである
これは伝統的に写像fを

f：Y　←　X

と書いてきたことと関連する

このときのXは定義域でありYは値域である
昔は右から書いて右から読んだのだそうだ
つまり数学書は左から書いてあるが右から読まなければならない

150 ：１３２人目の素数さん：2020/03/31(火) 18:53:45 ID:+LMTnMxG.net

前に何処かに書いたかも知れないが
この右から書くというのが改められたのが1960年頃であり
数学史的にはごく最近の出来事である
詳しくは

成田正雄『初等代数学』共立出版　1966

を読まれたい

151 ：１３２人目の素数さん：2020/04/01(水) 00:07:59 ID:vf0RBxx6.net

同じことだが書き直してみた

■写像

f：Y　←　X　

すべてのx∈Xに対して　あるy∈Yが唯一つ　f(x)=y　をみたすように存在する

翻訳

あるy∈Yが　f(x)=y　をみたすように　唯一つ存在し　それがfによって　すべてのx∈Xに対応すると書ける

例

Y:={1,2,3}

f(x):=x

とする．このとき

f(x_1)=1
f(x_2)=2
f(x_3)=3

となるすべてのx_1,x_2,x_3∈Xを書ける(全射)．

また

f(x_1)=1
f(x_2)=1
f(x_3)=2

などでもよい(全射でない)．


■全射

すべてのy∈Yに対して　あるx∈Xが　f(x)=y　をみたすように存在する

翻訳

あるx∈Xが　f(x)=y　をみたすように存在し　それがfによって　すべてのy∈Yの値として書ける

例

X：={1,2,3}
f(x):=x

とする．このとき

f(1)=1
f(2)=2
f(3)=3

である(とくに全単射)．これより値域は

Y:={1,2,3}

であることがわかる．

152 ：１３２人目の素数さん：2020/04/01(水) 00:09:25 ID:vf0RBxx6.net

現代に合わせれば写像は

f：X　→　Y

と書いた方が望ましいだろう

153 ：１３２人目の素数さん：2020/04/01(水) 00:11:30 ID:vf0RBxx6.net

>>151
＞となるすべてのx_1,x_2,x_3∈Xを書ける(全射)

訂正　全単射

154 ：１３２人目の素数さん：2020/04/01(水) 00:17:37 ID:vf0RBxx6.net

訂正
写像の翻訳
あるy∈Yが　y=f(x)　をみたすように　唯一つ存在し　それがfによって　すべてのx∈Xに対応すると書ける

全射の翻訳
あるx∈Xが　y=f(x)　をみたすように存在し　それがfによって　すべてのy∈Yの値として書ける

155 ：１３２人目の素数さん：2020/04/01(水) 08:39:27 ID:ibjGMPr7.net

写像f:X→Yとはf={(x,y)∈X×Y | 2つの条件}のことだぞ
それ以上でも以下でもない

156 ：１３２人目の素数さん：2020/04/01(水) 09:20:16 ID:vf0RBxx6.net

＞写像の定義はそれ以上でも以下でもない

これじゃあ話になりませんな
まあ少しでも議論できたらよいなと思って書き込んだのだが
意味がなかったようだ
俺はこれで立ち去るわ
じゃあな

157 ：１３２人目の素数さん：2020/04/27(月) 22:26:43.51 ID:GTbCbwO5e

ゲーデルの不完全性定理って分かったと思って次の日に何だったっけと思う。
人間はあの定理その物だからそうなのか？と思うが・・・
ところで竹内の基本予想って何なの？
多分ミレニアム問題に相当する予想だと予想してるんだが？

158 ：１３２人目の素数さん：2020/04/27(月) 23:21:21.37 ID:GTbCbwO5e

それとゲーデルが連続体濃度はアレフ２だと言っていたいきさつも
教えてくれる人はいないものか？

159 ：１３２人目の素数さん：2020/04/28(火) 00:45:31.89 ID:yvkQWcIlo

俺の勝手な推測だがアレフ２なら解析学の色々な基本問題が全部解決する
んじゃないかなんて想像してるのだが

160 ：１３２人目の素数さん：2020/04/29(水) 15:37:57.74 ID:HOklEGWA4

ペアノ算術系が矛盾してると疑っている人もいるって照井先生の本に書いてあったけど
そうなら数学をやっても意味が無いって事でフェルマーの予想ＡＢＣ予想もやるだけ無駄
ってことだよね。整数論はペアノ算術を使いまくってるからね。

161 ：１３２人目の素数さん：2020/05/08(金) 23:03:28.02 ID:sL0sKauOY

【副業】動画編集初めて一週間でいくら稼いだのか！？
https://www.youtube.com/watch?v=9eLbGKmzIok
月5万円稼ぐ動画編集の仕事とは？旅先での営業の方法は？裏ワザってある？
https://www.youtube.com/watch?v=NHsrdMPtJ3Q
動画編集で月５万円稼ぐ！初心者のための５つの方法
https://www.youtube.com/watch?v=HQxdKS5ougQ
【コラボ】初心者から動画編集で月30万円稼ぐ方法を聞いてきた！
https://www.youtube.com/watch?v=6PxG5h6-4Hw
動画編集は意外と儲かる件。高校生でも○○万円
https://www.youtube.com/watch?v=GsOPKVkex58
【体験談】動画編集のディレクターという職業
https://www.youtube.com/watch?v=PLshf0PJyNo

162 ：１３２人目の素数さん：2020/05/11(月) 21:42:44 ID:FABjWISR.net

ここの人たちはこのスレで議論されている逆接、「しかし」、「であっても」を論理学として扱うというのはどう思う？

数学記号を考案・改良するスレ
https://rio2016.5ch.net/test/read.cgi/math/1582284855/l50

163 ：１３２人目の素数さん：2020/05/13(水) 10:31:13 ID:amMseTLl.net

神戸大学で数理論理学を専攻して博士を取りたい場合、学部から神戸大学に行くのがいいですか？
それとも学部は京大など旧帝や東京工業大に行ったほうがいいですか？
お勧め大学があれば教えてください。

164 ：１３２人目の素数さん：2020/05/13(水) 10:53:07 ID:EIyANIud.net

あくまで個人的な意見ですが、
東大や京大に行くとレベルが高い人がいて気圧されることもありますね
(数理論理学では就職先が研究者くらいしかないでしょうし、そういう意味では神戸大学の方が心が折れにくいでしょう)

そんな性格でなければ、例えば東大には新井敏康先生とかいらっしゃいますし、感情抜きでは東大京大の方が研究職に就きやすいのではないでしょうか

165 ：１３２人目の素数さん：2020/05/13(水) 11:03:37 ID:YxiDM0Si.net

>>163
入れるところに行けば？

166 ：１３２人目の素数さん：2020/05/13(水) 11:08:06 ID:YxiDM0Si.net

>>164
周りがどうこういう以前に自分の意欲と努力の問題だけどね

よく「まだ本気だしてないだけ」っていう人いるけど
そもそも本気だせない時点で意欲が欠如してるわけで
そういう時は自分の内なる声に耳を傾けて
別の道に行ったほうがいいよね

167 ：１３２人目の素数さん：2020/05/14(木) 13:39:19 ID:laTGt7ex.net

数理論理も、数論幾何とか関数解析とか位相幾何みたいな
「ふつうの」数学の分野も、多分就職は
そう変わらないのであまりそう言うことは考えなくて良い。

2012年以降はこれまでは就職はそれなりに良かったけど
今後は企業の倒産とかが続いて就職先が減ってくる
可能性があるので、それは留意した方が良いけど

168 ：１３２人目の素数さん：2020/05/14(木) 17:11:27 ID:yUsAr7Ai.net

そもそも就職考えるんなら数学科に行かないほうがいいけどね

169 ：１３２人目の素数さん：2020/05/14(木) 19:16:10.94 ID:yMurV5iC.net

産業界からは世捨て人と呼ばれている。

170 ：１３２人目の素数さん：2020/05/24(日) 23:03:11 ID:OpZXQBtX.net

wikipediaの型理論のページに
「型理論の詳細はホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』にある。」
って書いてあるの古すぎじゃないですか？

外国ではHoTTとかやっているというのに

171 ：１３２人目の素数さん：2020/05/24(日) 23:11:42 ID:p1hbh81S.net

プリンキピアマテマティカ読んで数学を勉強してるやつなんて今どきいないっしょ

172 ：１３２人目の素数さん：2020/06/29(月) 22:13:56.24 ID:A6HnHqWU.net

いけねえ
知らぬとはいえ
俺はフェイトから知識を盗むところだった
だからあいつは強情だったんだな
謎の上から目線で人の話は聞かないという姿勢
それは情報を守るためだったんだな
よくわかったよ
今までありがとうな
またどこかで会おう

173 ：１３２人目の素数さん：2020/09/10(木) 21:25:33.88 ID:09TJq5ZY.net

背理法不要論は数学基礎論の範疇ですか

174 ：１３２人目の素数さん：2020/09/11(金) 10:15:35.74 ID:ymVLBOEu.net

背理法不要論という立場自体は、信念の問題で、いわゆる基礎論の範疇ではありません。
ですが、一般に背理法が成立しない証明体系はあり(直感主義論理の証明体系など)、その体系の数理論理学・証明論的な研究は範疇になりますね。
そういった研究は、もはや化石のようなものでしょう。

175 ：１３２人目の素数さん：2020/10/27(火) 02:07:09.31 ID:Qpi1JQGL.net

別に化石ではないと思うけど。
数学の中心的な潮流かとか言われたらアレだけど

176 ：１３２人目の素数さん：2020/11/07(土) 01:10:49.70 ID:5UHV1VuJ.net

幾何学的モデル理論のamazonレビュー、
なかなか的外れでアレだな

177 ：１３２人目の素数さん：2020/12/19(土) 12:58:49.73 ID:4hwmCOKs.net

kuso

178 ：１３２人目の素数さん：2020/12/19(土) 16:18:51.48 ID:4hwmCOKs.net

基礎論は数学ではありません

179 ：１３２人目の素数さん：2020/12/19(土) 16:28:07.89 ID:4hwmCOKs.net

基礎論をやる連中は閉鎖的です

180 ：１３２人目の素数さん：2020/12/19(土) 16:34:34.76 ID:4hwmCOKs.net

test

181 ：１３２人目の素数さん：2020/12/19(土) 21:19:51.76 ID:4hwmCOKs.net

二回の術語論理

182 ：１３２人目の素数さん：2020/12/20(日) 15:31:08.04 ID:pN5qV0wM.net

散会

183 ：１３２人目の素数さん：2020/12/21(月) 23:05:58.17 ID:slb93lrJ.net

Pを仮定して矛盾が出たら¬Pを結論するのは背理法じゃないんだよなあ
これはチョ環主義論理でも問題なく使える

184 ：１３２人目の素数さん：2020/12/21(月) 23:28:12.69 ID:eRMpoYlk.net

素朴集合論

185 ：１３２人目の素数さん：2020/12/22(火) 11:21:28.41 ID:l21dM6jc.net

点集合論

186 ：１３２人目の素数さん：2020/12/22(火) 17:26:41.73 ID:4zoIFivU.net

>>176
氏のレビューは鵜呑みはできない部分もあるね
カリフォルニア州立工芸大学(全米屈指のエリート校)の現数学科名誉教授の本を読み「あまり理解してる人ではなさそう」と評してる(当然、理解してないなどと思われるような部分はない)
ただ圏論についてなんかのレビューとかは参考になる部分も多い

187 ：１３２人目の素数さん：2020/12/22(火) 18:38:59.85 ID:SzaK3Ywi.net

>>186
評価に値するところなどどこにもない。本文を読んでいたらあんな出鱈目なレビューは書けない

188 ：１３２人目の素数さん：2020/12/22(火) 22:17:13.50 ID:RfMIjE2z.net

論理学やり始めたばかりなんですけど、真理表とタブローの木と自然演繹って何が違うんですか？同じことの別表現？

189 ：１３２人目の素数さん：2020/12/22(火) 22:58:56.96 ID:l21dM6jc.net

かわいそうに

190 ：１３２人目の素数さん：2020/12/22(火) 23:00:17.20 ID:l21dM6jc.net

ここ笑うとこ？
>カリフォルニア州立工芸大学(全米屈指のエリート校)

191 ：１３２人目の素数さん：2020/12/22(火) 23:07:46.62 ID:l21dM6jc.net

まさかcatechの間違い？

192 ：１３２人目の素数さん：2020/12/22(火) 23:08:50.83 ID:l21dM6jc.net

caltechだったｗ

193 ：１３２人目の素数さん：2020/12/22(火) 23:10:21.75 ID:8IPH7YoJ.net

カルテックのことか？

ゴメン、おれカリフォルニアなら
ＵＣバークレーしかしらんわｗ

194 ：１３２人目の素数さん：2020/12/22(火) 23:11:55.86 ID:8IPH7YoJ.net

>>188
＞真理表とタブローの木と自然演繹って何が違うんですか？

戸田山和久の「論理学をつくる」でも読んでみて　いい本だから　デカいけどｗ

195 ：１３２人目の素数さん：2020/12/22(火) 23:16:40.87 ID:l21dM6jc.net

科学哲学の冒険はいいね

196 ：１３２人目の素数さん：2020/12/22(火) 23:17:23.16 ID:l21dM6jc.net

論文の教室もいいぞ

197 ：１３２人目の素数さん：2020/12/22(火) 23:46:50.11 ID:l29QQJeL.net

>>194
真理値表は命題論理の論理式を真理値関数として表したもの
タブローの木は命題論理の論理式が真（または偽）であることの同値性を表したもの
自然演繹は仮定と結論の連鎖を表現したもの

198 ：１３２人目の素数さん：2020/12/23(水) 00:15:58.43 ID:QLH9bnSQ.net

>>194
読んでみるわ

>197
何となくわかったわ

199 ：１３２人目の素数さん：2020/12/23(水) 00:51:33.97 ID:+TUB+VXn.net

>>198
真理値表は{T,F}だけでなくN値やファジーや他の付値を付けることも可能
タブローの木は真偽だけ
自然演繹は推論規則や公理を調節可能

200 ：１３２人目の素数さん：2020/12/24(木) 23:49:41.55 ID:b5EOE98c.net

自然演繹やった。シークエント計算とかいうのもやった方がいいん？

201 ：１３２人目の素数さん：2020/12/24(木) 23:52:46.09 ID:b5EOE98c.net

あ、もうやってた

202 ：１３２人目の素数さん：2020/12/25(金) 00:37:46.41 ID:gtZA6OGh.net

>>200
本質的に同じ

203 ：１３２人目の素数さん：2021/01/05(火) 12:09:14.49 ID:lt2IPKYB.net

無限論理では
¬∀a1∃b1∀a2∃b3∀a3∃b3…P(a1,b1,a1,b2,…)
＝
∃a1∀b1∃a2∀b2∃a3∀b3…¬P(a1,b1,a1,b2,…)
てことにならないの？（変数はすべて集合Xの元）
これを普通の有限の論理式に書くコトってできないのかな

204 ：１３２人目の素数さん：2021/01/12(火) 02:55:33.16 ID:4JWb2sP4.net

論理を語るメタ論理を論じる地の文が精々プレーンな一階論理なのが笑えるところ

205 ：１３２人目の素数さん：2021/01/12(火) 20:30:14.11 ID:SZEETdnM.net

iZ-Cのサンプルプログラム書き始めたので見てね。
https://sunasunax.hatenablog.com

206 ：１３２人目の素数さん：2021/01/18(月) 22:40:42.19 ID:Xvy2vIAP.net

>>204
意味不明

207 ：１３２人目の素数さん：2021/01/19(火) 08:36:59.74 ID:OT1YzgW0.net

>>206
でもないが

208 ：１３２人目の素数さん：2021/01/19(火) 09:59:05.91 ID:7ty+V44F.net

>>207
じゃあ意味を教えて

「論理を語るメタ論理を論じる地の文が精々プレーンな一階論理なのが笑えるところ」
何が言いたいんだろう？

209 ：１３２人目の素数さん：2021/01/19(火) 12:09:49.65 ID:42ng3Osp.net

横からだけど意味わからないなら少し勉強が足りないと思う

210 ：１３２人目の素数さん：2021/02/02(火) 17:35:45.58 ID:h9fxRf+qM

萩原京平　平本蓮　煽り合い
https://www.youtube.com/watch?v=d0xqI98FV1A
平本蓮　入場　RIZIN26
https://www.youtube.com/watch?v=22dB9qf7T5A
お待たせしました、総合格闘家平本蓮です。【RIZIN.26】
https://www.youtube.com/watch?v=rOHjz40XdeM
1秒でも早く倒す。RIZIN.26は俺がジャックする。
https://www.youtube.com/watch?v=8hH6Nl33Fr0&t=464s
未来は僕等の手の中
https://www.youtube.com/watch?v=D-4rdpOttY8&t=291s
【密着】Preparation | 平本蓮 / Ren Hiramoto - RIZIN.26
https://www.youtube.com/watch?v=AvoHP646ouE&t=2468s
平本蓮の「譲れないもの」/ 質問コーナー
https://www.youtube.com/watch?v=_VEz9-MXiKI&t=16s
CHEHON 『Champion Road』MUSIC VIDEO
https://www.youtube.com/watch?v=oUZLNuynjHg

211 ：１３２人目の素数さん：2021/02/07(日) 00:55:50.47 ID:jQOhK4XwG

お前らの、いわば数学世界の「お遊戯」は
聞き飽きた。

頭脳の優越を誇るなら、その証左を
「論理的に示せ」。

すなわち、今日本における最大の問題
「コロナ感染の終息」についての対策を
具体的に政策立案せよ。

これが問題だ。お前ら解けるかな？
解けないなら、池沼ヒッキーと何ら変わらぬゴミども。　笑　(#^^#)

212 ：１３２人目の素数さん：2021/03/28(日) 03:27:22.77 ID:mKvp33II.net

丸善出版のスマリヤン三部作と>>133の本で迷ってるんだけどどっちが良書？

213 ：１３２人目の素数さん：2021/03/28(日) 08:35:31.73 ID:U1XBPI6N.net

いい加減さが許容できない人はスムリアンの本はやめた方がよい

214 ：１３２人目の素数さん：2021/04/01(木) 01:29:03.44 ID:sTOYz/XZ.net

前原本とかやめとけ
お前らほんと凡人が小綺麗にまとめた本好きだな
あんなの読んだら数学のセンス悪くなるって
何歳か知らないけど若いならスマリヤンみたいな天才が書いた本から吸収した方がいい

215 ：１３２人目の素数さん：2021/04/01(木) 05:27:50.28 ID:vOS6sd9e.net

すごい暴論だね

216 ：１３２人目の素数さん：2021/04/01(木) 06:48:20.45 ID:ucoTEeNO.net

すごくたくさんの内容が無理に
詰められた本って、「わざわざ一冊に纏めなくても」
という感じはどうしても出てきちゃうよね

新井「数学基礎論」とかJechとか
Schindlerとかそんな感じ

217 ：１３２人目の素数さん：2021/04/01(木) 15:25:44.66 ID:PGfVosn9.net

>>214
センスのある人の本ばかり読んでると高瀬正仁になってしまう

218 ：１３２人目の素数さん：2021/04/02(金) 22:38:23.21 ID:5xtBVH2m.net

丸善のスマリヤン不完全性定理（改訳版）は完全に頭おかしい

219 ：１３２人目の素数さん：2021/04/03(土) 01:35:45.11 ID:eWa+a5fS.net

高橋が戦犯？

220 ：１３２人目の素数さん：2021/04/03(土) 01:50:17.24 ID:+5+47BBd.net

その本、原著でよんだけどめっちゃよかった
昔の高橋訳がいけてなさすぎたけど改訳でもだめなのか

221 ：１３２人目の素数さん：2021/04/03(土) 01:53:57.23 ID:C9qOHU9B.net

スマリヤンは某一般向け書だけ読んだけど頭おかしいのは合ってるよ、とても面白い読み物だった

222 ：１３２人目の素数さん：2021/04/03(土) 01:57:00.01 ID:RQfig9CE.net

>>219
問題の解説がない
その上問題の難易度が高い
そりゃ独学で全問解けたら天才だと思うよ
到底人にすすめる本ではない

223 ：１３２人目の素数さん：2021/04/03(土) 02:18:31.47 ID:+5+47BBd.net

確かに解説ないのはおかしい難易度だよね
スマリヤン先生は代入なしの方法で簡単に算術化した方法を解説してんのに
演習問題では代入ありの煩雑なやり方を導かせるという
あり得ない投げっぷりだと思った記憶がある

224 ：１３２人目の素数さん：2021/05/08(土) 23:17:49.51 ID:r1Klbeuf.net

このスレで質問するのが適切かどうかわからないのですが。

射影幾何の公理に
　公理３ 任意の異なる２点に対し，これと結びつくただ１つの直線が存在する
　公理４ 任意の異なる２直線に対し，これと結びつくただ１つの点が存在する
があって、この二つは双対とのことですが、
この二つの双対関係はなにか深い理由がある必然的なことなのでしょうか、それとも
単なる偶然のことなのでしょうか？

ちなみに、双対というのも数理論理学の対象なのでしょうか？

225 ：１３２人目の素数さん：2021/05/09(日) 17:57:02.53 ID:zwxorq/q.net

>>224
数理論理学で射影幾何の双対の話が出るのは
数理論理学をドライブしていたのが形式主義であることを
強調するときが多いんじゃないかな。
意味抜きで公理だけが重要という意味で。
点や直線が未定義用語という意味で。

>この二つの双対関係はなにか深い理由がある必然的なことなのでしょうか
論理学的な観点「のみ」で話をするならば
射影幾何の公理系が「たまたま」その変換（点を直線と読み替えるetc)によって
不変であるという性質だからだと思います。

>ちなみに、双対というのも数理論理学の対象なのでしょうか？
数理論理学は、極論すれば論理式という記号列の代数的な操作なので
双対という概念はしょっちゅう出てきますが、それは数理論理学が
双対を扱うというよりも数理論理がそのような構造のもとで
展開されているからだと思います。

226 ：１３２人目の素数さん：2021/05/09(日) 19:52:46.46 ID:AKgWyr84.net

>>225
丁寧な回答ありがとうございます。

先の２つの公理の双対性はまあ偶然的と思ってもよいのですね。
なお、公理３と公理４は双対という以前に論理的に同値ですね。あとで気づきました。
双対と論理的同値とは微妙に関係しているのかな？

双対は数理論理の対象ではない（数理論理自体が双対的構造になっている）
ということですね。そのあたり数理論理と圏論なんかとは少し違うのですね。

227 ：１３２人目の素数さん：2021/05/09(日) 20:11:01.35 ID:YS3vxiDw.net

>>224
>ちなみに、双対というのも数理論理学の対象なのでしょうか？
射影幾何関係無しならandとorの双対性定理とかかな

228 ：１３２人目の素数さん：2021/05/09(日) 20:13:19.10 ID:YS3vxiDw.net

>>226
鵜呑みにせず理解深めるよう勉強したらいいよ

229 ：１３２人目の素数さん：2021/05/11(火) 15:24:29.33 ID:xW0NFNhy.net

＞公理３ 任意の異なる２点に対し，これと結びつくただ１つの直線が存在する
＞公理４ 任意の異なる２直線に対し，これと結びつくただ１つの点が存在する
＞なお、公理３と公理４は双対という以前に論理的に同値ですね。あとで気づきました。

趣旨とは違うので蛇足ですが論理的に同値ではないとおもいます
意味・モデルに引きずられてないでしょうか？
公理３は ∀xyPx⊃Py⊃∃!z Lz⊃Rxyz で
公理４は ∀xyLx⊃Ly⊃∃!z Pz⊃R*xyz ですよね
公理３と公理４を同値とするような論理的な導出はないと思います

230 ：１３２人目の素数さん：2021/05/12(水) 00:13:11.33 ID:jFoqblLO.net

リンゴとビールと椅子に置き換えて考えよう

231 ：１３２人目の素数さん：2021/05/12(水) 10:29:14.02 ID:fswPqcwM.net

微妙にまちがえてました。こうですね
公理３は ∀xyPx⊃Py⊃∃!z Lz∧Rxyz
公理４は ∀xyLx⊃Ly⊃∃!z Pz∧R*xyz

232 ：１３２人目の素数さん：2021/05/12(水) 12:08:33.22 ID:noCchEa2.net

随分一つの円にどれだけ180°が組まれてるかによるよな

233 ：１３２人目の素数さん：2021/05/12(水) 12:49:44.86 ID:jFoqblLO.net

細かいけど"全ての異なる"のニュアンスが抜けてね
∀xy:[(x/=y)(Px→Py)...]

三項関係R*は反射的推移閉包でいいのかな、双対性を初めから組み込んだ公理だね
(ところで三項だとどの組について言及しているのか曖昧じゃない？)

任意の異なる2林檎に対しただ一つの相性の良いビールが存在
任意の異なる2ビールに対しただ一つの相性の良いリンゴが存在

主語zを固定して
リンゴと合う(x, y)、ビールと合う(x,y)は推移的なのでリンゴとビールの相性の連鎖で複雑な幾何学ができる
x,yに対して反射的なので、王林と紅玉がクリアドライに合うなら紅玉と王林もそう、どっちから食べても問題ない

234 ：１３２人目の素数さん：2021/05/12(水) 12:55:11.13 ID:jFoqblLO.net

あ、"全ての異なる"を入れると同じリンゴ2つの食い合わせが保証されないのか
飽きるという意味論が自然に導かれた

235 ：１３２人目の素数さん：2021/05/12(水) 13:11:20.41 ID:8yGtQ7W5.net

これが形式主義のパワーだね

236 ：１３２人目の素数さん：2021/05/12(水) 13:17:36.68 ID:fswPqcwM.net

同一性の話はご指摘のとおり。R*は閉包ではなくてRとは別の三項関係ということ。修正すると
公理３は ∀xyPx⊃Py⊃x≠y⊃∃!z Lz∧Rxyz
公理４は ∀xyLx⊃Ly⊃x≠y⊃∃!z Pz∧Txyz
Px,Lx,Rxyz,Txyzを
M1： 「点である」「直線である」「線上に二点がある」「点は直線の交点である」
M2： 「直線である」「点である」「点は直線の交点である」「線上に二点がある」
と読む二つのモデルM1,M2において公理３と公理４は意味が互い違いになる。
そのような公理系だからこそ、双対性を持つ

237 ：１３２人目の素数さん：2021/05/12(水) 13:29:04.07 ID:jFoqblLO.net

>>236
M1とM2が置換(12)(34)で移るからRとTが双対になるのね、納得

*が付いてたからRは多分幾何学に必要そうな推移性と反射性を備えてるんだろうなと推測しました
実際これで必要十分なんでしょうかね？

238 ：１３２人目の素数さん：2021/05/12(水) 13:45:20.62 ID:jFoqblLO.net

基礎論はあんまり興味ないんだけど、数理論理スレってないのな
0階1階ファジーあたりはむしろ応用の方が熱いのでは
最も古典的かつ単純なbooleanSATだってよく後援付いてコンペやってるくらいだし
分けちゃダメかな？

239 ：１３２人目の素数さん：2021/05/12(水) 13:52:45.20 ID:jFoqblLO.net

同じ違和感抱いてる人居ないかと基礎でレス検索したら>>22で腑に落ちた

仮に日本語として基礎論=数理論理としても、スレの見る限り入り乱れてるので、言葉でなく内容で割るべきかと

240 ：１３２人目の素数さん：2021/05/12(水) 13:54:22.13 ID:v4bRloCn.net

>>229
> 公理３と公理４を同値とするような論理的な導出はないと思います

記号式でやると結構ごちゃごちゃするので論理的導出を日本語でやってみます。

(Ax3) あらゆる2点A,B上を通る直線は唯一に限る　（「異なる」は省略；以下同じ）
このAx3の否定を仮定する。すなわち、
(¬Ax3) ある2点A,B上を2つの直線L,Mが通る
とする。すると、
(*) ある2つの直線L,Mの上に2つの点A,Bがある
ことになる。これは、
(Ax4) あらゆる2直線L,Mの上には唯一の点がある
の否定である。

以上から、¬Ax3 -> ¬Ax4
同様にして、¬Ax4 -> ¬Ax3
結局、 Ax3 <-> Ax4

なお、お気づきと思いますが、
Ax3の否定（¬Ax3）のときに、
「どの2点についてもそれらを通る直線が無い、ということはない」
という前提をおいていますから、厳密には、公理３と公理４は「論理的に"ほぼ"同値」
と言っておくべきだったかもしれません。

以上どうでしょうか？

241 ：１３２人目の素数さん：2021/05/12(水) 16:35:31.76 ID:fswPqcwM.net

具体的な論証をするためにはAx3,Ax4以外の公理を共有しないと
議論できないと思います。ただ、一般的にAx3,Ax4をともに公理と呼ぶなら
それらは互いに独立（少なくとも独立と信じられている）のではないでしょうか？

その上であえて指摘させてもらいます

＞(*) ある2つの直線L,Mの上に2つの点A,Bがある
これを Line(L,A,B)かつLine(M,A,B) と書きましょう。そして
＞(Ax4) あらゆる2直線L,Mの上には唯一の点がある の否定
これを Cross(L,M,A)かつ Cross(L,M,B) と書きましょう
（アルファベットが異なるものは違うものという規約は維持します）
貴方はこの二つを同じとおっしゃっていますがそこを埋める
公理なり推論規則なりはあるのでしょうか？

直観的には明らかのような気もしますが
Line関係とCross関係を取り持つ公理なりがないと
なんともいえないかなあというきがします。

242 ：１３２人目の素数さん：2021/05/12(水) 17:00:31.23 ID:jFoqblLO.net

（同じようなことを(拙く)書いてたら適切なレスが来てた）

俺も>>237で指摘してもらったように、通る(>>226の表現では結び付く)の意味が不明瞭
記号を借りると、RとR*(後にT)をオーバーロードしてしまっている

243 ：１３２人目の素数さん：2021/05/12(水) 17:41:30.90 ID:jFoqblLO.net

記号を入れ替えただけの公理があるからこそ、その一方から従った定理と記号を入れ替えた双対定理が他方から自動的に従う

点である-線である （P-L）
cross-at - on-line(R-T)

あといくつか点と線の性質が公理1,2にあるはずで、これも必要
少なくとも>>233で述べたもの
cross-at(a,b,c)=cross(c,b,a) 反射性
…略

244 ：１３２人目の素数さん：2021/05/12(水) 17:50:32.99 ID:jFoqblLO.net

補足
公理3,4だけで不十分な理由

cross-at(a,b,c)=cross(c,b,a)
であるのに
on-line(A, B, C)/=on-line(C, B, A)
なら、双対定理は明らかに成り立たない

双対のある体系を指定したいなら、点と線は無定義語であってはならない
少なくともその性質は述語を介して間接的に(かつ整合的に)定義することが要請される

245 ：１３２人目の素数さん：2021/05/12(水) 17:54:57.35 ID:jFoqblLO.net

無定義語という言葉は違うニュアンスで使われたりするな、誤解を招きそう、ごめん
点と線自体はリンゴでもビールでもいい、しかし上述のような性質は定義する必要はある

246 ：１３２人目の素数さん：2021/05/12(水) 18:16:29.98 ID:fswPqcwM.net

定義とか未定義用語とか意味とかその辺りの言葉遣いやニュアンスが
数理論理の人と数学一般の人とでだいぶ違うきがする
気がするだけだけかもしれないけど

247 ：１３２人目の素数さん：2021/05/12(水) 22:23:10.14 ID:v4bRloCn.net

>>241
>具体的な論証をするためにはAx3,Ax4以外の公理を共有しないと
>議論できないと思います。

「どの2点についてもそれらを通る直線がある」
「どの2直線も少なくとも同じ1点を通る」
という2つの公理があればAx3とAx4は同値になると思います。
ただそうすると、公理の個数がむしろ1つ増えてしまいますｗ
こうして、公理の個数という観点では、元のAx3とAx4の2つの公理の設定が
最もシンプルだったというところに落ち着くのかもしれません。

>ただ、一般的にAx3,Ax4をともに公理と呼ぶなら
>それらは互いに独立（少なくとも独立と信じられている）のではないでしょうか？

一般に、公理群は必ずしも独立である必要はないでしょう。
ただ、上に述べたようにして、元のAx3とAx4の組が最もシンプルなのかもしれません。
それでも、Ax3とAx4の重複感あるいは非独立感がまだぬぐえないのですがｗ

> Line(L,A,B)かつLine(M,A,B) と〜〜
> Cross(L,M,A)かつ Cross(L,M,B)
> この二つを同じ〜〜を埋める公理なり推論規則なりはあるのでしょうか？

この二つが同じであるためには、他に何の公理も推論規則も必要としません。
Line(L,A,B) <-> on(A,L) and on(B,L)
Line(M,A,B) <-> on(A,M) and on(B,M)
Cross(L,M,A) <-> on(A,L) and on(A,M)
Cross(L,M,B) <-> on(B,L) and on(B,M)
でしょうから。