曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。アマゾンアソシエイトやってまっせ。更新のお知らせはTwitter@cut_eliminationで

おすすめの記事

 当ブログは論理学を中心とした哲学・数学・計算機科学の勉強記録と、アニメの批評・感想を中心に書いております。おすすめの記事は以下です。

 

 

cut-elimination.hatenablog.com

 アニメにもジェンダーフェミニズムを考えるうえで示唆に富んだ作品はたくさんありますよ、という記事です。いろいろな作品を紹介しています。本当の目的はアニメ一般に対する「前時代的」という批判への反論です。私の調べが進むにつれてアップデートされていきます。

 

 

cut-elimination.hatenablog.com

 アニメーションおよびアニメの技術面や、アニメを見るという経験にフォーカスを当て、「アニメとは何か?」というテーマを哲学的に考えます。アニメが好きな方、哲学に興味がある方におすすめです。

 

 

cut-elimination.hatenablog.com

 藤井聡太先生の脳内には将棋盤がないという説を、様々なインタビューや棋士の証言をもとに検証しています。

 

 

cut-elimination.hatenablog.com

 マンガ『チェンソーマン』第43話に出てくるロシア語の歌を翻訳しています。元ネタはなんなのかもちょいと考察しています。

 

あとはカテゴリーから見てみてください。

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ弐拾弐「命題的な(?)等しさ(途中から)」(復習編)

 こちらの復習編。

同一性の除去公理

 わたくし的に気になったのは、プリンキピアでは性質に量化しているがITTではそれができないという点で、集合族を \Pi で束縛することもできるのに何故だろうと思った。しかしITTはどうも高階論理に対応するものではないので、なんかあるのだろう。

左射影規則の逆の証明

 この例はティピカルだと書いてある(34ページ)が、何がティピカルなのかわからなかった。ここの段落の議論は難しくてよくわからない。

性質と要素のインデックス付族

 具体的な導出がわからなかったのでまた次回。

 

ウォルトン『フィクションとは何か』読書会記録其ノ弐拾六・第10章1-3節(復習編)

 こちらの復習編。

ガリヴァーリリパット人も存在しないのなら、彼らについての命題も存在しない。それゆえ、ガリヴァーリリパット人に捕らえられたという命題も存在しないと思われる。(385ページ)

私の説だとこのような命題は存在するともいえるし存在しないともいえる、と思う。これはde reとde dictoとか絡んでくるかも。

 例えば

 

 セバスチャンはシエルの執事である。

 

という命題は存在するのか? ウォルトン説ではこれは何か別の命題の言い換えということになるが、私の考えではセバスチャンやシエルという存在者についての命題とも言えると思われる。作品を超えて作品の登場人物に言及できるか、という問題かもしれない。二次創作などでこの設定は改変できる、とか考えだすと固定指示子の議論に似てくる。

 あと予習編でりんごとハチミツを例にとったが、これらは種名辞なので微妙だったかも。

『竜とそばかすの姫』の感想(死ぬほどのネタバレ)

 すごく微妙だった! なんだろう、この気持ち。

