>>192
>アイデアの飛翔をうながす(可能性を持つ)数学的直観」とよばれるもので

数学的直観とは、人の高階論理能力を使った、加速定理の実現かもしれないね(^^
https://ja.wikipedia.org/wiki/%E9%AB%98%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86
高階述語論理

高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理は(帰納的に公理化された)健全で完全な証明計算が認められないとされた。しかし、Henkin model によれば、健全で完全な証明計算は存在する。

高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types や Calculus of Constructions (CoC) がある。

(>>182もご参照)
https://www.amazon.co.jp/dp/4130120573
圏論による論理学―高階論理とトポス 単行本 ? 2007/12/1 清水 義夫 (著) 出版社: 東京大学出版会

著者略歴 (「BOOK著者紹介情報」より)
清水/義夫
1939年東京に生まれる。1963年東京大学文学部哲学科卒業。1967年東京大学大学院人文科学研究科博士課程退学。現在、千葉工業大学情報科学部教授(本データはこの書籍が刊行された当時に掲載されていたものです)

https://ja.wikipedia.org/wiki/%E5%8A%A0%E9%80%9F%E5%AE%9A%E7%90%86
加速定理

形式的体系に関する加速定理
理論 {\displaystyle T} T とその拡大理論 {\displaystyle S} S について「 {\displaystyle T} T において証明可能な論理式で {\displaystyle S} S においてはより簡単に証明できるものが存在する」という形の定理は、計算複雑性に関する加速定理の類比として、同じく加速定理と呼ばれる。その代表的なものとしてはゲーデルの加速定理がある。

つづく