白と黒のとびら 第16章 返答

ガレット君はついに塔の問いかけに答えます

• 「〇と●からなる全ての文字列を含む集合から、『塔の動作を記述した文字列のうち、それ自体が、自身が表す動作によって表現される言語の"文"であるような文字列』を取り除いた文字列」
  • 塔の動作を表す文字列ではないもの(つまり文法エラーに相当する)も含まれるわけですね
• 証明は背理法による
  • この言語(Lとする。またここでいう言語は〇と●からなる文字列の集合を意味する)が塔によって表現できるとする
    • この言語を表現するように塔の動作を記述する文字列が存在するはず。これを S とする
    • S が L の文である(S が L に含まれる)と仮定する
      • L の定義より、S は「Sが表現する言語の文ではない」とことなるが、これは S が L の文であることと矛盾する
    • S が L の文でないと仮定する
      • L の定義より S は L の文であることになり、矛盾する
  • よって L が塔によって表現可能という前提が誤り

さて、物語はクライマックスを迎えますが、それは読んでのお楽しみとします。
エピローグは主にストーリー展開なので飛ばして、次回は「解説」の章を読んで本書を終えようと思います。
次は、ついに TAPL の邦訳「型システム入門」を読もうと思います。これは長くかかりそうです。