話の話

 なんというか、すごく変な映画だった。細田さんてこんな感じだったけか。『未来のミライ』は金曜ロードショーで一度見ただけだったからあまり憶えていないのだけど、あれもそうだったかもしれない。とにかくものすごく散漫なのよ。話が。

 スズが歌えなくなった経緯がよくわからなかった。お母さんが亡くなったときとカラオケで歌わされそうになったときでは何年も離れているはずである。おそらく歌えなくなった原因はお母さんが亡くなったことにあるはずだが、そのときの描写がなかった(と思う)。なぜ高校生になってからのことが象徴的に出てきたのだろう? そもそもお母さんの死と歌がどのように結びついているのかがわからない。合唱サークルのババアたちが出てくる。スズはお母さんと一緒に参加していたようである。なんかそのあたりだろうか。すずはあのサークルが嫌になっているわけではないのでトラウマがあるわけでもなさそうだが。

 そして(!)歌えるようになったことがスズにとってどういう意味を持つのか? あとメガネの子のスペックとかあの子がいかにプロデュースしたのかとかも謎である。けっこうメガネの子とのやりとりもおもしろかったが、あまりなかったなあ。

 あとそもそもあの合唱のババアたちが必要だったのかという問題もある。電話をしたりクルマを飛ばしたりというどこのババアでもできる活躍しかしていない。そのキャラの薄さを埋めるためかババアのひとりが「オハイオで〜」という昔の恋話をしだす。オハイオとかいらんねん、と思った。

 サックスの子とカヌーの子の告白のくだりとかも、なんでこんなサイドの話にたっぷりとるんじゃ、となった。あとクラス内のLINEイジメみたいなやつもなんだったのだろう? あとババアとシノブくんはなぜスズがBelleだと気づいたのだろう? よくわからない。

 とにかくエピソードや描写のバランスが変なのである。けっこうポカンとしちゃう瞬間が多かった。「ワシはいま何を見せられているのだ?」みたいな。これは話とかキャラクター以外にもいろいろある。後述。

 テレビシリーズとかOVAシリーズのほうが良さそうなストーリー構想だと思う。でもやっぱりレイアウトの雄大さは映画向きだったり。

 というこの作りはもしかしたら意図的かもしれない。「小説を読んで補完してください」みたいな。ワシゃ読まんぞ!

ビジュアルと音楽

 最初にUチュートリアルみたいなシーケンスがあるが、ここがいちばん良かった。すごくワクワクした。クジラに乗ったBelleに。また最初の曲もとても良かった。millennium paradeだと思う。

 Uは3次元モデルを作っているのだろうが、それがあればよいというものではない。実写映画でロケーションのなかでどう撮るかというのと同じで、レイアウトが重要である。細田作品の最大の長所はああいう未来的な世界観のデザインとレイアウトのセンスだと思う(細田さんが直々に描いているわけではなかろうけど)。画面の半分くらいを、巨大構造物みたいなのの外から見た側面が占めていてあとは空、みたいなレイアウトがキービジュアルにもなっていたと思うが、あれは本当に美しい。CGで緻密に作っているのに書割みたいな雲が出ているのもオシャレである(誰の発案かは存ぜぬが)。

 で歌なのだが、中村佳穂さんは、こういう「歌が感動をもたらす」「歌で世界を救う」系の映画*1の歌い手史上最も上手いと思う。マジで。曲も良い。ただし、わたくし的にはクライマックスの歌より前半に出てきた二曲のほうが良かったのが残念だった。けどクライマックスの、画面やや右にスズが背を向けて浮んで粒みたいになったアバターと構造物が背景を埋めている、このレイアウトなんかも素晴しいと思う。

 キャラクターデザインはBelleに関してはすごく良かった。ディズニーの人がやっているらしく*2、けっこう『美女と野獣』のパロディ的である。

全体的に

 細田さんは『おおかみこどもの雨と雪』のようなファンタジー的で家族を描くのが最近の作風だが、『サマーウォーズ』みたいなインターネットを題材にしたSFもある。けどこれもまあ家族の話である。もっと純粋にインターネットの仮想空間の話だとさらに遡って「デジモン」の劇場版2『ぼくらのウォーゲーム』がある。

 これらはタイトルも話も似ているのだが、今回の『竜とそばかすの姫』もなんだかんだで似ている。大きく違うのは、現実のコンピュータやインターネットがどんどん進化しているという点であろう。この三作はそれぞれちょっとずつ近未来のサイバースペースを描いていると思う。私はこのたび初めてリアルタイムで実感しながら細田ワールドを観たことになる。

 『サマーウォーズ』の頃はまだトゥイッターがまだ全くと言っていいほど普及していなかったはずで、掲示板とかテレビが主要メディアだったはず。今作ではけっこう「つぶやき」スタイルの言葉の洪水みたいなイメージが重要である。しかしあのつぶやきに声を乗せるのはちょっと違和感があった。SNSのイメージを描こうとしているのだろうが、トゥイッターを見ていても声は聴えてこない。しかしこの違和感以上のもっと大きな違和感があって、これは「根源的な問題点」として後述。

 『ウォーゲーム』や『サマーウォーズ』ではサイバースペース上の悪事が現実世界にも悪影響を与えるのだが、今作ではそれがどうもなさそうだった。これはあとで気づいたのだけれどけっこう重要なポイントのように思う。そしてまたよくわからない点でもある。竜がやっていたことというのは実はオープンワールドのチート程度のことだったのではなかろうか。「チート程度」と書いたがプレイヤーたちからしたら大問題である。それであのヒロアカみたいな自治厨が暴走したのだろう。このあたりも後述するとして、じゃあケイくんはなんで竜なんてやっていたのだろう。それができたのだろう。またも謎である。

 最終的に虐待を扱うことにしたのは細田さんの発案だろうか。最後にリアルに対面するところなんかは『君の名は。』とか『天気の子』のラストみたいだった(私はこれけっこう好き)。これは川村元気さんの発案だろうか???

