再帰的可算な理論と初等再帰的な理論が一致するというCraigの絡繰 (Craig's trick) とその算術的階層への一般化を紹介する。以下では言語に指数関数に対する関数記号が含まれていると仮定する。
集合X⊆NνがΓ-定義可能 (Γ-definable) であるとは、あるφ∈Γ が存在しX={x→∈Nν∣N⊨φ(x→)}となることである。関数fがΓ-定義可能であるのはそのグラフがΓ-定義可能であることとし、理論TがΓ-定義可能であるのはTに含まれる論理式のコード全体{⌜φ⌝∣φ∈T}がΓ-定義可能であることとする。
任意のΣn+10-定義可能な理論Tに対し、あるΠn0-定義可能な理論Sが存在し、任意の論理式φに対しT⊢φ⟺S⊢φとなる。
まず再帰理論の基本的結果、空でない集合XがΣn+10-定義可能であることとXはあるΠn0-定義可能関数の値域となることが同値になることに気をつける。今、理論Tが空だとするど自明に成立つので空でないとし、Πn0-定義可能な関数fでrng(f)={⌜φ⌝∣φ∈T}となるようなものを取る。また論理式φに対してφnをφ0:=⊤,φn+1:=φn∧φと定めて、理論SをS:={φn+1∣f(n)=⌜φ⌝}とする。Sの定義からT⊢φ⟺S⊢φとなることは明らか。またnと⌜φ⌝から⌜φn⌝を返す関数、すなわちg(n,⌜φ⌝)=⌜φn⌝を満たす関数gは初等再帰的であることからx∈{⌜φ⌝∣φ∈S}は(∃y<x)[x=g(y+1,f(y))]と同値であり、Πn0-定義可能である。
任意の再帰的可算な理論Tに対し、ある初等再帰的な理論Sが存在し、任意の論理式φに対しT⊢φ⟺S⊢φとなる。
再帰的可算であることとΣ10-定義可能であることの同値性と初等再帰的であることとΠ00-定義可能であることの同値性による。後者の同値性は関数記号として指数関数を含んでいることによる。
バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。