2021-03-04

レーブの定理

「スマリヤンの決定不能の論理パズル（白揚社 2008年）」という本にレーブの定理がわかりやすく紹介されていたので、それを紹介したいと思います。
レーブの定理
任意の命題 $k,C$ について、もし4型の推論者が $BC\supset C$ と $k\equiv (Bk\supset C)$ を信じるならば、 $C$ を信じる。
ここで、 $Bk$ というのは、「命題 $k$ を信じている」という意味で、4型の推論者とは以下の推論規則に従う人です。
$(A1a)(p\equiv 1)\supset Bp$
$(A1b)Bp\wedge B(p\supset q)\supset Bq$
$(A2)B(Bp\wedge B(p\supset q)\supset Bq)$
$(A3)Bp\supset BBp$
$(A4)B(Bp\supset BBp)$
証明する前に補題を２つほど示します。
補題１
$B(p\supset(q\supset r))\supset B(Bp\supset(Bq\supset Br))$
証明　 $(1)B(B(p\supset q)\supset (Bp\supset Bq) )$ 　∵(A2)と同値

　　　 $(2)BB(p\supset q)\supset B(Bp\supset Bq)$ 　∵(1),(A1b)より

　　　 $(3)BB(p\supset (q\supset r) )\supset B(Bp\supset B(q\supset r) )$

　　　　　　∵(2)の $q$ を $q\supset r$ に置き換え

　　　 $(4)B( (B(q\supset r)\supset (Bq\supset Br) )$

　　　　　 $\supset ( (Bp\supset B(q\supset r) )\supset (Bp\supset (Bq\supset Br) ) ) )$

　　　　　　∵ $(Y\supset Z)\supset( (X\supset Y)\supset(X\supset Z) )$ の $X$ を $Bp$ , $Y$ を $B(q\supset r)$ ,

　　　　　　　 $Z$ を $(Bq\supset Br)$ に置き換え

　　　 $(5)B( (Bp\supset B(q\supset r) )\supset (Bp\supset (Bq\supset Br) ) )$ 　∵(1),(4),(A1b)より

　　　 $(6)B(Bp\supset B(q\supset r) )\supset B(Bp\supset (Bq\supset Br) )$ 　∵(5),(A1b)より

　　　 $(7)BB(p\supset (q\supset r))\supset B(Bp\supset (Bq\supset Br) )$ 　∵(3),(6)より

　　　 $(8)B(p\supset(q\supset r))\supset BB(p\supset(q\supset r))$ 　∵(A3)より

　　　　∴ $B(p\supset(q\supset r))\supset B(Bp\supset(Bq\supset Br))$ 　∵(7),(8)より

補題２（本では、補題１）
$B(p\supset (Bp\supset q) )\supset B(Bp\supset Bq)$
証明　 $(1)B(p\supset (Bp\supset q) )\supset B(Bp\supset (BBp\supset Bq) )$ 　∵補題１より

　　　 $(2)B(Bp\supset BBp)$ 　∵(4)より

　　　 $(3)B( (Bp\supset BBp)\supset ( (Bp\supset (BBp\supset Bq) )\supset (Bp\supset Bq) ) )$

　　　　　　∵ $(X\supset Y)\supset ( (X\supset (Y\supset Z) )\supset (X\supset Z) )$ の $X$ を $Bp$ , $Y$ を $BBp$ ,

　　　　　　　 $Z$ を $Bq$ に置き換え

　　　 $(4)B( (Bp\supset (BBp\supset Bq) )\supset (Bp\supset Bq) )$ 　∵(2),(3),(A1b)より

　　　　∴ $B(p\supset (Bp\supset q) )\supset B(Bp\supset Bq)$ ∵(1),(4),(A1b)より

ではレーブの定理を証明します。
レーブの定理
$B(BC\supset C)\wedge B(k\equiv (Bk\supset C))\supset BC$
証明　 $(1)B(k\equiv (Bk\supset C))\supset B(Bk\supset BC)$ 　∵補題２より

