プログラマー向けの（？）数理論理学（１）数学的言明

プログラマー向けというか、数理論理学の枠組みをプログラムとして実装したい人とか形式化数学をやりたい人向けの記事かもしれません（形式化数学についてはこちらの記事もどうぞ）。

また、1年前にも似たような内容の連載を書こうとして1記事目で止まってしまったので今回最初から書き直すことにしました。

数理論理学とは

数理論理学とは数学的な議論を厳密に行うために必須となる数学のツールであり、たとえば、「2は素数である」というような数学的言明やより複雑なものを数学的に取り扱うための理論です。

数学的言明

数学における全ての主張は数学的言明として表されますが、数学的言明は真である（正しい）か偽である（正しくない）かが明確に判断できるような形になっていなければなりません。つまり、曖昧な部分がなく完全に明確に述べられていなければなりません。

そして、複雑な数学的言明はより単純な数学的言明が論理的に組み合わされた形となることもあります。

単純な数学的言明から複雑な数学的言明を組み立てる際に使用されるのが下のような論理結合子と呼ばれるものです。

• 否定・・・「～でない」という意味です。たとえば、「2は素数でない」という言明は「2は素数である」という言明を否定したものです。記号は￢を使います。
• 連言・・・「～かつ・・・」という意味です。たとえば、「2は素数であり、かつ、3も素数である」という言明は「2は素数である」という言明と「3は素数である」という言明の連言です。記号は∧を使います。
• 選言・・・「～または・・・」という意味です。たとえば、「2は素数であるか、または、3は素数である」という言明は「2は素数である」という言明と「3は素数である」という言明の選言です。記号は∨を使います。
• 含意・・・「～ならば・・・」という意味です。たとえば、「2が素数であるならば3は素数である」という言明は「2は素数である」という言明と「3は素数である」という言明の含意です。記号は→を使います。
• 同値・・・「～ならば・・・かつ・・・ならば～」という意味です。たとえば、「2が素数であるならば3は素数であり、かつ、3が素数であるならば2は素数である」という言明は「2は素数である」という言明と「3は素数である」という言明の同値です。記号は↔を使います。

このような論理結合子によって組み立てられた複雑な数学的言明は部品となった数学的言明が真であるか偽であるかによってその真偽も決まることに注意してください。

たとえば、「2は素数でない」という言明の真偽は「2は素数である」という言明が真である場合には必ず偽となるし、逆に偽である場合には必ず真となります。

また、具体的な数学的言明は無数にありますが（たとえば、「2は素数である」、「3は素数である」、「4は素数である」・・・）、論理結合子それぞれの作用は変わりません（たとえば、「2は素数でない」という言明と「3は素数でない」という言明における「～でない」という否定の論理結合子の働きは同じ）。

ですから、論理結合子の作用を考える際には具体的な数学的言明それぞれにおける作用を1つずつ考えるのではなく、あらゆる数学的言明を表すメタ変数P、Q、Rなどを導入し、「Pでない」、「PかつQ」などの真偽がP、Qなどの真偽に応じてどのようになるかを考えます。

それを表形式で表すと下のようになります。ただし、Tは「真」を表し、Fは「偽」を表します。

• Pでない（￢P）

P	￢P
T	F
F	T

• PかつQ（P ∧　Q）

P	Q	P ∧ Q
T	T	T
T	F	F
F	T	F
F	F	F

• PまたはQ（P ∨　Q）

P	Q	P ∨ Q
T	T	T
T	F	T
F	T	T
F	F	F

• PならばQ（P →　Q）

P	Q	P → Q
T	T	T
T	F	F
F	T	T
F	F	T

• PならばQかつQならばP（P ↔　Q）

P	Q	P ↔ Q
T	T	T
T	F	F
F	T	F
F	F	T

数学的言明の取り扱い（プログラム上）

ここから下は数学的言明をプログラムでどう実装するかという話なので、プログラミングに興味のない方は飛ばして次の記事に進んでください。

---

それではこのような数学的言明をプログラム上で扱うにはどのようにすれば良いでしょうか？

