二〇一一年 霜月 廿三日 水曜日
■ 「折り紙公理」の形式化・その３ [/origami]
その２で、
∀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)→(∃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))))
が証明できることを示した。この定理の意味するところは、「２つの点 a、b と平行でない２本の直線 l、m があり、b が m の上にあるとき、『a を l の上に乗せ、b を m の上に乗せるように折る』という折り方は、『a を l の上に乗せ、b を通る直線を折る』か『a を l の上に乗せ、m と垂直に折る』のいずれかである」ということだ。
同様に、a、b、l、m を所与とし、F(l, a, a)∧F(m, b, b) を仮定すると、
∃n(P(l, n)∧P(m, n)∧F(l, a, a)∧F(m, b, b))∨∃c∃d∃n(F(n, a, c)∧F(l, c, c)∧F(n, b, d)∧F(m, d, d)∧F(l, a, a)∧F(m, b, b))
が言え、(b = d)∨¬(b = d) であることから、
∃n(P(l, n)∧P(m, n))∨∃c∃n(F(n, a, c)∧F(l, c, c)∧F(l, a, a)∧F(n, b, b))∨∃c∃n(F(n, a, c)∧F(l, c, c)∧F(l, a, a)∧P(n, m))
が言え、(a = c)∨¬(a = c) であることから、
∃n(P(l, n)∧P(m, n))∨∃n(F(n, a, a)∧F(n, b, b))∨∃n(P(n, l)∧F(n, b, b))∨∃n(F(n, a, a)∧P(n, m))
が言える。つまり、
∀a∀b∀l∀m((F(l, a, a)∧F(m, b, b))→(∃n(P(l, n)∧P(m, n))∨∃n(F(n, a, a)∧F(n, b, b))∨∃n(P(n, l)∧F(n, b, b))∨∃n(F(n, a, a)∧P(n, m))))
が証明できる。これが意味するところは、「２つの点 a、b と平行でない２本の直線 l、m があり、a が l の上にあり、b が m の上にあるとき、『a を l の上に乗せ、b を m の上に乗せるように折る』という折り方は、『２つの点を通る直線を折る』か『１つの点を通り１本の直線と垂直に折る』のいずれかである」ということだ。
その４に続く。
最近のツイート
[もっと読む]
カテゴリ
[/language] (74)
[/links] (206)
[/mac] (97)
[/music] (36)
[/origami] (375)
[/this_blog/ajax] (7)
[/this_blog/blosxom] (4)
[/this_blog/history] (12)
[/this_blog/perl] (9)
最新記事
◇ 検察の「暴走」・その２ [/links]
◇ 検察の「暴走」・その１ [/links]
◇ 折り紙ろうそく [/origami]
◇ 家庭用灌漑設備 [/language]
◇ Weekend Japanology に出演 [/origami]
◇ 算数における掛け算について [/links]
◇ 「折り紙公理」の形式化・その６ [/origami]
◇ 「折り紙公理」の形式化・その５ [/origami]
◇ 折り紙ティーセット [/origami]
◇ 「折り紙公理」の形式化・その４ [/origami]
◇ 「折り紙公理」の形式化・その３ [/origami]
◇ ジョセフ・ウーさんのインスタレーション [/origami]
◇ 「折り紙公理」の形式化・その２ [/origami]
◇ 「折り紙公理」の形式化・その１ [/origami]
◇ Ear-igami [/origami]