　　　 $(2)B( (Bk\supset BC\wedge BC\supset C)\supset (Bk\supset C))$

　　　　　　∵ $( (X\supset Y)\wedge (Y\supset Z))\supset (X\supset Z)$ の $X$ を $Bk$ , $Y$ を $BC$ ,

　　　　　　　 $Z$ を $C$ に置き換え

　　　 $(3)B(BC\supset C)\wedge B(k\equiv (Bk\supset C))\supset B(Bk\supset C)$ ∵(1),(2),(A1b)より

　　　 $(4)B(Bk\supset C)\wedge B( (Bk\supset C)\equiv k)\supset Bk$ 　∵(A1b)より

　　　 $(5)Bk\supset BBk$ 　∵(A3)より

　　　 $(6)BBk\wedge B(Bk\supset C)\supset BC$ 　∵(A1b)より

　　　　∴ $B(BC\supset C)\wedge B(k\equiv (Bk\supset C))\supset BC$ 　∵(3),(4),(5),(6)より

これで、レーブの定理が示せました。
実は、本はまだ半分までしか読んでないので、これがレーブの定理の全てなのかは分かりません。（まだ読んでないとこにも出てきていたので）
実際にはもっと詳しく書いてあるので、興味があったらぜひ読んでみてください。

2021-02-05

コラッツ予想 Part1

うごメモで書いたことを、一応ここに書き記します。
以下の整数関数C(x),D(x)を再帰的に定義する。（全てで定義されてるとは限らない）
法は以下全て２。
$C(1)=0$
$C(2x)=C(x)$
$C(x)=C(3x+1)+1(x\geq3)$
$D(1)=0$
$D(2x)=D(x)+1$
$D(x)=D(3x+1) (x\geq3)$