根源的な問題点

 結局のところUってなんなのだろうか? これがわからないのである。神経か何かを接続して感覚も仮想世界の中にいるように感じられている、ということでいいのだと思うが、その間リアルの身体はどうしているのだろう? 話に関して「何を見せられているのだ?」と書いたが、もっと根源的に「いま我々が見ているものは何なのだろう?」というのがわからないのである。登場人物が真に見ている光景なのか、それを抽象化したイメージなのか。というのは『サマーウォーズ』でもそうだったかもしれないが、あちらはたぶんちゃんとディスプレイ越しということになっていたと思う。キャラクターがサイバースペースにいるように描かれているのはそういうイメージかと。今敏監督の『パプリカ』の夢の世界とかもちゃんと分離されていたような。

 例えばunveilされたスズはどう見えているのだろう? CGのはずだが、それはunveilといえるのか? でもこれはさすがに「愚かな問い」かも。これが作品の質を損ねているとかではなさそうだ。

 私がこうした点で気になってしまうのはこんな感じでケンダル・ウォルトンの虚構論、特に描出体の議論に慣れてしまったからだろうか。また最近は「羅小黒戦記」で"衆生の門"なるVRゲームの話をやっていて、これがものすごく設定が緻密にできている。ログインとログアウトの仕組みを明確に作中で描いている。ログイン中に現実で空き巣(?)が入ったというのがゲーム内で警告されてたりとかおもしろい。このような徹底っぷりが本作にはなく、そこを観客に補完させているのが物足りなさに繋がった。

 羅小黒戦記についてついでに述べておくと、この作品はSNSとかネットゲームとかにどっぷりと漬かった人たちが作っているのがよくわかるのである。細田さんがSNSとかオープンワールドのゲームとか歌い手とかVTuberとかボカロとかMADとかいうものにそれほどハマっているような感じはしない。SNS上のつながりみたいなのに肯定的でも否定的でもなさそうではある。お母さんが亡くなったときのは不特定多数の声の恐ろしさみたいなのはあった。

www.bilibili.com

まとめ

 というわけで良い作品とも悪い作品とも言い難いのだが、良くも悪くもない作品というわけではなく、良いところはとことん良いので、こういう作品は大事である。ただ、数年に一度の細田守作品がそういう評価でいいのかな〜というのはある。

*1:20世紀少年ェ…

*2:「ディズニーの人」というなんか失礼な言い方しかできないほど私はディズニーをよく知らない。

ウォルトン『フィクションとは何か』読書会記録其ノ弐拾伍・第10章1-3節(予習編) 2.5次元と3次元の違い〜知りもしない『黒執事』を題材に〜

 シリーズの他の回はこちらから。

 

 第10章のタイトルは「架空の存在者をしりぞける」というもので、虚構的対象と言われるものを存在者として認めないとする立場を論じている。私としてはキャラクターの存在を擁護したいのでこの章の議論は倒すべき敵である😡

