直観主義，背理法と否定の導入

Tomoki UDA @t_uda

私もそれは推論規則だと思っていた。あと否定の導入でも分かるけど、私は RAA って呼んでたな… これ、マイナーな呼び方…？ [区間ぜろ]

品格の塊 @noukoknows

ロジックTL

品格の塊 @noukoknows

鏡さんに褒められたのでいい気になって文章公開したらえらい騒ぎになってヒヤヒヤしたけどマスハラはされずに済んでいるような感じなのですごいほっとしてる

keno @keno1728

要するに, 一貫性があって聞かれたときにちゃんと説明できればどっちでもいいってことですね. > 公理or推論規則

ジャバ仙人 @plus7

ヒルベルト流ってなに，フェンシングの流派？

黒ごまのかき氷 @hymathlogic

ヒルベルト流だと⇒記号を含んだ公理がたくさん出てくるからフェンシングしても強うそう（謎

平泉 @hrizm_math

ヒルベルト流は竹刀だけどゲンツェン流は金属バット

平泉 @hrizm_math

どちらも本気で人を殴れば死ぬという意味で同値

平泉 @hrizm_math

NK(肉食う)　NJ(肉じゃなくて魚を食う)

平泉 @hrizm_math

LK(ルックルックこんにちは)

品格の塊 @noukoknows

JK？

mod_poppo @mod_poppo

"論理学も公理図式もLKもJKも" JKという論理学用語がある可能性

平泉 @hrizm_math

「ありえない演算子」と「マジで？演算子」が追加された形式論理の体系JK

V-alg-d（ZZ） @alg_d

形式的証明というのは、大体こういう定義になっている。 (1)公理を定義する。 (2)推論規則を定義する。 (3)公理は証明可能である。 (4)証明可能なものから推論規則で得られるものは証明可能である。

V-alg-d（ZZ） @alg_d

つまり、形式的証明に《証明する力》を付けるには「公理を増やす」か「推論規則を増やす」かすればよい。

V-alg-d（ZZ） @alg_d

当然形式的証明には、普段我々が使っているような数学が出来る程度には《証明する力》が欲しいから、ある程度《証明する力》を付けなければならない。それを付けるのに公理を増やしたのがHilbert、推論規則を増やしたのがGentzen。

V-alg-d（ZZ） @alg_d

とまあこんな感じだと思う。

V-alg-d（ZZ） @alg_d

Gentzen流(LK) http://t.co/2o4X6oUD 　 Hilbert流 http://t.co/KQlZfmp1

ytb @ytb_at_twt

「直観主義，背理法と否定の導入」のまとめを読んだ。面白かったんですが、直観主義論理と数学的直観主義（実無限の否定）を一直線に考えるのは誤解のもとだと思います。というのも、例えば、直観主義論理上で包括原理を仮定すればラッセルのパラドックスが矛盾を導きます。

ytb @ytb_at_twt

数学的直観主義者は、もちろん包括原理は非可述的なので認めない訳です。つまり、直観主義論理と数学的直観主義は切り離して考えることができ、直観主義論理上でどんなときも実無限が考えられない訳じゃない（直観主義論理上の公理的集合論では実無限をある程度扱うことが出来るはず）と思います。

H. Miyoshi (ALC Japan is rescheduled in 2025) @metaphusika

@ytb_at_twt 直観主義数学の定義ってそれほど明確じゃないと思うのでちょっと誤解を招きそうです。言いたい立場がどれかはわかりますが。

Hiroyasu Kamo @kamo_hiroyasu

@metaphusika @ytb_at_twt 直観主義論理＝LJと同値な論理およびその拡張。直観主義数学＝直観主義論理をベース論理とし、「万物は構成的である」を意味する公理を持つ理論。数学的直観主義＝構成的な対象のみ実在を認める哲学的立場。と使い分けていますが、いかがでしょう