$x=2^p q+r$ とおくと、 $p\geq D(r)$ の時、
$C(2^p q+r)=\left\{C(3^{C(r)+\frac{p-D(r)}{2}} q+1)+C(r)+\frac{p-D(r)}{2} (p\equiv D(r)) \\ C(3^{C(r)+\frac{p-D(r)+1}{2}} q+2)+C(r)+\frac{p-D(r)+1}{2} (p \not\equiv D(r))\right.$
$D(2^p q+r)=\left\{D(3^{C(r)+\frac{p-D(r)}{2}} q+1)+p (p\equiv D(r)) \\ D(3^{C(r)+\frac{p-D(r)+1}{2}} q+2)+p (p \not\equiv D(r))\right.$
また、 $E(x)=D(x)-2C(x)$ とおくと、
$E(2^p q+r)=\left\{E(3^{\frac{p-E(r)}{2}} q+1)+E(r) (p\equiv E(r)) \\ E(3^{\frac{p -E(r)+1}{2}} q+2)+E(r)-1 (p \not\equiv E(r))\right.$
となる。
E(x)についてわかっていることは、
・正と負の値を取る
・E(1)からE(26)は正で、値が突出するE(27)は負
くらいです。それだけです。

2021-02-05

コラッツ予想 Part2

以下、 $a\equiv b (mod x)$ を $a\equiv_{x} b$ で表します。
$x_{n+1}=\left\{D(x_n)=\frac{x_n}{2} (x_n\equiv_2 0)\\ C(x_n)=\frac{3x_n+1}{2} (x_n\equiv_2 1)\right.$
$x_0=m$
$i$ 回目の偶奇を $a_i=0,1$ とおき、 $f_{a_i}(m)$ を
$f_{a_i}(m)=\left\{ D(m) (a_i=0)\\ C(m) (a_i=1) \right.$
とおけば、
$m\equiv_2 a_0 \\f_{a_0}(m)\equiv_2 a_1 \\ f_{a_1}\circ f_{a_0}(m)\equiv_2 a_2 \\ \ldots$
となります。
この論理積が有限の時は、（私のやり方で）一意にまとめられて、j番目までまとめると、
$m\equiv_2 a_0$
$m\equiv_4 a_0+2a_1$
$m\equiv_8 5a_0+2a_1+4a_2+4a_0a_1$
$m\equiv_{16} 5a_0+10a_1+4a_2+8a_3+4a_0a_1+8a_0a_2+8a_1a_2$
$m\equiv_{32} 21a_0+10a_1+20a_2+8a_3+16a_4+4a_0a_1+8a_0a_2+8a_1a_2$
$+16a_0a_3+16a_1a_3+16a_2a_3+16a_0a_1a_2$
$m\equiv_{64} 21a_0+42a_1+20a_2+40a_3+16a_4+36a_0a_1+8a_0a_2+8a_1a_2$
$+16a_0a_3+16a_1a_3+16a_2a_3+16a_0a_1a_2+32a_0a_4+32a_1a_4+32a_2a_4$
$+32a_3a_4+32a_0a_1a_3+32a_0a_2a_3+32a_1a_2a_3$
となっています。
一般化はできていませんが、合同式を無視してj=2,4の右辺のグラフを書くと、
f:id:mikuwaorenoyome:20131004050054p:plain

ちなみに、前回定義したC(n)のC(n)=C(3n+1)+1をC(n)=C(n+1)+1に変えたものをグラフに書くと、

どこか似てるような気が・・・

2021-02-05

コラッツ予想 Part3

$C_0=C_1=0\\C_{2n}=C_n\\C_{2n+1}=C_{2n+2}+1$
の母関数
$\displaystyle Q(x)=\sum_{k=0}^\infty C_kx^k$
を考えます。
以下の議論は、私の無知により多少不正確です。（つまり、母関数を扱ったことはありません）
$Q(x)=Q_0(x)+Q_1(x)$
$\displaystyle Q_0(x)=\sum_{k=0}^\infty C_{2k}x^{2k}$
$\displaystyle Q_1(x)=\sum_{k=0}^\infty C_{2k+1}x^{2k+1}$
と分けると、
$\displaystyle Q_0(x)=\sum_{k=0}^\infty C_{k}(x^2)^k=Q(x^2)$
$\displaystyle\begin{eqnarray}Q_1(x)&=&\sum_{k=0}^\infty (C_{2k+2}+1)x^{2k+1} \\ &=&\sum_{k=0}^\infty C_{2k+2}x^{2k+1}+\sum_{k=0}^\infty x^{2k+1} \\&=&\frac{Q_0(x)}{x}+\frac{x}{1-x^2} \end{eqnarray}$
また、
$\displaystyle \begin{eqnarray} Q_0(x)&=&\sum_{k=0}^\infty (\frac{(-1)^k+1}{2})C_kx^{k} \\ &=&\frac{1}{2}(\sum_{k=0}^\infty (-1)^kC_kx^{k}+\sum_{k=0}^\infty C_{k}x^{k}) \\ &=&\frac{Q(x)+Q(-x)}{2} \end{eqnarray}$
になります。Q1を無視すれば、
$Q(x^2)=\frac{Q(x)+Q(-x)}{2}$
単純に、 $Q(x)=\log f(x)$ とあ思いましたが、
$(f(x^2))^2=f(x)f(-x)$ になり、私には力不足のようです。

2020-09-29

ポリオミノの平面充填

数学

1種類のポリオミノの平面充填を考える。

定義

ミノ

$m:\in\mathbb{Z}^2$

ポリオミノ

$m_i\in\mathbb{Z}^2\\i\neq j\rightarrow m_i\neq m_j\\n\in\mathbb{N}\\M:=\{m_1,\cdots,m_n\}$

平行移動

$p:\in\mathbb{Z}^2$

ミノの平行移動

$m+p:=(m_x+p_x,m_y+p_y)$

ポリオミノの平行移動

$M+p:=\{m_1+p,\cdots,m_n+p\}$

平行移動の組

$p_n\in\mathbb{Z}^2\\P:=(p_n)_{n=1}^\infty$

ポリオミノの平行移動の組

$M+P:=(M+p_n)_{n=1}^\infty$

ポリオミノの平面充填可能性

Mが平面充填可能 $:\leftrightarrow\exists P,M+P=\mathbb{Z}^2$

2019-11-12

オセロ必勝法 Part4

プログラミング

(defun Othello ()
  (setq table nil)
  (setq sq 8)
  (setq r nil)
  (defun initable ()
    (defun initableat ()
      (cond ((not table) (setq table '((0 0))))
            ((= (caar table) (1- sq)) (setq table (push `(0 ,(1+ (cadr (car table)))) table)))
            (t (setq table (push `(,(1+ (caar table)) ,(cadr (car table))) table)))))
    (defun nest (f n)
      (if (zerop n) nil
        (progn (funcall f)
               (nest f (1- n)))))
    (nest 'initableat (* sq sq))
    (setq table (reverse table))
    (setq table (mapcar (lambda (x) (list x 0)) table)))
  (defun setdisk (x y disk)
    (setq table (mapcar (lambda (z) (cond ((and (eq (caar z) x)
                                                (eq (cadr (car z)) y))
                                           (list (list x y) disk))
                                          (t z)))
                        table)))
  (defun subsetdisk (x y disk)
    (setq subtable (mapcar (lambda (z) (cond ((and (eq (caar z) x)
                                                   (eq (cadr (car z)) y))
                                              (list (list x y) disk))
                                             (t z)))
                           subtable)))
  (defun begintable ()
    (setq table nil)
    (initable)
    (setdisk 1 1 t)
    (setdisk 2 1 nil)
    (setdisk 1 2 nil)
    (setdisk 2 2 t)
    (display))
  (defun neighbor (x)
    (cond ((= x 0) '(-1 -1))
          ((= x 1) '(0 -1))
          ((= x 2) '(1 -1))
          ((= x 3) '(-1 0))
          ((= x 4) '(1 0))
          ((= x 5) '(-1 1))
          ((= x 6) '(0 1))
          ((= x 7) '(1 1))))
  (defun getdisk (x y)
    (cadr (elt table (+ (* sq y) x))))
  (defun turnover (x y color)
    (let ((dir nil)
          (flag nil)
          (i 0)
          (subtable table)
          (nei 8))
      ;(if (not (checkturnover x y color)) '(cant put here)
        (progn (setdisk x y color)
               (setq subtable table)
               (defun turnoverat (x y color dir flag)
                 (let ((neix (+ x (car (neighbor dir))))
                       (neiy (+ y (cadr (neighbor dir)))))
                   (if (or (> 0 (+ (* sq neiy) neix))
                           (<= (* sq sq) (+ (* sq neiy) neix))
                           (eq (getdisk neix neiy) 0))
                       (setq subtable table)
                     (if (not flag)
                         (if (eq (getdisk neix neiy) (not color))
                             (progn (subsetdisk neix neiy color)
                                    (turnoverat neix neiy color dir t)))
                       (cond ((eq (getdisk neix neiy) 0) (setq subtable table))
                             ((eq (getdisk neix neiy) (not color))
                              (progn (subsetdisk neix neiy color)
                                     (turnoverat neix neiy color dir t)))
                             ((eq (getdisk neix neiy) color) (setq table subtable)))))))
               (while (< i nei)
                 (turnoverat x y color i flag)
                 (setq i (1+ i))))
        ;)
    )
                                        ;(display)
    table)
  (defun checkturnover (x y color)
    (let ((dir nil)
          (flag nil)
          (i 0)
          (subtable table)
          (nei 8)
          (checkflag nil))
      (if (eq (getdisk x y) 0)
          (progn (defun checkturnoverat (x y color dir flag)
                   (let ((neix (+ x (car (neighbor dir))))
                         (neiy (+ y (cadr (neighbor dir)))))
                     (if (or (> 0 (+ (* sq neiy) neix))
                             (<= (* sq sq) (+ (* sq neiy) neix))
                             (eq (getdisk neix neiy) 0))
                         nil
                       (if (not flag)
                           (if (eq (getdisk neix neiy) (not color))
                               (checkturnoverat neix neiy color dir t))
                         (cond ((eq (getdisk neix neiy) 0))
                               ((eq (getdisk neix neiy) (not color))
                                (checkturnoverat neix neiy color dir t))
                               ((eq (getdisk neix neiy) color) (setq checkflag t)))))))
                 (while (< i nei)
                   (checkturnoverat x y color i flag)
                   (setq i (1+ i)))))
      checkflag))
  (defun displaycolor ()
    (mapcar (lambda (x) (cond ((eq (cadr x) 0) 0)
                              ((eq (cadr x) nil) '●)
                              ((eq (cadr x) t) '○)
                              (t '.)))
            table))
  (defun cutoff (table)
    (let ((i nil)
          (j nil))
      (defun cutoffat (table i j)
        (cond ((eq i nil) (progn (setq i 0)
                                 (setq j 0)
                                 (setq p nil)
                                 (setq q nil)
                                 (cutoffat table i j)))
              ((< i sq) (progn (push (car table) p)
                               (cutoffat (cdr table) (1+ i) j)))
              ((< j sq) (progn (push (reverse p) q)
                               (setq i 0)
                               (setq p nil)
                               (cutoffat table i (1+ j))))
              (t (reverse q))))
      (cutoffat table i j)))
  (defun displaynewline (table)
    (if (eq table nil) nil
      (progn (setq r (concat r (format "%s" (car table)) (string ?\n)))
             (displaynewline (cdr table))))
    r)
  (defun display ()
    (setq r (string ?\n))
    (displaynewline (cutoff (displaycolor))))
  (defun count ()
    (let ((sumb 0)
          (sumw 0))
      (defun countat (table)
        (cond ((eq table nil) nil)
              ((eq (cadr (car table)) nil) (progn (setq sumb (1+ sumb))
                                                  (countat (cdr table))))
              ((eq (cadr (car table)) t) (progn (setq sumw (1+ sumw))
                                                (countat (cdr table))))
              (t (countat (cdr table)))))
      (countat table)
      (cond ((= sumb sumw) 'draw)
            ((> sumb sumw) nil)
            ((< sumb sumw) t))))
  (defun end (table)
    (catch 'loop
      (let ((j 0))
        (while (< j sq)
          (let ((i 0))
            (while (< i sq)
              (if (or (checkturnover i j nil)
                      (checkturnover i j t))
                  (throw 'loop nil))
              (setq i (1+ i))))
          (setq j (1+ j))))
      t))
  (defun strategy (table turn)
    (if (end table) (count)
      (catch 'loop
        (let ((j 0)
              (i 0)   
              (win (not turn))
              (flag nil))
          (while (< j sq)
            (while (< i sq)
              (if (checkturnover i j turn)
                  (let ((x (strategy (turnover i j turn) (not turn))))
                    (cond ((eq turn x)
                           (throw 'loop turn))
                          ((eq 'draw x)
                           (setq win 'draw)))
                    (setq flag t)))
              (setq i (1+ i)))
            (setq i 0)
            (setq j (1+ j)))
          (if (not flag)
              (strategy table (not turn))
            win))))))

というわけで、プログラムは出来たのですが、計算量が多すぎます。
多く見積もっても、10^80分かかります。
どうしたものか・・・

人生の役に立たない数学

最近買った本

レーブの定理

コラッツ予想 Part1

コラッツ予想 Part2

コラッツ予想 Part3

ポリオミノの平面充填

定義

オセロ必勝法 Part4