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

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

おすすめの記事

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

 

cut-elimination.hatenablog.com

 

cut-elimination.hatenablog.com

 

cut-elimination.hatenablog.com

 

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

『チェンソーマン』のロシア語の歌(?)の訳と考察

  『チェンソーマン』は全巻読んだのだけれど感想を書いていなかった。それはまた別の機会に。今回のテーマは同作の第43話で出てくるロシア語の歌である。実は私はロシア語がちょっとできるので、これを訳してこの歌がなんなのか考えます。

 私は『チェンソーマン』のキャラでレゼがいちばん好きです。エピソードとしてもいちばん好きです。

 

 以下ネタバレもあるので注意。

 

「ジェーンは教会で眠った」

 第43話のサブタイトルは「ジェーンは教会で眠った」となっている。この話の前後はレゼというキャラクターが出てきて主人公デンジを翻弄するというエピソードが続いている。

 実はレゼはソ連で育てられたスパイで、デンジの心臓を狙っていた。しかしレゼのデンジへの想いは本当にすべて嘘だったのか…みたいな切ないやつである。

 というわけなのでレゼの母語はロシア語なのだろう。

 この回では、ただのかわいい子かと思われたレゼが、何者かに襲われた際に超人的な戦闘力を見せ、あきらかに只者ではないと判明する。その戦闘シーンで突如ロシア語の歌をくちずさむのである。

 なお、先ほどから「歌」と書いているが、歌なのかどうかも判然としない。しかし吹き出しに「♪」マークが付いているので歌っているっぽい。また後述のとおり、これが歌だとして既存の歌なのかどうかはわかっていない。

 以下の訳を見ていただければわかるとおり、歌詞のなかで「ジェーン」という女性の名前が出てきて、教会で眠るというくだりもある。なのでこのサブタイトルは歌のタイトルなんじゃないかと推測される。しかしただの推測である。

※環境によってはキリル文字(ロシア語の文字)がうまく表示されないようです。全角になってしまいます。しかし『チェンソーマン』も写植(?)がうまくいっていないのかキリル文字が全角になってしまっているのでまあまあまあ。

私訳

 День моего свидания с Джейн

 僕とジェーンのデートの日

 

 Все готово

 準備は万端

 

 Утром мы пойдем вместе в церковть

 朝、一緒に教会へ行こう

 

 Мы будем пить кофе и есть омлеты в кафе

 カフェでコーヒーを飲んでオムレツを食べよう

 

 После того как мы прогуляемся в парке

 公園をちょっと散歩したら

 

 Мы пойдем в аквариум и увиде※ любимых Джейн, дельфинов и пингвинов

 水族館へ行ってジェーンの好きなイルカとペンギンを見よう

 

 После обеда мы отдохнем

 ディナーの後はひと休みしよう

 

 Итак, что мы сделали утром

 それで、僕らは今朝なにをしたっけ

 

 Мы будем говорить об этом пока не вспомним

 思い出すまで語り合うけど

 

 Мы не вспомним

 僕らは思い出せないだろう

 

 И ночью мы будем спать в церкви

 そして僕らは教会で眠るだろう

 

 ※印をつけた"увиде"は調べてもロシア語にはない語で、おそらく"увидем"の誤植であろうかと。なのでそのように訳した。

  「朝、一緒に教会へ行こう」からは全て未来時制になっている。なのですべては「僕」の願望かもしれない。またロシア語には未来形にも完了体と不完了体の区別があって、それらが混ざった文章になっている。これらの使い分けはけっこう難しい。完了体は一回きりの動作で不完了体は継続性があったり反復される動作に使うというのが基本である。「教会へ行こう」のところは完了体で、一人称複数の完了体未来は勧誘のニュアンスがあるように思う。しかし全体的にこの歌は計画なのか願望なのかジェーンへの誘いなのか判然としない。これらが渾然一体とした感じもする。もしくは機械翻訳にかけたためにそのあたりのニュアンスが不徹底なのか…(出典については後述)。そういったことを判定できるほどのロシア語の知識は私にはない。例えば日本語→ロシア語の機械翻訳の精度もよく知らない。しかし「行く」「ちょっと散歩する」「見る」「ひと休みする」「思い出す」が完了体で「飲む」「食べる」「語り合う」「眠る」が不完了体というのはうまく使い分けられている感じである。

既訳があります

 以下のようにTwitterでも訳を載せている方がいる。正確には投稿者のご友人が訳者である。私の上の訳もこれをちょっと参考にさせていただいた。

mobile.twitter.com

しかし、解釈の相違点もいくつかある。

 "любимых Джейн, "というのを「最愛なるジェーン」と訳しているが、"любимых"は複数生格という形をしていて呼びかけに適した形ではないように思える。ジェーンに呼びかけるなら"любимая Джейн, "となるべきではないかと。これはあとのイルカとペンギンが同じ形なのでそこに掛かっていて、ジェーンは「愛する」というのの主体になっていると私は考えた。しかしДжейнという非ロシア的な名前は格変化をしないので解釈が難しい。また" , "が付いているのはちょっと不自然かもしれず、「愛しのジェーン」と呼びかけているという解釈も捨てきれないかも*1

 続いて「思い出せない」もしくは「思い出さない」の解釈について。この方は"обед"を「昼食」と訳しているのだが、ロシアでは日本と一日の食事の感覚が違っていて、どちらかというと夕食と考えるべきではないかと思う。"обед"は日本の昼食よりは遅い時間で、一日のメインの食事である。なので「思い出せない」のはこれが一日の終りだからで、それくらい一日が楽しくて充実していたということなのだと思う。しかしこの方の「わざと思い出さずいつまでも語り合っていたい」というこの方の解釈はなかなか鋭いなと感心してしまった。

