恒等コンビネータと α → α のヒルベルト流の証明
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/06/07 20:51 UTC 版)
「カリー＝ハワード同型対応」の記事における「恒等コンビネータと α → α のヒルベルト流の証明」の解説
簡単な例として α → α {\displaystyle \alpha \to \alpha } のヒルベルト流の証明を構成する。ラムダ計算では、これは恒等関数 I = λ x . x {\displaystyle I=\lambda x.x} の型であり、コンビネータ論理では恒等関数は S {\displaystyle S} と K {\displaystyle K} により I = S K K {\displaystyle I=SKK} （ただし慣例によって適用は左結合と見做す）と表現できる。以上の説明は α → α {\displaystyle \alpha \to \alpha } の証明の構成を与えている。実際、この論理式は次のようにしてヒルベルト流の証明体系にて証明可能である（慣例に従い含意記号は右結合と見做す）： 第二の公理図式から ( α → ( β → α ) → α ) → ( α → β → α ) → α → α {\displaystyle (\alpha \to (\beta \to \alpha )\to \alpha )\to (\alpha \to \beta \to \alpha )\to \alpha \to \alpha } を得る、 第一の公理図式から α → ( β → α ) → α {\displaystyle \alpha \to (\beta \to \alpha )\to \alpha } を得る、 第一の公理図式から α → β → α {\displaystyle \alpha \to \beta \to \alpha } を得る、 モーダス・ポネンスを2回適用して α → α {\displaystyle \alpha \to \alpha } を得る。
※この「恒等コンビネータと α → α のヒルベルト流の証明」の解説は、「カリー＝ハワード同型対応」の解説の一部です。
「恒等コンビネータと α → α のヒルベルト流の証明」を含む「カリー＝ハワード同型対応」の記事については、「カリー＝ハワード同型対応」の概要を参照ください。
- 恒等コンビネータと α → α のヒルベルト流の証明のページへのリンク