まずプログラム上で、たとえば、「2は素数である」というような具体的な数学的言明を扱うには「2」のような数学的対象物や「素数」のような数学的概念をプログラムで定義できるような機構を導入しなければならなくなり、それを今説明するのは難しいので、今回はP、Q、Rのようなあらゆる数学的言明を表すメタ変数を数学的言明として取り扱うことを考えます。

最終的にはこのようなメタ変数に具体的な数学的言明を代入することが可能になることになります。

ということは最初にP、Q、Rのようなメタ変数をプログラム上で作れるようにしなければなりません。

このメタ変数は

• 無限に作れなければならない。
• 重複してはならない。

ので、P、Q、Rのような変数名を採用するよりはP1、P2、P3のようなPの後に連番を付加するスタイルの方が実装しやすいですので、この方法で実装しましょう。

メタ変数を作る関数は下のようになります。

function create_proposition (index) {
  return {
    type: 'prop',
    subtype: 'atom',
    index: index
  }
}

単純な関数です。

メタ変数のPの後の数字をindex引数として受け取り、メタ変数を表すオブジェクトを返すだけの関数です。

このオブジェクトのtypeプロパティはpropとしています。typeプロパティはオブジェクトの種類を表すためのもので、propはこのオブジェクトが数学的言明を表すことを示しています。

propはpropositionの略なのですが、たとえば、CoqでもProp型として採用されています。

そして、subtypeプロパティはatomとしています。subtypeプロパティはオブジェクトの更に細かい種類を識別するためのものでatomはこのオブジェクトがメタ変数を表すことを示しています。

atomは「原子的な」という意味で、数学的言明の最小単位であることを表しています。

そして、indexプロパティにはindex引数の値を格納します。

メタ変数を作る関数が作成できたので、次は論理結合子によって組み立てられる数学的言明を作る関数を実装していきます。

基本的な実装方法はメタ変数の場合と同じで、作成する数学的言明の材料となる数学的言明を表すオブジェクトを引数として受け取り、新しい数学的言明を表すオブジェクトを作成し、それを返すだけです。

ですから下のようになります。

function create_negation (p) {
    if (p.type !== 'prop') {
        throw new Error('not prop.');
    }

    return {
        type: 'prop', 
        subtype: 'neg', 
        sub: p
    };
}

function create_conjunction (p1, p2) {
    if (p1.type !== 'prop') {
        throw new Error('not prop.');
    }
    if (p2.type !== 'prop') {
        throw new Error('not prop.');
    }

    return {
        type: 'prop', 
        subtype: 'conj', 
        sub1: p1, 
        sub2: p2
    };
}

function create_disjunction (p1, p2) {
    if (p1.type !== 'prop') {
        throw new Error('not prop.');
    }
    if (p2.type !== 'prop') {
        throw new Error('not prop.');
    }

    return {
        type: 'prop', 
        subtype: 'disj', 
        sub1: p1, 
        sub2: p2
    };
}

function create_implication (p1, p2) {
    if (p1.type !== 'prop') {
        throw new Error('not prop.');
    }
    if (p2.type !== 'prop') {
        throw new Error('not prop.');
    }

    return {
        type: 'prop', 
        subtype: 'imp', 
        sub1: p1, 
        sub2: p2
    };
}

function create_equivalence (p1, p2) {
    if (p1.type !== 'prop') {
        throw new Error('not prop.');
    }
    if (p2.type !== 'prop') {
        throw new Error('not prop.');
    }

    return {
        type: 'prop', 
        subtype: 'equiv', 
        sub1: p1, 
        sub2: p2
    };
}

上から順番に否定、連言、選言、含意、同値の論理結合子によって組み立てられる数学的言明を作る関数です。

特に難しいことは何もしていません。

引数が適切なものでない場合には例外を投げます。

また、subtypeプロパティの値であるneg、conj、disj、imp、equivはそれぞれ否定、連言、選言、含意、同値の論理結合子によって組み立てられた数学的言明であることを示しています。

なお、sub、sub1、sub2プロパティにより、新たに作成されたオブジェクトの材料となったオブジェクトにアクセスできるようにしています。

プログラムによる数学的言明の作成

これで数学的言明をプログラムで作成することができるようになりましたので、適当な数学的言明を作成してみましょう。

たとえば、P1 → P2という言明は下のようにすれば作成できます。

var p1 = create_implication(create_proposition(1), create_proposition(2));

また、(P1 ∧ ￢P2) ∨ P3という言明は下のようにすれば作成できます（なお、(、)の使い方は普通の数式における場合と同じです）。

var p2 = create_disjunction(create_conjunction(create_proposition(1), create_negation(create_proposition(2))), create_proposition(3));

しかし、毎回プログラム上で数学的言明を作らなければならないのは面倒ですし、プログラム自体createから始まる関数の呼び出しの複雑な組み合わせとなるので分かりにくいです。

なので、単純なコマンドを呼び出すことで自由に数学的言明を組み立てていけるような仕組みを考えます。

コマンドによる数学的言明の作成

まず、math.jsというファイルに上で作成した関数を全て格納してください。

更に下のような数学的言明を表すオブジェクトをHTML形式で出力する関数を追加します。

function tohtml (obj) {
  if (obj.typr === 'prop') {
    if (obj.subtype === 'atom') {
      return 'P' + '<sub>' + obj.index + '</sub>';
    }
    else if (obj.subtype === 'neg') {
      return '( ' + '￢' + tohtml(obj.sub) + ' )';
    }
    else if (obj.subtype === 'conj') {
      return '( ' + tohtml(obj.sub1) + ' ∧ ' + tohtml(obj.sub2) + ' )';
    }
    else if (obj.subtype === 'disj') {
      return '( ' + tohtml(obj.sub1) + ' ∨ ' + tohtml(obj.sub2) + ' )';
    }
    else if (obj.subtype === 'imp') {
      return '( ' + tohtml(obj.sub1) + ' → ' + tohtml(obj.sub2) + ' )';
    }
    else if (obj.subtype === 'equiv') {
      return '( ' + tohtml(obj.sub1) + ' ↔ ' + tohtml(obj.sub2) + ' )';
    }
    else {
      throw new Error('not supported subtype.');
    }
  }
  else {
    throw new Error('not supported type.');
  }
}

そして、下のようなHTMLページを用意します。このHTMLページはmath.jsを保存したのと同じフォルダにmain.htmlというファイル名で保存することにしましょう。

<!DOCTYPE html>
<html lang="ja">
<head>
  <meta charset="utf-8">
  <title>形式化数学</title>
</head>
<body>
  <script src="asset/lib/vue-2.5.13/vue.min.js"></script>

  <div id="main">
    <input type="text" v-model="input" @keydown.enter="execute_command">
    <button @click="execute_command">実行</button>
    <div v-for="output in outputs" :key="output.id">
      <span v-html="output.html"></span>
    </div>
  </div>

  <script src="math.js"></script>
  <script src="main.js"></script>
</body>
</html>

また、上のHTMLページではVue.jsを利用しますのでVue.jsも準備してください。math.jsを保存したフォルダのassetフォルダのlibフォルダのvue-2.5.13フォルダにvue.min.jsファイルを格納します。

最後に、main.jsという下のような内容のJavaScriptファイルをmath.jsを保存したのと同じフォルダに用意します。

var id = 0;

var context = {
  pindex: 0,
  sindex: 0,
  ss: new Map()
};

function execute_command (context, command) {
  var cs = command.split(' ');

  if (cs[0] === 'prop') {
    context.pindex++;
    var p = create_proposition(context.pindex);

    add_object(context, p);

    return p;
  }
  else if (cs[0] === 'neg') {
    var objs = get_n_objects_from_args(context, 1, cs);
    var p = create_negation(objs[0]);

    add_object(context, p);

    return p;
  }
  else if (cs[0] === 'conj') {
    var objs = get_n_objects_from_args(context, 2, cs);
    var p = create_conjunction(objs[0], objs[1]);

    add_object(context, p);

    return p;
  }
  else if (cs[0] === 'disj') {
    var objs = get_n_objects_from_args(context, 2, cs);
    var p = create_disjunction(objs[0], objs[1]);

    add_object(context, p);

    return p;
  }
  else if (cs[0] === 'imp') {
    var objs = get_n_objects_from_args(context, 2, cs);
    var p = create_implication(objs[0], objs[1]);

    add_object(context, p);

    return p;
  }
  else if (cs[0] === 'equiv') {
    var objs = get_n_objects_from_args(context, 2, cs);
    var p = create_equivalence(objs[0], objs[1]);

    add_object(context, p);

    return p;
  }
  else {
    throw new Error('not supported command.');
  }
}