分析哲学の伝統的な議論

 ラッセルとマイノングの有名な存在すること(being)と実在すること(existence)を分ける議論などを取り上げてウォルトン先生は「こういった仕掛けは、ヴードゥー呪術的な形而上学に見える。こんなものは矛盾を隠蔽するために考案されたごまかしだという印象は避け難い」(380ページ)というやや差別的な表現で一蹴している。ロジックをやっている私は本来こういうのを擁護するべき立場かもしれないが、ぶっちゃけウォルトン先生に同意である。

 もうひとつ一蹴されているのが、それを指示の問題に還元するやり方である。虚構的対象が問題なのではなくそれを指示する行為や作用の分析である。これもなんだかややこしい議論になるだなのだ。

虚構的対象への疑いと抽象的存在者一般に対する疑いの違い

 虚構的対象が(現実にはいなさそうなのに指示したり真偽が問えたりするということを除いて)存在論的に特殊なのは、「サンタクロースは実在する」とかいうふうに、誰もが実在や存在について語るという点であるという(384ページ)。これは抽象的存在者一般にはない特徴で、例えば数や特性について実在するとかしないとかいうのは哲学者くらいのものである。

 ただし、数や特性がりんごやハチミツ*1と同じようなモノだとは一般人や子どもでも思うまい。あくまで、存在論的な問い(?)みたいなものをこれらに対してふつうは抱かない、ということである。

ふりをする

 ウォルトン先生が重視するのは「ふりをする」という行為である。ただしどうも前のほうで退けたサールの(言語行為論的な)偽装説とは違うらしい。サールの論では虚構というのは作者による「ふり」であったが、ウォルトンは読者のごっこ遊びに注目する。なお、このあたりは柏端達也『現代形而上学入門』のフィクションを扱った章で争点になっていた。柏端先生はサールを指示してウォルトンを批判している。これについてはそのうち論じたい。

 ウォルトン先生の基本的な方針はこうである。例文として本文にも登場する

 

 トム・ソーヤーは自分の葬式に出席した。

 

を考える。これを私が発話したとすると、これは『トム・ソーヤーの冒険』において真となる。重要なのはこれが現実世界のおいて真となるのではなく『トム・ソーヤーの冒険』の虚構世界において真となっていることである。この発話(断定)自体がごっこ遊びの一部を成している、というのがウォルトン説で、これはなかなかおもしろい。

 例文のような言明は「通常の言明」と呼ばれている。これは無茶な深読みなどせずとも自然と成り立つような言明である。『トム・ソーヤーの冒険』は、こうしたことを話す人が真なことを話しているということを、自分自身について虚構的に成り立つようにする、ということである(395ページ)。虚構的対象の存在やそれへの指示はここでは問題ではない。消去できる。重要なのはあくまでごっこ遊びと、それにおける例文のような断定するふりだからである。

私は何故これに反対なのか?

 実はここまでの議論は完全に正しいと私は思っている。しかしそれでも虚構的対象は存在すると思う。あんまり固まっていないので徒然なるままに書く。

 まず、今のところほとんど文学作品や伝説みたいなのしか扱われていない。描出体だとこの議論はどうなるだろう?

 また、例えばこれでユニコーンやトム・ソーヤーといった存在者はしりぞけられるが、例えば虚構においてりんごやハチミツといったごくふつうの存在者に言及することはある。これはどうだろう。これらは架空の存在者ではないので、今回のようにしてしりぞけられることはない。

 このシリーズで何度か書いたが、例えばアニメを見ているときにキャラクターがそこにいるように感じられる。ユニコーンタペストリーはユニコーンという存在者を描いたものといえるが、今回のような議論ではそうではないことになる。しかし私としては、キャラクターの絵は、特定のキャラクターという存在者を絵というメディアで表現したものだ、と言いたい。これを示す微妙な例がある。それは2.5次元と3次元の違いである。

 2.5次元も3次元の実写もどちらもあるような作品を探したところ、『黒執事』がヒットした。

↓こちらが原作マンガ

↓これが実写映画版。もうひとりの主人公の少年が何故か剛力彩芽さんになっている。原作とは違う人物らしい。こういうのは(よくない言い方だが)原作レイプなどと言われて叩かれたりする。

