Inter-universal geometry と ABC予想 (応援スレ) 60

608 名前：１３２人目の素数さん mailto:sage [2021/10/25(月) 00:09:34.16 ID:wB/2IR+g.net] >>547 つづき 単純階型理論（Simple Theory of Types） ここでは、Mendelson (1997, 289-293）の体系 ST を解説する。 基盤となる論理は一階述語論理であり、量化変数の範囲は型によって限定される。 最下層の型の個体要素は、ある集合論の原要素（Ur-elements）に対応する。それぞれの型にはより高位の型があり、ペアノの公理の後者関数（successor function）の記法にも似ている。ST では最高位の型があるかどうかは規定していない。超限数個の型があってもなんら不都合は生じない。 https://ja.wikipedia.org/wiki/%E9%AB%98%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86 高階述語論理（こうかいじゅつごろんり、英: Higher-order logic）は、一階述語論理と様々な意味で対比される用語である。 例えば、その違いは量化される変項の種類にも現われている。一階述語論理では、大まかに言えば述語に対する量化ができない。述語を量化できる論理体系については二階述語論理に詳しい。 その他の違いとして、基盤となる型理論で許されている型構築の違いがある。高階述語（higher-order predicate）とは、引数として1つ以上の別の述語をとることができる述語である。一般に n 階の高階述語の引数は1つ以上の (n - 1) 階の述語である（ここで n > 1）。同じことは高階関数（higher-order function）にも言える。 高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理の任意の標準モデルで真となる命題のみ、そしてそれらの全てを証明できるような（帰納的に公理化された）健全で完全な証明計算は存在しない。一方、モデルの範囲を（非標準的モデルを含む）ヘンキンモデルに拡大すれば、任意のモデルで真となる命題のみ、そしてそれらの全てを証明できるような、健全で完全な証明計算は存在する。 高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types や Calculus of Constructions (CoC) がある。 つづく

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef