文脈付き構成的意味論を構成的意味論に変換する
ここでは, 自然数の集合 に0を含めることとする。
記法 は を表す。 の時は を表す。
記法 は を表す。 の時は (真理値の真)を表す。
式
- .
これは, 次のようなことを含意している:
- が項数 の関手であり, が式であるとき, は式である。
- 特に, が項数 の関手であるとき, は式である。
- が式であるとき, ある自然数 , ある項数 の関手 , ある式 が存在し, .
文脈付き構成的意味論
文脈付き構成的意味論 は形式言語 , 文脈集合 , 値集合 , 解釈 からなる組である。
このとき のもとの式の意味 を, つぎの帰納的定義によって定める。
文脈 のもとの式 の値は になる。
文脈付き構成的意味論を構成的意味論に変換する
文脈付き構成的意味論 から自明な構成的意味論 を構成できる。