黒執事

黒執事

  • 水嶋 ヒロ
Amazon

↓これが2.5次元のミュージカルかな。「生執事」と呼ばれるらしい。

主人公は執事のセバスチャンである*2。実写映画では水嶋ヒロ氏が演じている。いろいろあったあとの久々の映画出演で話題になったのを憶えている。2.5次元(生執事)のほうは何度も公演していて再演もあって様々な人が演じているようだが、リンクのやつは古川雄大氏である。

 私が言いたいのはこういうことである。おそらくこれらを見る人は(私は見ていないのだが)、水嶋ヒロ氏はセバスチャンという人物*3であると思って見ているが、古川雄大氏はセバスチャンというキャラクターだと思って見ている。これは断定やふりといった言語行為では説明のつかない違いではないかと思う。まあ頑張れば説明できそうだが、私はセバスチャンをりんごやハチミツのようなものとして認めて、古川氏はそれそのもの、水嶋氏はそれと多くの性質を共有した別な何か、であるというごっこ遊びが成立していると考えたほうが自然であると思う。それくらいキャラクターというのは直観的に強力で印象的な何かなのである。

 なんかうまく書けなかった。

 

 どうでしょう? 10章後半へつづく。 

*1:

*2:執事のキャラクターは何故かセバスチャンという名前であることが多く、この由来は諸説あるようです。

*3:人物なのかどうかはアレですが…

ウォルトン『フィクションとは何か』読書会記録其ノ弐拾四・第9章(復習編)

 

 

 ぶっちゃけこの章のテーマはあまり関心がないというか、知識がなくて論じれない。拙者は学部時代はいちおう文学らしきものを専攻する学科だったけど、なんだかんだ文学理論をしっかりとは勉強せずにきてしまった。勉強したうえで読み返したいですな。作者の死とか人称とか語り手とか、そういうのとは違った視点でおもしろいだろう。

 『こころ』は第3部がまるまる手紙だったり、『カラマーゾフの兄弟』は語り手が事件の真相を知っている「全知」で「消されて」いる感じだったのに後半では表に出てきて裁判を傍聴しているとか、よさげな例を思いつくけどあんまり論じがいがないなと思ってた。

 

ウォルトン『フィクションとは何か』読書会記録其ノ弐拾参・第9章(予習編)

 過去の回はこちらから。

 フェミニズムと萌え絵批判の問題について考えていて、メイク・ビリーブを援用したい所存。あと佐々木敦先生の本をチラ見したら、(もちろん分析哲学に詳しくないのだろうが)メイク・ビリーブで解決してしまうことを延々と考えてるっぽくもあり。詳しく読んで考えてみたい所存。

 

 さあ本題だ!

 

 言語による表象作用は基本的には描出ではないということだった。ではどういうものか、というのがこの章である。いろいろと用語が出てくるのでまとめる。

用語

作者と語り手

 作者と語り手を区別せよというのはよく言われる。しかし「作者が語り手である」ということが虚構的に成立することはある。ただ、この場合の作者=語り手に関する虚構的真理が現実においても真理であるとは言えない。

仲立ち

 出来事は語り手を通じて間接的に示される。描出ではこのようなことはない。

語り手の二種類の信頼性

 信頼できない語り手というのはミステリーやポストモダン的な文学によく出てくる。本書の立場からすると信頼性には二種類がある。すなわち「語り手が人として信頼できることが虚構として成り立つ」という意味と「語り手が虚構において語ることは、それが虚構において本当である」という意味とである(353ページ)。

 これらの概念は似ているが、必ずしも一致しない。

全知の語り手、不在の語り手、消された語り手

 よく「神の視点」とかいう。語り手は何故そんなに登場人物の内面までわかるのか、とか言われるが、まあこういうのは「愚かな問い」ということで。

 語り手の存在感が希薄な作品がある。ウォルトンは語り手が「不在」ではなく「消されている」とするよう提案する(361ページ)。語り手がいなさそうな作品でもなんか匂わされることがあるので。