出典はどこか?

 この歌、何か出典があるのだろうか? これが調べてもよくわからない。ジェーンというのは普通は英語圏の名前なので、英語の歌か何かが元なのかもしれない。しかし名前だけでは根拠が薄い。

 先のツイートで「元はイギリスの小説家による恋愛小説」とある。これは以下のツイートから広まった説だと思う。

mobile.twitter.com

私はこのハーレクイン小説を読んでいないのだが、あらすじを見てみてもどうも「ジェーン」という名前以外の共通点はなさそうである。水族館や教会といったモチーフもなさそうで。というか『二人のティータイム』のヒロインの名前は正確には「メリー・ジェーン」だった。この小説と結びつけるのはどうもこの方の早とちりではないかなと。

 先のツイートでは拙いロシア語か上級のロシア語かという問題にも触れられていたが、文法的には関係代名詞や仮定法や副動詞(というのがロシア語文法にはあるのです)が出てこないのでかなり簡単である。でも歌詞ってそんなもんかも。それ以上に、韻やスラングや主語の省略なんかがないことでネイティブっぽいロシア語に感じられない感じ感である。もとはロシア語ではないんじゃないかと私は思う。ロシア語だとしても子供向けの何かか。

 などといろいろ考えたのだが、私の説はふつうにタツキ先生が考えたオリジナルの詞だというものである。そもそもなぜ「元ネタがある」と思ったのかというと、これがロシア語だからである。出典もなくロシア語の詞を作れるはずがない、と。しかし別にロシアの文献かなんかに出典がなくとも日本語で考えて翻訳をする手段はいくらでもある。マンガの作中に英語が出てくる際と事情はそれほどかわらない。そしてジェーンという名前はロシアっぽくないのだから、この時点で「ロシア語だから元ネタがあるに違いない」と考える根拠は薄れる。ロシア語っぽくないのだから。翻訳ソフトも使えるし、ロシア語に詳しいアドバイザーがいるのかもしれないし、そもそもタツキ先生ご自身がロシア語を知っている可能性だってある。

 もうひとつ「元ネタがある」と思った根拠があって、それはこの詞があまりにもオシャレで『チェンソーマン』の作風から浮いているということである。どうも私のなかに「『チェンソーマン』の作者にこんなオシャレな詞が書けるはずがないしロシア語がわかるはずがない」という偏見があったようで、反省している。タツキ先生、ごめんなさい。

 作中でトーリカというキャラクターも出てくるが、私ははじめこれもロシア語由来の名前かと思った。ロシア語の"только"というのは英語の"only"にあたる語で、「唯一無二」みたいな意味もまああるだろうけど、もっと「ただわずかにそれだけ」みたいな否定的なニュアンスが強い語かなと。しかしトーリカはドイツ人のサンタクロースの弟子なのでロシア人ではない、かと思いきやサンタクロースのピクシブ百科を見るとロシア(ソ連)人という説もあるらしい。

dic.pixiv.net

この説が妥当かどうかは疑わしいが(私と同じく名前から判断しているので)、少なくともトーリカの出身はドイツとは限らないようだ。そもそも「サンタクロース」というのもドイツ語ではないので、そのへんはけっこう曖昧である。

 この"только"なのだが、文字通りカナを当てると「トルコ」になると思う。しかしロシア語の発音では「トーリカ」が近い。ロシア語を学んだことのある方ならば「トルコ」よりも「トーリカ」のほうが自然に感じると思う。トーリカの名前の由来が"только"なのだとしたら、やはりタツキ先生がある程度ロシア語ができるか、あるいは背後にロシア語のブレーンがいるかしていると思う。

結論

 本作はアニメ化が決定している。このエピソードまでやるかどうかは今のところわからないが、これが歌として映像化されることで何か新たな情報が出てくるかもしれない。それまで結論は待ちましょうや。

 

 

「ジェーンは教会で眠った」は↓この巻に収録されています。

 

 読んでませんが…

*1:ただ「最愛」までいくかな? という感じまします。

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ参「判断の形式の解釈」「命題」(予習編)

 Per Martin-Löf, "Intuitionistic Type Theory", 1984の「判断の形式の解釈」「命題」の章を読んで訳したり考えたりしています。

判断の形式の解釈(Explanations of the forms of judgements)

canonical、equality、computation

