blog.鶯梭庵

二〇一一年神無月廿八日金曜日

■ 「折り紙公理」の形式化・その２ [/origami]

その１で、折り紙公理系の公理を２つ挙げた。しかし、公理系と名乗るからには、公理から形式的な推論によって定理が証明できなければ意味がない。そこで、この２つの公理を形式化してみたい。具体的には、述語論理の記号と等号「=」、そして「直線 l で折ったときに点 a と点 b が重なる」という述語（F(l, a, b) と書く）だけを使って、これらの公理を記述する。

（述語論理の記号は以下の通り。¬A は「A ではない」、A∧B は「A かつ B」、A∨B は「A または B」、∀x(A(x)) は「すべての x について A(x)」、∃x(A(x)) は「ある x について A(x)」。）

実は、この述語 F(x, y, z) は非常に便利で、平面幾何学のさまざまな概念を表すことができる。たとえば、「点 a が直線 l の上にある」は F(l, a, a) と表すことができる。したがって、「直線 l で折ったときに点 a が直線 m の上に乗る」は ∃b(F(l, a, b)∧F(m, b, b)) と書くことができる。

また、「直線 l と m が垂直」は ∃a∃b(¬(a = b)∧F(l, a, b)∧F(m, a, a)∧F(m, b, b)) と書ける。これを P(l, m) と略記する。「直線 l と m が平行」は、「l と m の両方に垂直な直線が存在する」と考えれば、∃n(P(l, n)∧P(m, n))と書ける（正確に言えば、この式が表しているのは「l と m は等しいか平行」である）。

すると、２つの公理は次のように書くことができる。

・∀l∀m(∃n(P(l, n)∧P(m, n))∨∃a(F(l, a, a)∧F(m, a, a)))

・∀a∀b∀l∀m(∃n(P(l, n)∧P(m, n))∨∃c∃d∃n(F(n, a, c)∧F(l, c, c)∧F(n, b, d)∧F(m, d, d)))

この２つの公理だけでは大した公理系にならないが、それでも興味深いことが証明できる。

いま、a、b、l、m を所与とし、F(m, b, b) を仮定しよう。すると、2番目の公理から、

∃n(P(l, n)∧P(m, n)∧F(m, b, b))∨∃c∃d∃n(F(n, a, c)∧F(l, c, c)∧F(n, b, d)∧F(m, d, d)∧F(m, b, b))

が言える。ここで、(b = d)∨¬(b = d) であることから、

∃n(P(l, n)∧P(m, n)∧F(m, b, b))∨∃c∃d∃n(F(n, a, c)∧F(l, c, c)∧F(n, b, d)∧F(m, d, d)∧F(m, b, b)∧(b = d))∨∃c∃d∃n(F(n, a, c)∧F(l, c, c)∧F(n, b, d)∧F(m, d, d)∧F(m, b, b)∧¬(b = d))

であり、

∃n(P(l, n)∧P(m, n))∨∃c∃n(F(n, a, c)∧F(l, c, c)∧F(n, b, b))∨∃c∃n(F(n, a, c)∧F(l, c, c)∧P(n, m))

が言える。非常に長い式で分かりにくいが、「∨」で３つの式がつながっており、それぞれ「l と m が等しいか平行」、「a を l の上に乗せ、b を通る n を折る」、「a を l の上に乗せ、m と垂直な n を折る」と解釈できることに注意してほしい。

以前、「２つの点 a、b と平行でない２本の直線 l、m があり、b が m の上にあるとき、『a を l の上に乗せ、b を m の上に乗せるように折る』という折り方は、『a を l の上に乗せ、b を通る直線を折る』か『a を l の上に乗せ、m と垂直に折る』のいずれかである」ということを、三角関数を使って証明したが、これを、ユークリッド幾何学を前提とせずに、公理だけから証明できたことになる。

その３に続く。

[この記事にコメントを書く。] [このカテゴリをまとめて読む。] [最新の記事を読む。]

blog.鶯梭庵

二〇一一年神無月廿八日金曜日

■ 「折り紙公理」の形式化・その２ [/origami]

最近のツイート

カテゴリ

最新記事

blog.鶯梭庵

二〇一一年 神無月 廿八日 金曜日

■ 「折り紙公理」の形式化・その２ [/origami]

最近のツイート

カテゴリ

最新記事

二〇一一年神無月廿八日金曜日