報告する語り手と物語を語る語り手

 今までのはだいたいが報告する語り手というものである(そうですよね?)。これは、語り手が作品世界のなかにいる。

 物語を語る語り手というのは、語り手が物語を語ったり作ったりしていることが虚構として成り立つ、そのような語り手のことである。

 物語を語る語り手が仲立ちをするのかどうかというのがいろいろ論じられている。しかしそれは置いといて、興味深いのは、物語を語る語り手についての虚構的真理は物語の中身についての虚構的真理に依存する、という指摘である(368-369ページ)。読者は中身の様子から作者がどういう人物かを推測するからである。ここで「作者」と言っているのは以下のことである。

内在する作者あるいは見かけ上の作者

 よく「作者の考えは〜」みたいなことをいうが、あれである。小説を読むときに漠然とイメージする作者のことである。これが物語を語る語り手とそこそこ一致する。

視点

 ジェラール・ジュネットは語り手(話している人物)と視点の人物(みている人物)を分けろという。これを論じた『物語のディスクール』は文学理論の聖典なので、ウォルトンのコメントを見ておく。

私が強く主張したいのは、次のことだけである。「語りのパースペクティヴを方向付ける視点を持った」唯一の登場人物、単一の登場人物といったものが(その作品のたった一つの文章においてでさえ)存在するはずだと思い込まないようにすること、そして、報告する語り手(話している人物)のパースペクティヴが、 多くの例で、少なくとも形の上では存在しているのを認めること、である。このパースペクティヴは、主要な視点が別の登場人物の視点である場合でさえ、形の上では存在するのである。(371ページ)(「」内は『物語のディスクール』からの引用)

メイク・ビリーブ説の柔軟さがよくわかる。

 

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ弐拾壱「有限集合」「無矛盾性」(予習編)

 直観主義型理論でごんす。

有限集合

規則

 これまでの規則はすべて、ある集合(あるいは集合族)からある集合を作るものだったが、ここで導入する有限集合は前提なしに直接に与えられるものである。n = 0, 1, 2, ... によって無限個のルールがあることに注意。

f:id:cut_elimination:20210709024844p:plain

{\mathbb N}_n形成則

 前提がない。

{\mathbb N}_n導入則

 {\mathbb N}_0には要素がない(これは図にも書いたように m \in \{x \mid 0 \leq x < n\} として n を変えていくとわかりやすいかも)。{\mathbb N}_1 はひとつのカノニカルな要素 0_1 を持ち、{\mathbb N}_2 はカノニカルな要素 0_2, 1_2 を持つ、などなど。

{\mathbb N}_n除去則

 C(z) \; set \; (z \in {\mathbb N}_n) はふつうに {\mathbb N}_n 上の性質として解釈できる。前提を知っていると仮定して、{\textsf R}_n を以下のように解釈する。

 まず、c を実行する。すると m_n \; (0 \leq m \leq n - 1) となる。対応する C(m_n) の要素 c_m を選んでさらに実行する。m_nc と等しいということだったので前提の c_m \in C(m_n) と合せて d \in C(c) となる。

 {\textsf R}_n は有限集合 {\mathbb N}_n) 上の再帰(recursion)である。場合わけによる定義のようなものである。n 個の規則がある。

{\mathbb N}_n等号則

 01 の規則のみを作っておいて、{\mathbb N}_2 \equiv {\mathbb N}_1 + {\mathbb N}_1, {\mathbb N}_3 \equiv {\mathbb N}_1 + {\mathbb N}_2 などなどと定義して他の規則を導出することもできる。

例:{\mathbb N}_0

 {\mathbb N}_0には要素がないので、導入則がない。なので

 \bot \equiv \emptyset \equiv {\mathbb N}_0

とするのは自然である。

{\mathbb N}_0除去則

 要素 c \in {\mathbb N}_0 はありえないので、{\textsf R}_0(c) を実行することはできない。{\textsf R}_0(c) という形のプログラムの命令の集合は空になる。これはダイクストラによって導入されたアボート(中断)という文と似ている。