function add_object (context, obj) {
  context.sindex++;
  context.ss.set(context.sindex, obj);
}

function get_n_objects_from_args (context, n, cs) {
  check_num_arguments(cs, n);

  var objs = [];
  for (var i = 0; i < n; i++) {
    var idx = get_int_argument(cs[1 + i]);
    check_in_range(idx, context.sindex);
    var obj = context.ss.get(idx);
    objs.push(obj);
  }

  return objs;
}

function check_num_arguments (cs, num) {
  if (cs.length < num + 1) {
    throw new Error('missing argument.');
  }
}

function get_int_argument (arg) {
  var i = parseInt(arg);
  if (isNaN(i)) {
    throw new Error('not integer.');
  }
  return i;
}

function check_in_range (arg, max) {
  if (arg < 1 || arg > max) {
    throw new Error('out of range.');
  }
}

var vm = new Vue({
  el: '#main',
  data: {
    input: '',
    outputs: []
  },
  computed: {},
  methods:  {
    execute_command: function () {
      var command = this.input;
      this.input = '';

      try {
        var obj = execute_command(context, command);
        if (obj != undefined && obj != null) {
          id++;
          this.outputs.push({
            id: id,
            html: '[' + id + ']' + tohtml(obj)
          });
        }
      }
      catch (err) {
        id++;
        this.outputs.push({
          id: id,
          html: err.message
        });
      }
    }
  }
});

このファイルでは主にユーザーが入力したコマンドを解釈して適切な数学的言明を作成し、出力する処理を行っています。

また、作成された数学的言明にはそれぞれに識別するための番号が付与され、作成した数学的言明を参照するにはこの番号を使用します。

コマンドは下のようにしました。

• propコマンド・・・メタ変数を作成するコマンドです。引数はありません。自動的に新しいメタ変数が作成されます。
• negコマンド・・・否定の論理結合子による数学的言明を作成するコマンドです。引数を1つ取り、この引数が示す数学的言明を材料とする新しい数学的言明を作成します。
• conjコマンド・・・連言の論理結合子による数学的言明を作成するコマンドです。引数を2つ取り、この引数が示す数学的言明を材料とする新しい数学的言明を作成します。
• disjコマンド・・・選言の論理結合子による数学的言明を作成するコマンドです。引数を2つ取り、この引数が示す数学的言明を材料とする新しい数学的言明を作成します。
• impコマンド・・・含意の論理結合子による数学的言明を作成するコマンドです。引数を2つ取り、この引数が示す数学的言明を材料とする新しい数学的言明を作成します。
• equivコマンド・・・同値の論理結合子による数学的言明を作成するコマンドです。引数を2つ取り、この引数が示す数学的言明を材料とする新しい数学的言明を作成します。

たとえば、propコマンドを実行すると、下のような数学的言明が作成されます。

[1]P1

ここで、[、]で囲まれた数値は数学的言明の番号を表します。

この数学的言明を材料として新しい数学的言明を作成したい場合にはこの番号をコマンドの引数として指定します。

たとえば、neg 1コマンドを実行すると、下のような数学的言明が作成されます。

[2]( ￢P1 )

また、imp 1 2コマンドを実行すると、下のような数学的言明が作成されます。

[3]( P1 → ( ￢P1 ) )

このようにして、コマンドを使用して自由に数学的言明を作成することができます。

今回はここまでにしたいと思います。次回は数学的な議論の大きな部分を構成する証明について説明し、プログラム上で実装したいと思います。