>>207
(引用開始)
素朴な疑問なんですけど、今時命題を証明するとき、
間接的な証明ではなく直接的に証拠を構成することで証明された
と見なす立場を取る論理で考える
ブラウアーのような直観主義論理の論法
で証明する人っているんですか？
(引用終り)

アホな解説>>208 しかできないやつがいるな （＾＾；
20世紀前半で詰んだ人よ

直観主義論理は、圏論で復権した！（下記）
これは 21世紀の常識だから 覚えておきましょう！　（＾＾；

(google検索)
直観主義論理 と 圏論の 関係
＜AI による概要＞
直観主義論理と圏論は、デカルト閉圏（Cartesian Closed Category: CCC）を基盤とする強い関係性（Curry-Howard-Lambek対応）にあります。直観主義的論理式は圏の対象、証明は射とみなされ、論理の構造（含意、論理積など）は圏の閉構造や積で自然に解釈されます。
主な関係のポイント
・カリー・ハワード・ランベック対応: 直観主義論理の証明、型理論の型（ラムダ計算）、圏論の射の三者が対応し、論理的な推論を数学的に厳密な「圏」の構造として記述できます。
・デカルト閉圏（CCC）: 構造（特に射の集合が対象自体となる内部ホム）により、直観主義論理の「含意」(\(A\rightarrow B\)) を自然に表現します。
・ハイティング代数（Heyting Algebra）: 直観主義命題論理の代数モデルであり、部分対象圏がその構造を持つ場合、その論理は直観主義的になります。
・応用: この対応はプログラミング言語の型理論、および証明支援系における証明の構造化に利用されています。
直観主義論理の「排中律（\(A\lor \neg A\)）を持たない」という特徴は、圏論的意味論においては、全ての構造がブール代数（古典論理）ではなく、より一般的なハイティング代数やトポスという構造で捉えられることに相当します。

https://www.kurims.kyoto-u.ac.jp/~terui/summer2013.pdf
直観主義論理への招待 - RIMS, Kyoto University
数学基礎論サマースクール2013 講義資料
照井一成（京都大学）
1 はじめに
直観主義論理 (intuitionistic logic) とは、オランダの数学者ブラウワー (1881-1966) が提唱した直観主義数学に由来する論理であり、直観主義数学で認められる推論の様式を弟子. のハイティング (1898-1980) が形式化したものである。 数学基礎論上の立場としての直観主義は、廃れて久しい。それはブラウワー個人の特異.
36 ページ