\bot除去則

 C(z)z に依存していないとき、前提と帰結の証明(構成)を隠して \bot 除去則を得る。矛盾からはなんでも出てくるというやつである。もうひとつの形の正当化もかいておいた。

例:{\mathbb N}_1

 \top \equiv {\mathbb N}_1

と定義する。{\mathbb N}_1 導入則によって 0_1 \in {\mathbb N}_1 を得るので 0_1{\mathbb N}_1 の要素であり、\top は true である。

 0_1{\mathbb N}_1 の唯一の要素であることは(たぶんカノニカルとかを無視して)図を参照。

例:{\mathbb N}_2

 Boolean \equiv {\mathbb N}_2

と定義する。これはプログラミングにおける真理値 \textsf{true, false} で構成される。\textsf{true} \equiv 0_2, \textsf{false} \equiv 1_2 と定義しよう。すると \textsf{if} c \textsf{then} c_0 \textsf{else} c_1 \equiv \textsf{R}_2(c, c_0, c_1) と定義できる。c\textsf{true} というのは c を実行すると 0_2 になるということで、{\mathbb N}_2 等号則によって \textsf{R}_2(c, c_0, c_1)c_0 と同じ値を持つ。そうでなければ、c を実行すると 1_2 になり、\textsf{R}_2(c, c_0, c_1)c_1 と同じ値を持つ。

 何故こんなに上手くいくのだろう?

 {\mathbb N}_2 の要素が 0_21_2 であることは証明できるが、命題の形となる。図を参照。

例:否定

 ~A \equiv \lnot A \equiv -A \equiv A \to {\mathbb N}_0

とすると、いちばん右のに含意の導入と除去がそのまま使えるので、それがそのまま否定の規則になる。ここで Cons \equiv \lnot Der('\bot') \equiv Der('\bot') \supset \bot 

無矛盾性

 規則の体系の無矛盾性について。

 無矛盾性は二つの方法で理解できる。

(1)数学的無矛盾性

 理論 T の無矛盾性を証明するには、別の理論 T' を考える。この T' はもとの理論 T の命題のコードと述語 Der を持つ。Der('A') はコードが 'A' の命題 AT で導出可能であるということを表す。ここで Cons \equiv \lnot Der('\bot') \equiv Der('\bot') \supset \bot と定義して、ConsT' で true であることを(頑張って)証明する。この方法は、ヒルベルトがやったように、公理や推論規則の意味論的正当化を諦めるならできる。直観主義型理論でもやろうと思えばできるのだが、我々は構文論と同じくらい意味論も重視しているので、ここではそれをとらない。以下の単純な無矛盾性を考える。

 第2不完全性定理がらみの難しい話ですな。

(2)単純な無矛盾性

 単純に \bot が証明できないこと、あるいは \bot \; true という判断ができないということである。上の Cons と違って数学的な命題ではない(よくわからないが)。こちらの無矛盾性は以下のように示す。

 c \in \bot とすると、c は実行したらカノニカルな要素 d \in \bot となる。しかし \bot空集合なのでカノニカルな要素を持たない。\bot \; true が証明されるとしたら直観主義型理論の規則の何かが間違っていることになるが、(ザックリしているけど)そんなものはない。\bot を導出する規則などないので。よって \bot \; true の証明はない。

 少なくとも T' の単純な無矛盾性を仮定すれば、もとの T の数学的無矛盾性からその単純な無矛盾性を出せる。:ある c について c \in Cons が証明できたとする。T が単純な無矛盾ではないとするとT における \bot \; true の証明、すなわちある a について a \in {\mathbb N}_0 の証明がある。コーディングによって ['a' \in Der('\bot')] が与えられる。c \in Cons とこれに \supset 除去則を適用して \textsf{Ap}(c, 'a') \in \bot を得る。すなわち \bot \; trueT' で導出可能である。よって \bot \; trueT' で証明可能でない、すなわち T' が単純な無矛盾であると仮定するとメタな意味で矛盾し、下線部が否定される。