19/03/15 07:30:34.60 wvBN32BE.net
>>192
>アイデアの飛翔をうながす(可能性を持つ)数学的直観」とよばれるもので
数学的直観とは、人の高階論理能力を使った、加速定理の実現かもしれないね（＾＾
URLﾘﾝｸ(ja.wikipedia.org)
高階述語論理
高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理は（帰納的に公理化された）健全で完全な証明計算が認められないとされた。しかし、Henkin model によれば、健全で完全な証明計算は存在する。
高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types や Calculus of Constructions (CoC) がある。
(>>182もご参照)
URLﾘﾝｸ(www.amazon.co.jp)
圏論による論理学―高階論理とトポス 単行本 ? 2007/12/1 清水 義夫 (著) 出版社: 東京大学出版会
著者略歴 (「BOOK著者紹介情報」より)
清水/義夫
1939年東京に生まれる。1963年東京大学文学部哲学科卒業。1967年東京大学大学院人文科学研究科博士課程退学。現在、千葉工業大学情報科学部教授(本データはこの書籍が刊行された当時に掲載されていたものです)
URLﾘﾝｸ(ja.wikipedia.org)
加速定理
形式的体系に関する加速定理
理論 {\displaystyle T} T とその拡大理論 {\displaystyle S} S について「 {\displaystyle T} T において証明可能な論理式で {\displaystyle S} S においてはより簡単に証明できるものが存在する」という形の定理は、計算複雑性に関する加速定理の類比として、同じく加速定理と呼ばれる。その代表的なものとしてはゲーデルの加速定理がある。
つづく