🚀 go-pugleaf

$@$D$E$-$N3^(J(ryu@sys.titech.ac.jp)$@$G$9!#(J

In article <SATOSHI.92Nov5173636@whale.ryukoku.ac.jp> satoshi@whale.ryukoku.ac.jp (Satoshi Kobayashi) writes:
 | |$@$H$J$i$J$$(JV^($@&8(J)$@$NMWAG$OL58B(J$@$K$"$j$c$7$^$;$s$+!"$C$F$$$&0UL#$J$s$G$9!#(J
 |
 |$@$=$l$O$b$A$m$sL58B$K$"$j$^$9!#$7$+$7!"$=$l$O!"O@M}$,D>(J$@4Q<g5A(J
 |$@E*$K$J$C$F$$$k$3$H$H$O2?$N4X78$b$"$j$^$;$s!#<B:]!"%V!<%kBe?t(J
 |$@CM$N=89g$N@$3&(JV^(B)($@&8$,$?$^$?(J$@$^40Hw%V!<%kBe?t(J B $@$K$J$C$F$$(J
 |$@$k>l9g$r9M$($F2<$5$$!#$b$A$m$s!"(JB $@$,M-8B$@$H$D$^$i$J$$$N$G$3(J
 |$@$3$G$O(J$@L58B$N>l9g$r9M$($^$9!#(J)$@$O!"8EE5O@M}$K4p$E$/=89gO@(J ZFC 
 |$@$N%b%G%k$K$J$C$F$$$^$9$,!"$3$N%b%G%k$r30$+$i(J$@8+$?$i!"(J
 |[a \in 2] $@!b(J 0 $@$H$J$k(J a $@$O$$$/$i$G$b$"$j$^$9!#$@$+$i$H$$$C$F!"(J
 |$@8EE5O@M}$G$O(J 2 $@$N85$,L58B(J$@$K$"$k!"$J$s$F8@$o$J$$$G$7$g$&!#(J

$@$b$A$m$s$G$9!#8EE5O@M}$G$O#1$N$_$,!V@5$7$$!W$7!V@5$7$$$+@5$7$/$J$$$+(J$@!W(J
$@$O>o$K@5$7$$$N$G$9$+$i$M!#(J
Ea = 1 $@$H$J$i$J$$$b$N$b4^$a$F9M$($k!"$F$3$H$OD>4Q<g5A$H$O4X78$J$$$s$G(J
$@$9(J$@$+!)(J

 |$@%b%G%k$NCf$G8+$F2?8D$"$k$+$H$$$&$N$H!"%b%G%k$r30$+$i8+$?;~2?(J
 |$@8D$K8+$($k$+!"$H$$$&$N$,0lHL$K(J$@$O0[$J$k$N$O!"%b%G%k$NM}O@$K$*(J
 |$@$$$F$OA4$/Ev$?$jA0$N$3$H$G!"IT;W5D$G$b$J$s$G$b$J$$$3$H$G$9!#(J

$@$^$"!"(J$@%9%3!<%l%`$N5UM}$J$s$+$O$=$l$,5UM}$G$"$k$C$F$3$H$,!"5UM}$J$s$@$H(J
$@$O;W$$$^$9!#(J
$@$7$+$7C]Fb30;K$N%b%G%k$N(J$@Cf$G$O%b%G%k$NCf$G$b30$+$i8+$F$b0lCW$7$F$$$k$H(J
$@;W$C$?$s$G$9$,!#!J$3$3$G>e$N<ALd$KLa$kLu$G$9!K(J

 | |$@$G(J$@$b!"@P86$5$s$N@bL@$O$=$&$$$&OC$7$G$O$J$$$h$&$G$9$,!#(J
 |
 |$@$b$A$m$s!"$=$&$$$&OC$G$O$J$$$G$9$M!#(J

$@@P86$5(J$@$s$N8@$&!V%U%!%8!<$J!W$C$F$$$&$N$K$&$^$$6q9g$KA46u4V$H$J$i$J$$%*!<(J
$@%W%s%;%C%H$,BP1~$7$F$?$iLLGr$+$C$?(J$@$N$K$J!"$C$F$$$&0UL#$G$9!#(J

 | | |>not(A) or not(not(A)) $@$H(J A or not(A) $@$O0c$&$b$N$G$O$J$+$C$?$s$G$9$+(J$@!)(J
 | | |
 | | |  $@0c$&$H$$$&$N$,D>4Q<g5A$NN)>l$J$N$G$9$M!#$G!"$3$N5?LdId$O2?$r$*J9$-$K(J
 | | |$@$J$j$?$$(J$@$N$G$7$g$&!#(J
 | |
 | |$@D>4Q<g5A$G$O(J not(not(A)) -> A $@$,F3$1$^$;$s!#$=$lL5$7$G!"(J
 | |not(A) or not(not(A)) -> A or not(A) $@!JJX59>e(J[1]$@$H$7$^$9!K(J
 | |$@$rF3$/$3$H$,$G$-$?$C$1!)(J
 | |$@$H!"$$$&5?Ld$G$9!#(J
 |
 |$@$G$-(J$@$^$;$s!#(J

$@$"!"$d$C$Q$j!#(J

 | |[1] $@$,$$$($J$$$N$J$i$P!"(Jnot(A) or not(not(A)) $@$,0lHL$K=P$F$-$?$H$7$F$b(J
 | |$@JL$K:$$i$J$$$+$i$G$9!#(J
 |
 |$@$=$s$J$3$H$"$j$^$;$s!#:$$j$^$9!#$J$<$J$i!"(J
 |  $@!VG$0U$N(J A $@$K$D$$$F(J not(A) or not(not(A))$@!W(J
 |$@$bD>4Q<g5AO@M}$K$*$$$FG'$a$k$3$H$N$G$-$J$$(J principle $@$@$+$i(J
 |$@$G$9!#GSCfN'$h$j(J$@$b<e$$(J principle $@$G$9$1$I$M!#GSCfN'$+$iF3$+(J
 |$@$l$k(J principle $@$G!"GSCfN'$h$j$O<e$$$1$l$I$b!"G'$a$k$H$^(J$@$:$$(J 
 |principle $@$OB>$K$b$?$/$5$s$"$j$^$9!#(J

$@$J$k$[$I!"JY6/$K$J$j$^$9!#$F!"$3$H$O(J
$@!VG$0U$N(J A $@$K$D$$$F(J not(A) or not(not(A))$@!W(J
$@$O(JLJ$@$G>ZL@$G$-$J$$$3$H$,>ZL@$5$l$F$$$k$s$G$9$+!)(J
$@!t>ZL@$7$h$&$H$7$F%I%D%\$K$O(J$@$^$C$?$s$G$9$,!#(J

 | |$@!V$3$NK\!W$OK\Ev$ND>4Q<g5A$NJ}!J@P86$5$s!)!K$+$i8+$?$i!"2?$8$c%3%j%c!"$C(J
 | |$@$F(J$@$$$&$b$s$@$H;W$$$^$9!#(J
 |
 |$@8=:_!"K\Ev$K!V<+J,$N<g5A!W$H$7$FD>4Q<g5AE*?t3X$r$d$C$F$$$k?M(J
 |$@$O$[$H$s$I(J$@$$$^$;$s!#(J(3$@?M$0$i$$$H$$$&@b$"$j!#(J)$@BgH>$N?M$OLLGr(J
 |$@$$$+$i8&5fBP>]$H$7$F$d$C$F$$$k$N$G$9!#@P86$5$s$b!V(J$@K\Ev$ND>4Q(J
 |$@<g5A$N?M!W$G$O$J$$$H;W$$$^$9!#>/$J$/$H$b!V695A$N(J intuitionism
 |(Brouwer $@$H$=$NDo;RC#$NN.(J$@57$ND>4Q<g5AE*?t3X(J)$@!W$r?.Jt$7$F$$$?$j$O(J
 |$@$7$J$$$H;W$$$^$9!#;d$bC1$J$k8&5fBP>]$H$7$F8+$F$$$^$9!#$@$+$i(J$@!"(J
 |$@!V2?$8$c%3%j%c!W$H$O;W$$$^$;$s!#(J

$@;d$O!V2?$8$c%3%j%c!W$H;W$C$?$s$G$9$h!#(J
$@$@$C$F@5B'$JO@M}<0(JA$@$KBP(J$@$7$F!"0z?t$,!"!V@5$7$$!W=89g$@$C$?$i!"(J
[not A or A] = 1
$@$K$J$C$F$$$^$9$b$N!#(J

$@$=$l$KHf$Y$?$i(J
$@!VG$0U$N(J A $@$K$D$$$F(J not(A) or not(not(A))$@!W(J
$@$J$s$F%I%*%C$F$3$H$J$$!"$H;W$$$^$;$s$+!)(J

$@$@$+$i!VD>4Q<g5AE*=89gO@(J$@!W$O<B$O!VGSCfN)$NFHN)@-!W$J$N$+$bCN$l$J$$!"$J(J
$@$s$F;W$C$F$$$k$s$G$9$,!"E*30$l$G$7$g$&$+!)(J