論理的議論は、日常生活の情念や雑念を取り払った、シンプルでドライなスタイルで遂行します。例えば、日常会話においては、「Aである」と「Aでなくはない」の意味は違います（違いをうまく説明できないけど）。論理（古典論理*1）では、「Aである」と「Aでなくはない」は完全に同じです。日常言語の微妙さ・煩雑さを切り捨て、理想化・単純化することにより、強靭な推論能力が手に入るのです。
日常言語を使っているかぎり、日常の論理、あるいは日常の非論理が混ざり込むことは避けられません。論理的推論のための人工言語を使うのが望ましいでしょう。そこで、プログラミング言語TypeScriptを（かなり無理クリに）使って、論理的命題の記述を試みてみます。
本文中の例題を実行してみたい方は、最後の節を先に見てください。
内容：
- 命題と真偽判定とは何であるか
- TypeScriptを使う
- 言霊の影響からの脱却
- なぜTypeScriptなのか
- 論理結合子
- 含意命題
- 全称命題
- 全称命題の実行の仕掛け（インチキ）
- 含意と全称について考える
- まだ先があるけれど
- HTML／JavaScript／TypeScriptコード
命題と真偽判定とは何であるか
次の文を考えてみましょう。
- xは大きい数である。
この文は、普通は「命題ではない」と言われます。なぜかというと、大きい数かどうかの真偽判定の基準がないからです。であるなら、真偽判定の基準を作ればいいだけです。そのとき、日本語で基準を書かないでプログラミング言語で書くことにします。
JavaScriptで書いてみます。
function isLarge(x) { return (x > 100); }
ブラウザのコンソールで実験してみれば：
>> isLarge(3) false >> isLarge(100) false >> isLarge(100.01) true >> isLarge(200) true
上から順に：
- 「3 は大きい数である。」は偽
- 「100 は大きい数である。」は偽
- 「100.01 は大きい数である。」は真
- 「200 は大きい数である。」は真
と真偽判定できています。通常の表現では、「は真」は省略して、「は偽」を「ではない」と言うので：
- 「3 は大きい数である。」ではない
- 「100 は大きい数である。」ではない
- 「100.01 は大きい数である。」
- 「200 は大きい数である。」
日本語の言い回しと、鍵括弧・句読点を調整して：
- 3 は大きい数ではない。
- 100 は大きい数ではない。
- 100.01 は大きい数である。
- 200 は大きい数である。
真偽判定とはこういうものです。「大きい数である」の基準を定義すれば、それだけで真偽判定が可能となります。このとき：
- 「大きい数である」とは何か？ を国民投票で決める必要はありません。
- 知人を集めて会議を開く必要もありません。
- 哲学的議論も不要です。（むしろ、不毛です。）
- 国語辞書を引く必要もありません。
- 社会通念に合致しているかを検討する必要もありません。
単に、真偽値（trueまたはfalse）を返す関数を定義するだけです。
関数名isLargeは英語の句"is large"からとっているので、意味が推測できますが、次の関数を代わりに使ってもかまいません。関数名の選択も全く自由です*2。
// 一文字の名前 function L(x) { return (x > 100); }
あるいは、
// 意味不明な名前 function taboncha_hoy(x) { return (x > 100); }
またあるいは、
// 意味はわかるが、 // ふさわしいとは思えない名前 function BeerIsGood(x) { return (x > 100); }
真偽値を返す関数を定義すれば、それだけで真偽判定ができる -- この極めてシンプルでドライな事実が、なかなかに理解してもらえないようです。
TypeScriptを使う
TypeScriptは、JavaScriptに対して上位互換なプログラミング言語で、洗練された機能と構文を持ちます。JavaScriptにコンパイル（トランスパイル）されて実行されるので、ブラウザ（のコンソール）で確認できます。素晴らしい！
TypeScript自体の説明はここではしません。Web上にたくさんの資料があります。僕自身もTypeScriptの記事をいくつか書いていますが、ひとつだけ（最初に書いた）記事を挙げると：
- TypeScriptと関手やモナドなど （入門記事ではありません。）
TypeScriptでは、次の形で無名関数*3を書けます。
- (引数の宣言) : 戻り値の型 => 関数の本体
記号'=>'は、論理記号の'⇒'（意味は「ならば」）と似てますが関係ありません。関数のヘッド（見出し部）とボディ（本体部）を区切る記号です。
例えば、先のisLarge関数は、TypeScriptでは次のように書けます。
(x:number) :boolean =>(x > 100)
簡潔に書けるだけでなく、JavaScriptには無かった型宣言ができます。この関数はnumber型を引数にして、boolean型（真偽値型）の戻り値をとることを、明確に記述できます。素晴らしい！
(x:number) :boolean =>(x > 100) は無名関数ですが、そのまま引数を渡すことができます。((x:number) :boolean =>(x > 100))(3) とか ((x:number) :boolean =>(x > 100))(200) とかです。しかし、同じ関数を何度も使うときは名前がないと不便です。無名関数に名前を付けるには、次の形式を使うことにします。
let isLarge = (x:number) :boolean =>(x > 100)
1行のコードですが、解説しましょう。「let 名前 = 式」は、「名前を、式とする」とか「名前とは、式のことである」と読めばいいでしょう。この例では：
- isLarge を、 (x:number) :boolean =>(x > 100) とする。
- isLarge とは、 (x:number) :boolean =>(x > 100) のことである。
式の部分は既に紹介した無名関数です。この無名関数は、次のように読めます。
- ヘッド部 (x:number) :boolean --- 型がnumberである引数xに対して、型がbooleanである戻り値を返す。
- ボディ部 (x > 100) --- 引数xが100より大きいかどうかを判定する。
TypeScriptには型があるので、関数isLargeの引数に文字列や配列が入ることはありません。コンパイラがチェックしてくれます。しかし、数値型がnumber型しかないので、整数と実数（コンピュータでは浮動小数点数）の区別もできません。そこで、TypeScriptにはない数値型を新しく導入します。natural, integer, rational, real の4つの型です。
| 型の名前 | 対応する集合 | 意味 |
|---|---|---|
| natural | N | 自然数の型 |
| integer | Z | 整数の型 |
| rational | Q | 有理数の型 |
| real | R | 実数の型 |
これらの新しい型をほんとに導入することは、TypeScripでは（ほとんどのプログラミング言語で）出来ません。組み込み型としてサポートすべき型です。なので、実際には型の名前だけ使えて、実質はnumberです。型の名前を使えるようにする仕掛けは後の節で明かします。
数値データやオブジェクトが、natural, integer, rational, real の4つの型に所属するかどうかを判定するには、次の関数が使えます。
- isNatural(x:any) :boolean
- isInteger(x:any) :boolean
- isRational(x:any) :boolean
- isReal(x:any) :boolean
型がナンチャッテ型なので、型への所属判定もナンチャッテですが、isNaturalとisIntegerはまーまー信頼できます。
さて、数の種類を自然数に特定した次の命題を考えます。
- 自然数xは大きい数である。
この命題に対応する真偽判定関数は次のように書けます。
let isLargeNatural = (x:natural) :boolean =>(x > 100)
引数の型がnumberからnaturalに変わっただけです。
言霊の影響からの脱却
TypeScriptで色々な命題を書いていきたいわけですが、その前に、僕がこんなことをしようとした動機を説明します。
数学的・論理的な命題を自然言語（我々にとっては日本語）で書くのは、なにかと問題があると思います。まず、自然言語は曖昧だから、正確な記述が難しいという問題が思い浮かぶでしょう。ですが、それより深刻な問題は、自然言語が強烈なイメージ喚起力を持っていることです。個々の言葉が、それぞれの人ごとに、経験や環境や状態に依存した強い連想を引き起こすこと -- これが大きな問題です。
例えば、先に扱った例である「大きい数」を「定義する」場合、「大きい数」「定義する」という日本語が、心のなかに様々な思いを湧き上がらせ、葛藤を引き起こします。
- 世間の人々は、どのくらいの数を「大きな数」と呼ぶんだろう？
- アンケート調査したほうがいいのかな？
- Wikipediaに「大きな数」ってないのか、調べてみよう。
- 「100を超えたら大きな数」って決めたら、誰かが「俺は300以上だと思う」とか言い出さないか？
- そもそも、ボクに「大きな数」を定義する資格なんてあるのだろうか？ そんな大それた事はボクには出来ない。
我々は、社会のなかで日常生活を営んでいます。その日常において使う言語が自然言語であるため、自然言語の言葉は社会や個人と深く結びつき、言葉を使うと同時に、現実世界や感情の世界に巻き込まれます。自然言語（日本語）には言霊〈ことだま〉が宿るとかいいますが、強烈なイメージ喚起力は言霊のパワーなのかも知れません。
数学的・論理的な命題の記述と解釈においては、言霊の影響 -- 現実世界や感情の世界への連想・参照 -- をできるだけ排除したい。命題を記述・解釈するとき、今日の天気も気分も株価も、消費税率も世界情勢も関係ないのです。ひたすらドライに真偽判定だけに注目します。
定義（それと公理）は、真偽判定をする際のベースを与えるものです。誰がどんな定義をしようが全く自由です。何の資格も要らないし（定義士2級試験とかない！）、明確であれば（真偽判定が実際にできれば）内容的制限もありません。矛盾したらマズイのですが、あえて「俺は矛盾した体系が作りたい」のであれば、それさえも自由です。
数学的・論理的な定義をするとき、あるいは公理を提示するとき、あなたの家族や友人や会社に許可を取る必要はないし、社会通念や多数派の意見を考慮する必要はないし、国語辞書やWikipediaを引用する必要もありません。それらを無視しろ、ということではなく、単に関係ないのです。ひたすら関係ないのです。
なんか誤解されそうな言い方をしてますが、一旦誤解されてその誤解を解くほうが楽なんで、今言ったことに注釈や補足を付けることはしません*4。ともかく、命題を扱う際は真偽判定に集中してください。言霊の影響を断ち切ってください。
なぜTypeScriptなのか
言霊の影響を断ち切るには、自然言語を使うのをやめて、人工言語を使えばいいのです。標準的な（ポピュラーな）人工言語は、古典述語論理とラムダ計算でしょう。しかし、これらの言語にどうも馴染めない、という人もいるし、ソフトウェアで構文をチェックしたり実行したりするすることが（お手軽には）できません。
Coq、Isabelle、Mizarなんてプログラミング言語もありますが、これらも敷居が高いので、普通のプログラミング言語（汎用プログラミング言語）を使うことにします。そう、TypeScriptです。TypeScriptがサンプル記述に向いていることは次の記事で書いています（興味があれば見てください）。
TypeScriptは、命題や証明の記述を目的にしてないので、うまくいかない事も多々あるんですが、そこは姑息な小手先の対処で乗り切りましょう。小手先の対処なので、実用性はありません。しかしそれでも、古典述語論理・ラムダ計算入門の素材、言霊の呪縛から逃れる手段としては使えると思います。
論理結合子
2つの命題を結びつけたり、命題の意味を変える演算子を論理結合子〈logical connective〉といいます。次の対応表を見るのが早いでしょう。
| 名称 | 意味 | 論理記号 | TypeScript |
|---|---|---|---|
| 連言 | かつ | ∧ | && |
| 選言 | または | ∨ | || |
| 否定 | ではない | ¬ | !, not |
| 含意 | ならば | ⇒, ⊃ | ? : true |
論理記号は比較的よく使われているものを選びました。他の論理記号については次の記事を見てください（興味があれば）。
TypeScriptの（というかJavaScriptの）演算子 &&, ||, ! は、論理の「かつ〈and〉」「または〈or〉」「ではない〈not〉」と同じか？ と聞かれると、「いや、違う」と答えざるを得ないのですが、我々の目的内では論理的な演算子と解釈しても大丈夫です。否定の ! は、not関数の形も許します。「ならば〈implies〉」として使う ? : true は、三項演算子の最後の項（引数）にtrueを入れたものです。
isLarge(x:number) :boolean が既に定義されているとして、論理結合子〈論理演算子〉を使った例を見てみましょう。
let bothAreLarge = (x:number, y:number) :boolean =>(isLarge(x) && isLarge(y)) let atLeastOneIsLarge = (x:number, y:number) :boolean =>(isLarge(x) || isLarge(y)) let isNotLarge = (x:number) :boolean =>(not(isLarge(x))) let bothAreNotLarge = (x:number, y:number) :boolean =>(isNotLarge(x) && isNotLarge(y))
ブラウザで試してみます。
>> bothAreLarge(30, 200) false >> bothAreLarge(300, 200) true >> atLeastOneIsLarge(0, 100.01) true >> atLeastOneIsLarge(200, 100.01) true >> bothAreNotLarge(0, 100.01) false >> bothAreNotLarge(0, 100) true
人工言語であるTypeScriptの実行結果を、自然言語である日本語に翻訳すれば次のようになります。
- 「30 と 200 の両方とも大きな数である。」は偽
- 「300 と 200 の両方とも大きな数である。」は真
- 「0 と 100.01 の少なくともひとつは大きな数である。」は真
- 「200 と 100.01 の少なくともひとつは大きな数である。」は真
- 「0 と 100.01 の両方とも大きな数ではない。」は偽
- 「0 と 100 の両方とも大きな数ではない。」は真
日本語の言い回しと、鍵括弧・句読点の調整は皆さんにお任せします。
含意（「ならば」）の使用例は次節にします。
含意命題
そろそろ「大きな数」の例も飽きてきたので、別な例題にします。自然数（非負の整数）だけを考えることにして、次の命題を例にします。
- x は y の倍数である。
TypeScriptで定義します。
let isMultipleOf = (x:natural, y:natural)/*{y !== 0}*/ :boolean =>(x % y === 0)
解説します。
- 命題の真偽判定をする関数の名前は isMultipleOf です。
- 引数は2つで、型はどちらも natural（自然数）です。
- /*{y !== 0}*/ は、第二引数 y に0は入れないでね、という制約です。コメントなので実効性はありませんが、守ってくれると信じましょう。
- 関数の戻り値は boolean（真偽値）です。
- 関数の本体は、引数 x を引数 y で割り算した余りを求めて0と比較するだけです。'%'は割り算の余りを求める演算子、'==='は等号です*5。
ちょっとだけ試してみます。
>> isMultipleOf(4, 2) true >> isMultipleOf(2, 4) false >> isMultipleOf(12, 4) true >> isMultipleOf(5, 4) false >> isMultipleOf(5, 5) true
説明はいらないでしょう。
さて、次の2つの命題を考えます。
- 4の倍数は2の倍数である。
- 4の倍数は3の倍数である。
もっとハッキリと言えば：
- x が 4 の倍数であるなら、x は 2 の倍数でもある。
- x が 4 の倍数であるなら、x は 3 の倍数でもある。
日本語としてのテニヲハとか句読点とかはどうでもいいので、
- x は 4 の倍数である ならば x は 2 の倍数である。
- x は 4 の倍数である ならば x は 3 の倍数である。
これらの命題は、TypeScriptで次のように書きます。
let multipleOf4IsMultipleOf2 = (x:natural) :boolean =>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true ) let multipleOf4IsMultipleOf3 = (x:natural) :boolean =>( isMultipleOf(x, 4) ? isMultipleOf(x, 3) : true )
「A ならば B」（記号的には「A ⇒ B」）という命題は、TypeScriptでは
- A ? B : true
という形で書きます。'?'と':'の組み合わせに慣れてない方は、次のif文と同じと思ってください。
if (A) { return B; } else { return true; }
一番目の命題を、JavaScript構文とif文で書けば：
function multipleOf4IsMultipleOf2(x) { if (isMultipleOf(x, 4)) { return isMultipleOf(x, 2); } else{ return true; } }
「A ならば B」の形の命題を含意命題〈conditional proposition | 条件命題〉と呼びます。Aを含意命題の前件〈antecedent〉と呼び、Bは後件〈succedent〉と呼びます。前件が偽のときは、含意命題全体は真になります。これも、哲学的・言語学的思弁にふけらないで、含意〈implication〉とはそういうものだ、と割り切ってください*6。「ならば」という日本語や、日本語を使う個人・社会を分析するのではなく、上に示したようなプログラムの挙動が分析の対象です。
では、実行して試してみます。
>> multipleOf4IsMultipleOf2(1) true >> multipleOf4IsMultipleOf2(2) true >> multipleOf4IsMultipleOf2(4) true >> multipleOf4IsMultipleOf3(12) true >> multipleOf4IsMultipleOf3(24) true
日本語に翻訳すれば：
- 「1 は 4 の倍数である ならば 1 は 2 の倍数である。」は真
- 「2 は 4 の倍数である ならば 2 は 2 の倍数である。」は真
- 「4 は 4 の倍数である ならば 4 は 2 の倍数である。」は真
- 「12 は 4 の倍数である ならば 12 は 3 の倍数である。」は真
- 「24 は 4 の倍数である ならば 24 は 3 の倍数である。」は真
1番目、2番目の命題で、「1 は 4 の倍数である」「2 は 4 の倍数である」は偽なので、全体は真です。こう真偽判定しないとダメな理由は次節以降で明らかになります。
全称命題
もう一度、前節で扱った2つの命題を挙げます。
- x が 4 の倍数であるなら、x は 2 の倍数でもある。
- x が 4 の倍数であるなら、x は 3 の倍数でもある。
1番目は真だが、2番目は偽のように思えます。しかし、2番目の命題が真になることもあるのは実験で確認済みです。これも再掲しましょう。
>> multipleOf4IsMultipleOf3(12) true >> multipleOf4IsMultipleOf3(24) true
xの値を12や24にしたときは、「x が 4 の倍数であるなら、x は 3 の倍数でもある。」は真になります。それなのに、2番目の命題は偽だと判断する根拠は何でしょう？ これは、ヨーク考えてみるべきことです。
我々が、変数を含む命題を解釈するとき、「どんな場合でも」「いつでも」「常に」といった言葉を先頭に付けているのです（無意識かも知れませんが）。「どんな場合でも」を先頭に付けると：
- どんな場合でも、x が 4 の倍数であるなら、x は 2 の倍数でもある。
- どんな場合でも、x が 4 の倍数であるなら、x は 3 の倍数でもある。
そうなると、たまたまxの特定の値で命題が成立しても、「どんな場合でも」とは言えません。実際、x = 4 で実験すると：
>> multipleOf4IsMultipleOf3(4) false
これが、2番目が偽である理由です。
「どんな場合でも」をもっと正確に言うと「x がどんな数であっても」です。数の種類（型）は自然数（natural型）だとしていたので、「x がどんな自然数であっても」です。論理記号では「∀x∈N」と書きます。記号'∀'は、"Any", "All"の"A"をひっくり返したものです。"for all x in natural"のように読みます。論理記号'∀'で始まる命題を全称命題〈universal proposition〉と呼びます。
全称命題を日本語で言うときは、「どんな自然数xでも」「すべての自然数xは」「任意の自然数xにおいて」「勝手に取った自然数xに対して」など様々な言葉使いをします。日本語表現の微妙な差異を分析するとかやりだすと*7、ラチがあかない、どうにもならないのでやめましょうね。くどく言いますが、我々は日本語を調査・分析したいのではありません！ むしろ日本語を使いたくないのです。
さて、∀x∈N.( … ) をTypeScriptでどう書けばいいでしょう。
- forAll(x:natural)( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true )
のように書けたら非常によいのですが、これは無理です。
- forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true) )
これでもいいですね。forAllの内部は無名関数です。forAllを、何もしないダミー関数として定義すれば、この書き方が出来ますが、実行は無意味になってしまいます。
多少は意味がある実行をするために、次の書き方とします。naturalを二度書く必要がありますが、我慢してください*8。
- natural.forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true) )
ところで、forAllのなかに入っている関数は既に名前が付いてました。以下に再掲。
let multipleOf4IsMultipleOf2 = (x:natural) :boolean =>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true )
この名前 multipleOf4IsMultipleOf2 を無名関数の代わりに使っても同じです。
- natural.forAll(multipleOf4IsMultipleOf2)
実験してみます。
>> natural.forAll(multipleOf4IsMultipleOf2) true >> natural.forAll(multipleOf4IsMultipleOf3) false
G
期待通りの結果になりました。種明かしは次節でします。
なお、注意事項ですが、TypeScriptソースコード上では natural.forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true) ) のように書けますが、ブラウザのコンソールでTypeScriptは使えないので、JavaScriptの書き方をしなくてはなりません(泣)。natural.forAll( function(x){return isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true} ) ですね。僕は、コンソールにTypeScript式を入れて、構文エラーでしばらく困惑してました、ダハハハ。
全称命題の実行の仕掛け（インチキ）
例題である全称命題を再度確認しましょう。
- 日本語： どんな場合でも、x が 4 の倍数であるなら、x は 2 の倍数でもある。
- より正確な日本語： 任意の自然数 x に対して、x が 4 の倍数である ならば x は 2 の倍数である。
- 論理式： ∀x∈N.( isMultipleOf(x, 4) ⇒ isMultipleOf(x, 2) )
- TypeScript： natural.forAll( (x:natural)=>(isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true) )
この命題の真偽判定をするには、変数xにすべての自然数を代入して確認する必要があります。自然数は無限個あるので、そんなことがコンピュータに出来るはずもなく、実行はハナからインチキだと分かります。
インチキの手口を紹介しましょう。まず、配列変数naturalが次のように定義されています。
var natural = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9];
配列のメソッドforAllが事前に定義されていて、natural.forAll(fn) と呼び出すと、次のコードと同じ働きをします。
var len = natural.length; var result = true; var i; for (i = 0; i < len; i++) { result = result && fn(natural[i]); } return result;
要するに、0から9の10個の自然数に対してだけ関数値（boolean型の値になる）をチェックして、全部trueならtrueを、そうでないならfalseを返すのです。natural.forAll(fn) の値は、次の長い式の値と同じです。
fn(0) && fn(1) && fn(2) && fn(3) && fn(4) && fn(5) && fn(6) && fn(7) && fn(8) && fn(9)
含意と全称について考える
「ならば」（論理記号では'⇒'）と「任意の」（論理記号では'∀'）を含むような命題は非常にしばしば登場します。「4の倍数は2の倍数である。」は次のように書けたのでした。
- より正確な日本語： 任意の自然数 x において、x は 4 の倍数である ならば x は 2 の倍数である。
- 論理式： ∀x∈N.( isMultipleOf(x, 4) ⇒ isMultipleOf(x, 2) )
- TypeScript： natural.forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true ) )
全称命題は、「どんな場合でも成立する」と主張するので、この場合「x = 0 でも、x = 1 でも、x = 2 でも、x = 3 でも、x = 4 でも、x = 5 でも、その他 x がどんな自然数でも」ということです。
- x = 0 のとき： 0 は 4 の倍数である ならば 0 は 2 の倍数である。
- x = 1 のとき： 1 は 4 の倍数である ならば 1 は 2 の倍数である。
- x = 2 のとき： 2 は 4 の倍数である ならば 2 は 2 の倍数である。
- x = 3 のとき： 3 は 4 の倍数である ならば 3 は 2 の倍数である。
- x = 4 のとき： 4 は 4 の倍数である ならば 4 は 2 の倍数である。
- x = 5 のとき： 5 は 4 の倍数である ならば 5 は 2 の倍数である。
- … …
ここでもし、「0 は 4 の倍数である ならば 0 は 2 の倍数である。」を偽と判定すると、x = 0 の時点で命題は成立せず、「どんな場合でも成立する」と主張できるはずありません。含意命題の前件「0 は 4 の倍数である」が偽のときは、これはヨシ（つまり真）として、さっさと先に進むのです。
もう一方の命題「4の倍数は3の倍数である。」も考えてみましょう。
- より正確な日本語： 任意の自然数 x において、x は 4 の倍数である ならば x は 3 の倍数である。
- 論理式： ∀x∈N.( isMultipleOf(x, 4) ⇒ isMultipleOf(x, 3) )
- TypeScript： natural.forAll( (x:natural)=>( isMultipleOf(x, 4) ? isMultipleOf(x, 3) : true ) )
「どんな場合でも成立する」と主張しているので、
- x = 0 のとき： 0 は 4 の倍数である ならば 0 は 3 の倍数である。
- x = 1 のとき： 1 は 4 の倍数である ならば 1 は 3 の倍数である。
- x = 2 のとき： 2 は 4 の倍数である ならば 2 は 3 の倍数である。
- x = 3 のとき： 3 は 4 の倍数である ならば 3 は 3 の倍数である。
- x = 4 のとき： 4 は 4 の倍数である ならば 4 は 3 の倍数である。
- x = 5 のとき： 5 は 4 の倍数である ならば 5 は 3 の倍数である。
- … …
このなかで注目すべきは、「4 は 4 の倍数である ならば 4 は 3 の倍数である。」です。含意命題の前件「4 は 4 の倍数である」は真ですが、後件「4 は 3 の倍数である」が偽です。これは、もとの主張に対する反例です。反例が見つかったので全称命題は偽です。しかし、最初の「0 は 4 の倍数である ならば 0 は 3 の倍数である」は反例ではありません。なぜなら、この命題は真だからです。
今の例では、xが0から9の範囲で反例が見つかって偽と判定できましたが、コンピュータでの実行では、調べた範囲に反例が見つからないでtrueを返すこともあります。無限に調べられないので、コンピュータからの報告は当てになりません！
0から9の範囲を広げて、0から百兆にしたところで事情は変わりません。だから、実験ではなくて証明が必要になるのです。
まだ先があるけれど
全称命題は紹介しましたが、全称とペアになる存在命題があります。また、「ただひとつだけ存在する」を意味する存在命題（一意存在命題）も重要です。一意存在命題に基づいて関数を定義することが非常にしばしばあります。例えば：
- 日本語： 実数 a に対して、a が非負なら、x2 = a かつ x ≧ 0 である実数xがただひとつだけ存在する。
- 論理式： ∀a∈R.( a ≧ 0 ⇒ ∃!x∈R.( x2 = a ∧ x ≧ 0 ) )
- TypeScript：すぐ下(↓)
real.forAll( (a:real)=>(
a >= 0 ?
real.uniquelyExists( (x:real)=>(
x*x === a &&
x >= 0 )
) : true )
)
'∃!'と'uniquelyExists'は、一意存在の論理記号です。この一意存在命題に基づいて非負平方根関数が定義されます。そのとき、「… であるところの x」という意味の論理記号が使われます。
このへんの話はちょっと難しいのでまたの機会にします。今日のところは、日本語表現にまとわりつく余計な情感や怨念(?)、邪魔になる意味的夾雑物を取り除くためにプログラミング言語表現が使えることが分かれば十分です。
HTML／JavaScript／TypeScriptコード
ブラウザで実験したいときは、次のようなHTMLファイルを作ります。
<!DOCTYPE html> <html> <head> <meta charset="utf-8"> <title>logical</title> <script src="./logical-support.js"></script> <script src="./logical.js"></script> <script src="./my-sample.js"></script> </head> <body> <h1>logical</h1> </body> </html>
読み込んでいるJavaScriptファイルのなかで、logical-support.jsは直接JavaScriptで手書きしたファイルです。「今どき、prototype使いやがって」と怒られそうですが、これしか手段が思いつかなくて …
/* logical-support.js */ Array.prototype.forAll = function(condFn) { var arr = this; var len = arr.length; var result = true; var i; for (i = 0; i < len; i++) { result = result && condFn(arr[i]); } return result; } Array.prototype.exists = function(condFn) { var arr = this; var len = arr.length; var result = false; var i; for (i = 0; i < len; i++) { result = result || condFn(arr[i]); } return result; } Array.prototype.uniquelyExists = function(condFn) { var arr = this; var len = arr.length; var count = 0; var i; for (i = 0; i < len; i++) { if (condFn(arr[i])) { count++; } } return (count === 1); } Array.prototype.the = function(condFn) { var arr = this; var len = arr.length; var count = 0; var item; var i; for (i = 0; i < len; i++) { if (condFn(arr[i])) { count++; item = arr[i]; } } if (count !== 1) throw "Not exist or Not unique"; return item; }
logical.jsとmy-sample.jsは、対応するTypeScriptファイルをコンパイルしたものです。先にコンパイル済みのJavaScriptコード、その後にTypeScriptソースコードを示します。
// logical.ts var natural = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]; var integer = [-5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5]; var rational = [-2, -1.5, -1, -0.5, 0, 0.5, 1, 1.5, 2]; var real = [-2, -1.5, -1, -0.5, 0, 0.5, 1, 1.5, 2]; var isNatural = function (x) { return ((typeof x) === 'number' && Math.ceil(x) === x && x >= 0); }; var isInteger = function (x) { return ((typeof x) === 'number' && Math.ceil(x) === x); }; var isRational = function (x) { return ((typeof x) === 'number'); }; var isReal = function (x) { return ((typeof x) === 'number'); }; var not = function (x) { return (!x); };
// my-sample.ts /// <reference path="./logical.ts" /> var isLarge = function (x) { return (x > 100); }; var bothAreLarge = function (x, y) { return (isLarge(x) && isLarge(y)); }; var atLeastOneIsLarge = function (x, y) { return (isLarge(x) || isLarge(y)); }; var isNotLarge = function (x) { return (not(isLarge(x))); }; var bothAreNotLarge = function (x, y) { return (isNotLarge(x) && isNotLarge(y)); }; var isMultipleOf = function (x, y) { return (x % y === 0); }; var multipleOf4IsMultipleOf2 = function (x) { return (isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true); }; var multipleOf4IsMultipleOf3 = function (x) { return (isMultipleOf(x, 4) ? isMultipleOf(x, 3) : true); }; var nonNegativeSquareRootUniquelyExists = real.forAll(function (a) { return (a >= 0 ? real.uniquelyExists(function (x) { return (x * x === a && x >= 0); }) : true); });
// logical.ts type natural = number; type integer = number; type rational = number; type real = number var natural = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]; var integer = [-5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5]; var rational = [-2, -1.5, -1, -0.5, 0, 0.5, 1, 1.5, 2]; var real = [-2, -1.5, -1, -0.5, 0, 0.5, 1, 1.5, 2]; let isNatural = (x:any) =>( (typeof x) === 'number' && Math.ceil(x) === x && x >= 0 ) let isInteger = (x:any) =>( (typeof x) === 'number' && Math.ceil(x) === x ) let isRational = (x:any) =>( (typeof x) === 'number' ) let isReal = (x:any) =>( (typeof x) === 'number' ) interface Array<T> { forAll( condFn: (item:T)=>boolean ) : boolean; exist( condFn: (item:T)=>boolean ) : boolean; uniquelyExists( condFn: (item:T)=>boolean ) : boolean; the( condFn: (item:T)=>boolean ) : T; } let not = (x:boolean)=>(!x)
// my-sample.ts /// <reference path="./logical.ts" /> let isLarge = (x:number)=>(x > 100) let bothAreLarge = (x:number, y:number) :boolean =>(isLarge(x) && isLarge(y)) let atLeastOneIsLarge = (x:number, y:number) :boolean =>(isLarge(x) || isLarge(y)) let isNotLarge = (x:number) :boolean =>(not(isLarge(x))) let bothAreNotLarge = (x:number, y:number) :boolean =>(isNotLarge(x) && isNotLarge(y)) let isMultipleOf = (x:natural, y:natural)/*{y !== 0}*/ :boolean =>(x % y === 0) let multipleOf4IsMultipleOf2 = (x:natural) :boolean =>( isMultipleOf(x, 4) ? isMultipleOf(x, 2) : true ) let multipleOf4IsMultipleOf3 = (x:natural) :boolean =>( isMultipleOf(x, 4) ? isMultipleOf(x, 3) : true ) let nonNegativeSquareRootUniquelyExists :boolean = real.forAll( (a:real)=>( a >= 0 ? real.uniquelyExists( (x:real)=>( x*x === a && x >= 0 ) ) : true ) )
*1:我々が使う論理は古典論理だと思っていいです。たくさんの非古典論理がありますが、当面は非古典論理を考える必要はありません。
*2:良いプログラミングの習慣として、分かりやすい名前を付けることが推奨されます。しかし、「名前によって関数の挙動が変わったりしない」という事実がとても重要です。
*3:匿名関数、インライン関数ともいいます。また、クロージャとかラムダ式と呼ぶこともあります。このへんの言葉使いについては「クロージャとラムダ式は同義だ、と主張してみる」、クロージャとオブジェクトの関係は「クロージャなんて貧乏人のオブジェクトだろ」を参照。
*4:って言っておいて、ひとつだけ注釈： 図形に対して「幾何的直感を使うな」とか、「比喩的説明はけしからん」とかではないです。全然違います。日本語の語・句・文から呼び起こされる印象・感情を論理的判断の基準にはできない、という話です。
*5:僕は習慣的に3個のイコールを並べてしまうのですが、2個のイコールでもたいてい問題はありません。
*6:含意命題の真偽表〈真理値表〉をどう埋めるか？ という問題です。この定義以外では具合が悪い理由がいくつもありますが、詳細は割愛します。
*8:内側の (x:natural) の natural は省略しても動作に関係しません。短く書きたいときは省略してもいいです。