解釈とは

 解釈と訳したのは explanation であって interpretation ではない。だからなんだって話かもしれないが。

 解釈は以下の問いのどれかに答えることで与えられる。

  • 集合とは何か?- 存在論的(古代ギリシア
  • 何かが集合であると判断するには何を知っていなければならないか?- 認識論的(デカルト、カントなど)
  • A は集合である」という形式の判断は何を意味するか?-意味論的(モダン)

しかし本質的には同じ問いである。

カノニカルな要素

At first sight,  we could assume that a set is defined by prescribing how its elements are formed.

 

まず、集合はその要素がいかに形成されるかを規定することで定義される、と仮定してみよう。

"prescribe"は「処方する」という意味もある。この例として自然数集合 {\mathbb N} の定義があげられる。

f:id:cut_elimination:20210421071958j:plain

この規則によって要素が構成される(constructed)。

 しかし、例えば 10^{10} なんかは明らかに {\mathbb N} の要素だがなんらかの a \in {\mathbb N} について a' という形はしていない。

We thus have to distinguish the elements which have a form by we can directly see that they are the result of one of the rules, and call them canonical, from all other elements, which we will call noncanonical.

 

なので、ある規則が適用された結果だと見てすぐにわかる形式の要素をカノニカルといい、他の要素を非カノニカルということにして区別せねばならない。

10^{10}{\mathbb N} の非カノニカルな要素である。ここから話は二つの非カノニカルな要素の同等性(equality)の定義に向う。この段階ではやや唐突である。すぐに、まずはカノニカルな要素の同等性を形成を規定しましょう、となる。いずれは10^{10}100000000005000000000 + 5000000000 が等しいことも判断できるようにしなければならない。

判断の解釈

(1) a set A is defined by prescribing how a canonical element of A is formed as well as how two equal canonical elements of A are formed.

 

(1) 集合 A は、A のカノニカルな要素がいかに形成されるか、および A の二つの等しい要素がいかに形成されるかを規定することで定義される。

これが「A は集合である」という形式の判断の意味の解釈であるという。ちょっと思ったのだが、これは a \in A という形式の判断とは違うのか。おそらく、ここでは「集合の(カノニカルな)要素の与え方」が与えられているだけで「集合の(カノニカルな)要素」が与えられているわけではない。あとで形式体系が導入されるが、「A set」という形式の判断は形成則(formation rule)で与えられ、カノニカルな要素は導入則(introduction rule)で与えられる。ここでの議論から考えると形成則は導入則の前提になるような集合(の判断)に適用されるべきであるが(導入則すなわち要素の与え方、が与えられているということなので)、実際そのようになっている。

 しかしなぜ同等性(equality)もあらかじめ定義しておくのだろうか? 一階論理は等式の公理(推論規則)も含むのも普通なので別に変ではないか…。

 というわけで同等性(等しさ)の形成(forming)を規定する(prescribe)。先程の {\mathbb N} の規則には以下を加えればよい。

f:id:cut_elimination:20210421112639j:plain

他にも A \times B の例が出ている。

f:id:cut_elimination:20210422112855j:plain

f:id:cut_elimination:20210422145407j:plain

 カノニカルな要素の間の同等性の定義を規定するのに反射的で対称的で推移的ならば特に制限はないとある。けっこう緩い。あとでITTは形式体系ではないということも書く。

 続いて集合の同等性の定義である。

(2) two sets A and B are equal if

f:id:cut_elimination:20210422113231j:plain

and

f:id:cut_elimination:20210422113335j:plain

for arbitrary canonical elements a, b.

これが A = B という判断の意味である。外延の等しさではなく、カノニカルな要素の形成の仕方の等しさということか。

 続いて集合の要素について。

(3) an element a of a set A is a method (or program) which, when executed, yields a canonical element of A as result.

 

(3) 集合 A の要素 a は、実行の結果として A のカノニカルな要素が得られるメソッド(プログラム)である。

これは「a \in A」という形式の判断の意味。計算の規則が書いてある。ここはけっこうちゃんと決まっている。集合 A の要素 a の計算過程で得られる b について、b の最も外側の形が A のカノニカルな要素であるならば、その b を値として停止する。これは正規順序(normal order)とか遅延評価(lazy evaluation)とか書いてある。例として (2 + 2) \in {\mathbb N} から (2 + 1)' というカノニカルな要素が得られるというのが挙げられている。これはこの式のなかの 2 を実行すると 1' になるがそれを最初にはやらないということだろう。ただし 2 + 1{\mathbb N} のカノニカルな要素だという判断にも計算が必要なのではないかと思うがどうか。それはさておきこれはラムダ計算の簡約の順番に関する戦略で正規順序簡約といわれるやつらしく、プログラミング言語ではHaskellで採用されている遅延評価に当たるものなのであろう。調べます。

 続いて要素の等しさ。

(4) two arbitrary elements a, b of a set A are equal if, when executed, a and b yield equal canonical elements of A as results.

 

(4) 集合 A の二つの任意の要素 a, b が等しいのは、ab の実行の結果として A の等しいカノニカルな要素が得られるときである。

これは「a = b \in A」という形式の判断の意味。この定義の「集合 A の等しいカノニカルな要素」というのは(1)ですでに与えられているのでよい感じである、とある。

 さて、カノニカルは正規(normal)と考えてよいのだろうか? そうすると計算を実行してカノニカルな要素を得るというのが証明の正規化に対応することになっていい感じなのであるが。しかし (2 + 1)' は素直に見るとまだ計算が終っている感じがしない(0'''' という形じゃないと)。

 例として e, f \in A \times B というのが挙げられている。ef はそれぞれ A \times B のなんらかのカノニカルな要素 (a, b), (c, d) を得るメソッドである。 e = f \in A \times B であるのは (a, b) = (c, d) \in A \times B という計算結果として得られるカノニカルな要素の等しさによる。そしてこれは先ほどの A \times B の要素の等しさの定義より、a = c \in A かつ b = d \in B である場合に成り立つ。

命題(Propositions)

命題、証明、集合としての命題

命題の定義

 古典的には命題とは真理値でしかない、とある。しかしそれだと無限のドメイン上の量化を含む命題を正当化するのが困難になるとあり、やはり無限の量化の問題が出てくる。量化を含む命題の真偽は、そこにドメインの要素(の名前)を代入した命題の真偽をチェックすることで決まるが全称量化された文ならば真のとき、存在量化ならば偽のとき、すべての要素を代入してチェックしなければならない。これは確かに困難である。

 というわけなので直観主義では以下のように考える。

a proposition is defined by laying down what counts as a proof of the proposition,

a proposition is true if it has a proof, that is, if a proof of it can be given.

 

命題は、その命題の証明とみなされるものを定めることで定義される、

命題が真であるのは、それが証明を持っているとき、つまり、その証明が与えられうるときである。(これはプラヴィッツの"Intuitionistic logic: a philosophical challenge"という論文の引用)

命題の定義と真理の定義はけっこう別問題だと思うのだが、証明を真理と置き換えることで命題を真理値ではなく証明可能性で定義するということではあろう。

proofとderivationと不完全性定理

 しかし次がわからない。

Thus, intuitionistically, truth is identified with provability, though of course not (because of Gödel's incompleteness theorem) with derivability within any particular formal system.

 

よって、直観主義の考え方では、真理は証明可能性と同一である。ただしもちろん(ゲーデル不完全性定理があるので)なんらかの特定の形式体系内の導出可能性と同一ではない。 

まず、provabilityとderivabilityの違いってなんだろうか。調べてみると、驚くべきことに、私と同じようにこのITT84を読んで同じところで疑問に思っている人がいた。以下のQ&Aサイトで「derivabilityとprovabilityの違いとは?」という質問がある。

logic - What is the difference between derivability and provability? - Mathematics Stack Exchange

回答によると、proofは通常の数学で使うインフォーマルな概念でderivationは形式体系で定義される形式的なやつである、とのこと。これは"Basic Proof Theory"でも同じ方針だったのでけっこう一般的なことかもしれない。ITTはどうも言語が明確に定義されるものではないようで、命題のproofの形式定義もない。

 では、これがゲーデル不完全性定理とどう関係するのか? 第一不完全性定理は真理と証明可能性のズレを示唆するので、それを言っているのかもしれない。しかし「真だが証明できない命題」と言ったときの「真」は証明体系と別で与えられることであって、証明体系内では意味を持たないと考えてもよい、はず。なので証明から真理を定義するなら証明できない命題は真ではないとしてしまえばよいのではないかと。ロッサーの不完全性定理の「証明も反証もできない」は真理値を決められないが、直観主義論理では安全なのではないかと。このあたりは数学的にも哲学的にも難しそうである。不完全性定理ってわかるようでわからない。

 しかしもっと怪しいのは、ITTが形式体系ではないとしても形式化はできるのではないかということである。だからこそプログラミング言語の基礎理論となっているのでは。となるとITTも(算術を扱うならば)不完全性定理からは逃れられない。以下のQ&Aは難しいけれどそういうことを言っているっぽい(proofとderivationの違いも先ほどのと同様)。

lo.logic - How do we construct the Gödel’s sentence in Martin-Löf type theory? - MathOverflow

 まだまだ勉強が必要である。

論理演算子の意味の解釈、すなわち証明の解釈

 論理結合子の意味の解釈はこれまでの流れのとおり、それを含んだ証明の解釈によって与えられる。

f:id:cut_elimination:20210422113149j:plain

というのがいわゆるBHK解釈のだいたい一般的なバージョンであるが、これをもうちょっと明確にすると以下のようになる。

f:id:cut_elimination:20210422113156j:plain

ただしこれらはすべてカノニカルな形の証明で、本当はカノニカルな証明を得るメソッドはすべて証明される命題の要素となる、と注意がある。

 私からの補足。A \supset B(\forall x)B(x) の違いであるが、前者の BA の要素と無関係であるのに対して後者の B(x) は量化のドメインの要素に依存して決まる。命題を型とみなしたとき、これが依存型になる。

The Formulae-as-Types Interpretation

 If we take seriously the idea that a proposition is defined by laying down how its canonical proofs are formed (as in the second table above) and accept that a set is defined by prescribing how its canonical elements are formed, then it is clear that it would only lead to unnecessary duplication to keep the notions of proposition and set (and the associated notions of proof of a proposition and element of a set) apart. Instead, we simply identify them, that is, treat them as one and the same notion. This is the formulae-as-types (propositions-as-sets) interpretation on which intuitionistic type theory is based.

 

 命題をそのカノニカルな証明の形成法(上の二つ目の表のように)を定めることで定義されるというアイデアを真面目に受け止め、かつ集合はそのカノニカルな要素の形成法を規定することで定義されるということも受け入れるならば、命題と集合という概念(およびそれらと関連する命題の証明と集合の要素という概念)を分けておくのは不要な繰り返しにしかなりそうにない、ということは明らかとなる。そうではなく、単純に同一視する、すなわちそれらを同じひとつの概念として扱おう。これが「型としての論理式(集合としての命題)」という解釈で、直観主義型理論のベースとなっている。

 形成法が似ているという観察から同一視していいのかという疑問があるのだが、そもそも論理式と型は導出体系のなかでまったく同じ振る舞いをするという前提がある。この対応は形に関するものだが、命題と集合というもっと概念(notion)的な、内部構造的な部分でも同じであるというのがマーティン=レーフ先生の主張なのだろう。

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

ウォルトン『フィクションとは何か』読書会記録其ノ壱・序章(予習編) - 曇りなき眼で見定めブログの復習編です。たいしたことはないです。

 

 表象体(representations)という漠然とした言葉を使うのは、あえてそうすることで確定した用法を持たせないためである。これがなかなか良いと予習編で書いた。その話に続けてさらに

 表象体というカテゴリーをどう形づくるべきか、またそう決定する理由は何か、といったことは、理論が展開されるにつれて徐々に明らかになるだろう。実際、理論を組み立ててものごとの理解に達するということは、その大部分が、ものごとをどう分類すれば最善なのかを決定し、どの類似性と相違性を認知し強調すべきかを決定する、ということなのである。それゆえ、探究範囲の確定は、その大部分が探究の結果として得られる。最初に挙げた作品例を越えて、いったい私たちの理論が何についての理論なのかを分かろうとしても、理論そのものを手中にするまでは無理なのだ。(4ページ)

 とある。これを最初に明言してしまうのもなかなかおもしろい。数学の本だとなかなかこうはならない。

 

 "make-believe"という語について訳注で「『ごっこ遊びにおけるように、事実でないと分かってはいるが進んで受け入れることにする』という心的態度」と書かれている。しかしごっこ遊びにおいては「事実でない」ということを意識してはいないはずである。なので難しい。

 

 言語分析によるアプローチについても。予習編で書き忘れていたが「ごっこ遊びを私が強調するのは、部分的には、この言語アプローチが過剰になっているのに対抗するためである」(5ページ)と述べられているのは重要である。分析哲学は基本的に言語の分析であるが、本書はその限界を超えうるのである。ただし著者は言語アプローチの重要性も同時に認めている。これらは相補的なのである。ここから予習編でも書いた「二種類の問い」に繋がる。

 

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ弍「緒言」「命題と判断」(復習編)

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ壱「緒言」「命題と判断」(予習編) - 曇りなき眼で見定めブログ これの復習編です。

f:id:cut_elimination:20210417212903j:plain

緒言

It is free from the deficiency of Russell's ramified theory of types, as regards the possibility of developing elementary parts of mathematics, like the theory of real numbers, because of the presence of operation which allows us to form the cartesian product of any given family of sets, in particular, the set of all functions from one set to another.

 

これ(可述的な直観主義の型の理論)は、実数の理論のような数学の初等的な部分を展開しうるという点で、ラッセルの分岐的な型の理論の欠点を逃れている。何故なら、任意の与えられた集合族からデカルト積を作る操作が存在するからである。具体的には、あるひとつの集合から他の集合への関数すべての集合である(ITT84, 1ページ)

この"in particular"以下はITTにおける"operation"の具体例を述べているのだと私は解釈したが、そのまま読むとちょっと微妙な書き方なので、もうちょっと読み進めてから再検討ということに。このあたりはいきなりかなりの予備知識を要求していて大変で、有限のドメイン上の量化ならいいが無限になると微妙になるというのもよくわからない。これは直観主義のすごく重要なポイントのような気がする。ビショップの構成的数学あたりもちゃんと勉強しなければ。可述的かつ還元公理なしでかなりの程度の数学が実行できるというのがITTの利点のはずで、となると実数の議論は避けて通れない!

命題と判断

判断の形式

...the premisses and conclusion of a logical inference are judgements.

 

…論理的推論の前提と帰結は判断である。

 これが重要そうである。つまりITTは判断から判断を導いていく体系なのである。

The distinction between propositions and judgements was clear from Frege to Principia. These notions have later been replaced by the formalistic notions of formula and theorem (in a formal system), respectively. Contrary to formulas, propositions are not defined inductively. So to speak, they form an open concept.

 

命題と判断の区別はフレーゲから『プリンキピア』までは明確である。のちにこれらはそれぞれ(形式体系における)形式的な論理式と定理に置き換わった。論理式と違って命題は帰納的に定義されない。言うなれば、命題は開かれた概念を形成する。

この"open concept"がよくわからなかったのだが、帰納的ではないということなので、 帰納的定義に使われる「これのみが〇〇である」というのがないということか、となった。また、論理式には well-formed というのがあるが命題にはない、とか。フレーゲの『概念記法』では命題は内容だから、とか。そんな感じである。

 その後の議論も予習編では書いていなかったが重要だった。ロジックの教科書ではふつう構文論と証明論と意味論を定義して解釈を与えていくが、ITTでは形式と意味の区別がないという。マーティン=レーフ先生によればこれは通常の数学実践に近い。ロジック以外の分野の数学者は形式と意味を分けて考えたりしないからだろう。また、この発想は証明論的意味論に繋がっていくと思われる。

When one treats logic as any other branch of mathematics, as in the metamathematical tradition originated by Hilbert, such judgements and inferences are only partially and formally represented in so-called object language, while they are implicitly used, as in any other branch of mathematics, in the so-calld metalanguage.

 

ロジックを他の数学の分野と同じように扱うとき、すなわちヒルベルト以来のメタ数学のようにするとき、こうした判断や推論は単に部分的かつ形式的にいわゆる対象言語内で表現されるだけであるが、いわゆるメタ言語内では、他の数学の分野においてと同じように、暗黙のうちにしか使われない。

ここはなかなか英語が読みにくかった! 勉強会内で私が言った解釈も間違っていたと思う。つまり、ヒルベルト以来のメタ数学では判断や推論を扱っているが、対象言語内の扱いは不十分だし、メタ言語では依然として明示されない、という点が不満なのである。これを体系内で明示するのがITTなのだ。

 \vdash記号の歴史的な意味とかを考えるとおもしろそうだな〜となった。 フレーゲの体系ではこの左には何も書かない、と思う。推件計算やITTでは左に書く。

...before a rule of inference can be justified, it must be explained what it is that we must know in order to have the right to make a judgement of any one of the various forms that the premisses and conclusion can have.

 

…推論の規則を正当化する前に、なんらかの形をした前提と結論の判断をすることが許されるためには何を知っていなければならないか、説明が必要だ。(3ページ、2段落目)

ここは私は予習でスルーしていたが重要なところだった。先述のとおり前提と結論は判断である。このくだりのあとで判断の4つの形式が導入されるが、それによって前提から結論を出す推論規則の前にそもそも前提と結論はどのような形をしていなければならないかがわかるのである。A = B という判断をするにはその前に A setB set という判断がなければならない、という注意も付け加わる。こういうのはITT84では上に()に入れて明示されるし、現代的な記法では\vdashの左に書かれるはず。

BHK解釈

 コルモゴロフがロジックをやっていた時代にはプログラミングなんてなかったよね。またコルモゴロフの直観主義論理の論文はあくまで論理結合子の解釈であって、命題を集合と解釈するという話は出てこない。それはCHIである。

 ハイティング算術と選択公理とCHIの関係は初耳であった。選択公理も逃げずにちゃんと向き合わないと。

 最後に、冒頭の画像を再掲する。

f:id:cut_elimination:20210417212903j:plain

これがITTの要であると思う。拡散希望ヒルベルトのメタ数学と違って、オブジェクトとしての命題の証明とメタ的な判断の証明とが体系ないで見事に同居している。

【今更ながら】(押井守ファンによる)『花束みたいな恋をした』の感想(徒然なるままに)

 けっこう胸が締めつけられるというかなんというか、最後すっきりした感じで終ってよかったですよ。

 あと相変らず清原果耶さんがいい感じの役で出てくる。

 私は麦くんが言っていたような"責任"を負いたくないので人との関わりを最小限にしているのだなあ。それでも共感する。

 絹ちゃんと麦くんと二人の人生の方向性がズレていくのだけど、それもタイミングとかそういうののせいであって何か決定的な経験があるわけではない。そういうのってあるよね。映画全体としてどちらか一方の人生を貶めるわけでもなく、そういう感じもとても良かったと思う。またそれとなく描かれるけど絹ちゃんは東京出身で親が一流企業に勤めているのに対して麦くんは地方出身でそれほど上流家庭ではなさそうで、こういうのも影響しているのでしょうな。

 私は東京から引越して札幌でこの映画を観たが、東京に住んだことのない人に井の頭線沿線のこの感じとか伝わるのかな〜と思った。しかしおそらく主人公らと同世代で同じ時代に大学生だった私にはめちゃくちゃわかってしまうこの感じ。「粋な夜電波」とか聴いてんじゃねえよ、と思った。どうも具体的なモデルがいるようなのだが、私も知り合いが何人か浮ぶ。

 

 さて、当ブログの関心事としては押井守監督である。私はあらすじに「押井守が〜」と書いてあったので観にいったのだが、まさかそのまま本人が出てくるとは。

 麦くんは押井さんを見て「犬が好きな人ですよ。あと立喰そばも」と言っていた。犬が好きというのはけっこう有名というか「攻殻機動隊」や『スカイ・クロラ』を観れば明らかだが、立喰そばが好きというのはけっこうマニアックである。 しかし同じ場面で実写版『魔女の宅急便』を観たという人に対して(こういう人が実写版を生んでいるのか)と心の中で言うのだが、『魔女の宅急便』は児童文学が原作で、マンガの実写化とはちょっとわけが違うと思う。それよりもこの頃の押井さんがやっていた実写版パトレイバーのほうがヤバイのではないかと。

 本作は押井さんのどの作品よりもヒットしていると思う。押井さんはいったいどんな気持ちなんだろう。この作品を観た人のうちどれくらいが押井さんを知っているのだろう。逆に作中の世界で『花束みたいな恋をした』という映画をやっていたら絹ちゃんと麦くんは観るだろうか。いろいろ考えてしまった。

 ちょっとフィクション論のセンシティブなところに踏み込みはじめたのでついでに言っておくと、押井さんは本人役なのに戸田恵子さんが役者として出てくるのがめちゃくちゃ混乱した。戸田さんは押井作品には出ていないが(『ニルスのふしぎな旅』に出演しているようなのでまったく絡みがないわけではないかもしれない)、ガンダムをはじめとした富野監督作品や『キャッツアイ』で一世を風靡した80年代を代表する声優である。実写ドラマに出だしたのは90年代からだ。

 

  「出会いは別れを内在している」みたいな台詞があったけど「内在」ではなく「内包」では?

 

 映像の上手いところでは、よくあるのかもしれないけど、スマホ越しの顔にピントが合っていたのがその向こうの実物に切り替わるやつ、あれは良かった。

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

 ケンダル・ウォルトンの『フィクションとは何か』も勉強していきます。現題は"Mimesis as Make-Believe: On the Foundations of the Representational Arts"で、田村均先生による訳を使用*1

 そんなにガチではなくラフにいきます。今回は序章。

いろんな例

 1ページ目の冒頭を引用する。

 私の出発点は、絵画、小説、物語、戯曲、映画、といったものを単純に観察することである。例えばスーラの『グランド・ジャット島の日曜日の午後』や、ディケンズの『二都物語』、ヒッチコックの『北北西に進路を取れ』、イプセンの『ヘッダガーブラー』、モーツァルトの『魔笛』、ミケランジェロの『ダヴィデ像』、エドガー・アラン・ポーの『告げ口心臓』といった作品を、それが人生と文化に対してもっている重要性に十分注意しながらよく見るのである。

 これらは表象藝術(representational arts)虚構(fiction)といったものの例である。原著が出たのは1990年だが、けっこう古典的な例が多い。この後で棒馬(棒を馬に見立てて跨るやつ)などの境界事例を出しているが、こういった曖昧さがそのまま文化になったようなものはたくさんある。現代日本に住んでいれば、絵画や小説といったジャンル分けができないが文化として成立しているものを見るのは日常茶飯事だろう。我々が興味があるのはそこである。例えばアイドルとか、プロレスとか、VTuberとか、漫才とか、そういったものだ。

表象体(representations)

 このような境界事例がたくさんあるため、ウォルトンはこれらを表象体(representations)という漠然とした言葉で総称する。なぜ表象(representation)などという手垢にまみれた言葉を使うのかというと、みなが適当に使っている言葉だからこそ意味が固定されないという利点があるからである(3, 4ページ)。

 これはとても良い方針である。このブログを誰が読んでいるのかわからないが、大学生にアドバイスしたい。履修登録をする際に科目名に「表象」と付いた講義は取らないほうがいい。もし取ったなら先生に「表象ってどういう意味ですか?」と訊いてみるといい。奥歯に物が挟まった感じになると思う。それくらい表象という言葉は意味が定まらないままなんとなくかっこいいフレーズとして広まっているのである。

 それをあえて使っての表象体。

メイク・ビリーブ

 本書のテーマであるmake-believeだが、訳すのが難しいと訳注[4]にも書いてある。邦訳の副題にもあるが「ごっこ遊び」と訳すのが一般的である。だが実際にはこれは「『ごっこ遊びにおけるように、事実でないと分かってはいるが進んで受け入れることにする』という心的態度」を言う(序章訳注[4])。これは注意。

二種類の問い

 本書では二種類の問いを扱うという。一方は表象体の役割や鑑賞のあり方、私なりにいえば表象体に内在する固有の問題である。もう一方は登場人物の存在やそれを指示する言語表現の意味など、わりと伝統的な問題を表象体に適用することである。前者は美学的問題で後者は形而上学的あるいは意味論的問題とされる。

 ウォルトンによればこれら二つは密接に関係している。メイク・ビリーブの考え方を利用して統一的な理論を作ろうというのが本書のテーマである。また、これはさらにスポーツや宗教にも応用できるという。この射程の広さが先述の我々の興味にとって心強いのである。

「深刻ぶった女はキレイじゃない」が真であるのは深刻ぶった女がキレイではないとき、またそのときに限る(ホフディラン「スマイル」の歌詞を考える)

 タイトルは有名なタルスキの真理定義のパロディである*1*2

 タルスキはおいといて、ここではホフディランの「スマイル」という曲の歌詞を考察したいのよ。 


www.youtube.com

まあ名曲である。最近は森七菜さんのカバーによってリバイバルしている。


www.youtube.com

 で、この曲の歌詞の「深刻ぶった女はキレイじゃないから」とか「すぐスマイルするべきだ 子供じゃないならね」といったフレーズがよくないのではないかということが言われている。例えば以下のnote記事。

note.com

書いた方は大学教授らしい。要約すると、ホフディランの歌詞の女性観は古典的であるとのこと。「女性だって深刻な場面はいくらでもあるのに」と。この方はリアルタイムでそれを感じていたらしいが、現代の価値観にはなお合っておらず、オロナミンCのCMで森七菜さんに歌わせるべきではない、と。なるほど、確かにそうだ。

 また、このnoteでは出てこないが、ネット上では「モラハラ」という言葉とともに批判する意見が多く見られる。私は、自分で考えた解釈ならいいが、こういった新語や人文学・言論界の流行をなぞることで考えた気になってしまうような状態を危険視している。また、現代の「アップデートされた」価値観で作品を見ることはとても良いことなのだが、それがなにか知的な営為であるかのような風潮はちょっと嫌である。なのでや注意深くこのへんのことを考えたい。

 私としてはこの曲は、ひとりの男がひとりの女に語りかける歌で、あまり一般論を持ち込むべきではないのではないかと思う。

モラルハラスメントとは何か?

  モラハラモラルハラスメント)って最近よく聴くけどなんなのだろう。モラルを強要するハラスメントだろうか? 調べてみたらけっこう興味深いことがわかってきた。

モラルハラスメント - Wikipedia

 日本語版ウィキペディアを見ると、どうもマリー=フランス・イルゴイエンヌというフランスの精神病理学者が考えた概念らしい。フランス語版ウィキペディアにも記事がある。

Harcèlement moral — Wikipédia

しかし英語では"mobbing"というとある。英語版ウィキペディアには「モラルハラスメント」という項目はなく、モラルハラスメントのページで英語版のリンクを押すと"mobbing"のページに行く。見るとモラハラとはだいぶ違うしイルゴイエンヌの名もモラルという語も出てこない。モビングといったらカラスがタカにやる嫌がらせである。これを人間社会にも転用したものっぽい。

Mobbing - Wikipedia

なぜウィキペディアはこれらを同じ概念としてリンクを作っているのだろう?

 こういうことはままあるものである。つまり、世界の学術界で認められている統一された用語はないのだろうが、誰もが見たり経験したりしていることに別の名前が付いたということかと。ポルトガル語ウィキペディアのリンクを見ると「モラルハラスメント」らしき題だった。ロシア語版は違ったが。しかしだったらモラルハラスメントなる概念が必要なのかどうなのか。世界的にはどちらかというとモビングのほうが優勢かと思う。

 多くの人がぼんやりと抱えていたことに明確な名前が付いて共有しやすくなるのは良いことだが、気になるのは、語として明確になっても依然として概念はぼんやりしたままだということだ。モラルハラスメントの「モラル」ってなんなのだろう。モラルを押し付けることなのか、モラルに反した態度をとることなのか、これが調べても判然としない。「モラルに関するハラスメント」みたいな説明がよく出てくるが、それってどういうことなのか? ウィキペディアを見てもよくわからなかった。なんだかこの言葉、人を糾弾するための道具みたいなになってしまっていやしないだろうか。

 というわけなので、私は今後はモラハラという言葉を使わないようにしたいな〜と思った。モラハラという言葉を使っている文章を読むときは、それがどういう意味で使われているのかよく考えることとする。

好意的に解釈した「スマイル」

 作詞者のワタナベさんがどう思って書いているのか、あえてトゲのあるフレーズとして書いているのか本気でそういう人なのかわからないのでなんとも言えないところがある。先ほどのnoteを見た感じ他の曲の歌詞も怪しいようだ。だがこの「スマイル」は歌詞をよく読み込んでみると*3、これがけっこう深いことがわかる。

  「深刻ぶった女はキレイじゃないから」というのは、そう思っているというよりそう言って励ましているのだと思う。あえて警句っぽい言い方をしてちょっと皮肉まじりにおちゃらけた感じを出した表現なのではなかろうか。とするとこの歌詞に対して「女だって深刻な状況はある」と反応するのは変ではなかろうか。これは一般的な信念を述べているのではないと思う。また、おそらくこれはたいして深刻ではない場面なのだろう。例えば持ってた株が大暴落したとかそんな場面で「深刻ぶった女はキレイじゃない」とかそんなことは言わないだろう。

 ここで当記事のタイトル回収をしておく。20世紀前半の分析哲学では、論理学を駆使して言語の意味を考察するのが主流だった。この流れの金字塔がタルスキの真理理論である。真理とかそういった論理学の概念を使って意味を定義できる。対して20世紀後半には、人間の発話や会話には論理的な意味以上の(社会的な?)機能があるという考え方が出てきた。これを言語行為論という。思うにこの歌詞に対する怒りの反応の多くは、意味を論理的に考えすぎたのではないだろうか。この歌詞は意味内容よりもそれを言うという行為が持つ機能を受け取るべきなのだと思う。「深刻ぶった女はキレイじゃないのさ」の「のさ」が重要である。「深刻ぶった女はキレイじゃない」だけで成立する歌詞ではない。

 あとついでに述べておくが、先ほどのnoteで「自分はバリバリ仕事をする芯の強い女性が好きなので」と書いてあるのはちょっと違和感がある。「深刻ぶった女はキレイじゃない」に対して「女にも深刻な状況はある」と反論するのも変だが、さらに「深刻な女」の具体例を出しにいくのはもっと変である。べつにバリバリ仕事をする芯の強い女性でなくても深刻な場面は人生において多々あるだろう。これだと「一般に女性は深刻なことなどない」という価値観を共有してしまっている気がする*4

 実は「深刻ぶった女はキレイじゃないから」という一節は歌詞中で一度しか出てこない。それよりも「すぐスマイルするべきだ 子供じゃないならね」がバースの最後で反復され、曲全体の最後もこれで締められる。こちらのほうが高圧的に読めると私は思っていて、事実この一節への批判も多い。ただ、先ほどの「これはたいして深刻な場面ではない」という解釈が妥当ならば以下のことが言える。「いつでもスマイルしようね」とか「かわいくスマイルしててね」といった妙に優しげなフレーズが並ぶ歌詞のあとで必ず「すぐスマイルするべきだ 子供じゃないならね」と言ってちょっとピリッとするのがこの歌詞の仕組みなのではないか、と。この歌詞の主人公の男は、ずっとぐずっている女に対して最初は優しく接しようとするも、必ずしまいにはイラついてしまう、これがこの歌のストーリーなのではないかと。歌詞というものは全体でひとつの主張を持っているとは限らなくて、歌のなかで心情の変化が描かれることもあるだろう。微妙な関係の揺れ動き、恋人の日常のなかにあるちょっと不穏な空気、これがこの曲のテーマなのではなかろうか。ここまで読み込んでみて初めて言えるが、まあなかなか嫌な男である。ただ、嫌な人間が描かれているからといってダメな作品とはならない。むしろ人間の嫌な面に踏み込んでいるために名作になることもある。

 しかし、じゃあなんで森七菜さんがカバーしてオロナミンCのCMに使われるのかって話は当然ここでも残っている。なのでここへの批判は妥当かと。ただまあこれはこれでちょっと曲の雰囲気も変って新たな解釈の余地があるのかも。

 あと「すぐスマイルするべきだ」というのは「す」で頭韻を踏んでいて、全体にウ段を多用している。この聴き心地の良さの裏にトゲがあるのが良いのだろう。

  「深刻ぶった女はキレイじゃないから」も後半の「人間なんてそれほどキレイじゃないから」と対になっている。こういう構成のおもしろさも見逃せない。

まとめ

 企業CMが炎上するときになんかに、「その映像が現代社会において持っている意味」みたいなものが特に議論もされずなんとなく決まってしまっているかのようになることがよくある。しかし映像しかり歌詞しかり、それは意外に多くの情報を持っていたりする。

 すぐ文句を言わず、注意深く解釈してから批判するべきだ。

 子供じゃないならね。

*1:正確には「真理述語の定義」と言ったほうがいいですかね。

*2:「有名な」と言っても分析哲学においての話であって、分析哲学に興味のない方にはなんじゃそりゃだと思いますが…

*3:歌詞を読み込むということが正しい鑑賞態度といえるのかどうかは難しい問題です。あくまで作品は歌なので。おそらく分析美学でそういう研究があるはずなので、そのうちちゃんと調べます。

*4:どうです? ワシのほうがアップデートできてますでしょう?