🚀 go-pugleaf

$B>.NSAo(B@$BN6C+Bg3X$G$9!#(B

$B$b$N$9$4$/CY$$%U%)%m!<$K$J$k$N$G!"5$$,0z$1$k$N$G$9$,!"8m2r$,9-$^$k$H$$(B
$B$1$J$$$N$G!">/$7$@$1=q$-$^$9(B$B!#(B

In article <DHrHEt.LBA@ulis.ac.jp> hiraga@ulis.ac.jp (Yuzuru Hiraga) writes:

 |$BGXM}K!!JH]DjE*GXM}(B$BK!!K$O0l<o$N!V>C5nK!!W$H9M$($k$3$H$,$G$-$^$9!#(B
 |$BHH:aA\::$G(B A, B $B$N$$$:$l$+!J0lJ}$@$1$,!KHH?M$G$"$k$3(B$B$H$O(B
                              ^^^^^^^^^^
$B!V0lJ}$@$1$,!W$H$$$&2>Dj$OITMW$G$9$M!#(B

 |$B@dBP3N<B$@$H$7(B$B$^$9!J$3$NE@$,=EMW$G$9!K!#(B
 |A $B$,HH?M$G$"$kD>@\>Z5r$,$"$l$PLdBj$J$$$N$G$9$,!"$=$&$G$J$$>l9g$G$b!"(B
 |$B!V(BB $B$OHH?M$G$O$"$j$($J$$!J%"%j%P%$$,$"$k$J$I!K!W$H$$$&$3$H$r<($;$l$P!"(B
 |$B$=$3$+$i(B A $B$,HH?M$G$"$k$H4V@\E*(B$B$K7kO@$E$1$i$l$^$9!#(B
 |$B$&$k$5$/8@$($P!"!V(BB $B$,HH?M$G$"$k$H$9$k$H!J%"%j%P%$$,$"$k$3$H$H!K(B
 |$BL7=b$,@8$8$k(B$B!"$@$+$i(B B $B$OHH?M$G$O$"$j$($J$$!"$9$k$H(B A, B $B$I$A$i$+$,(B
 |$BHH?M$G$"$k$N$O3N$+$J$N$@$+$i!"(BA $B$,HH?M$G$7$+(B$B$"$j$($J$$!W$H$$$&$3$H$G!"(B
 |$B$3$l$J$iGXM}K!$N7A<0$HId9g$7$^$9!#(B

$B$3$N@bL@$OITE,@Z$@$H;W$$$^$9!#$J$<$J(B$B$i!">e$N?dO@$K$OGXM}K!$OA4$/I,MW$J(B
$B$$$+$i$G$9!#K\Mh$N0UL#$G$NGXM}K!$,I,MW$G$J$$$@$1$G$J$/!"3{$5$s$,8@(B$B$&=j$N(B
$B9NDjE*$JGXM}K!$5$($bI,MW$G$O$"$j$^$;$s!#(B

$B>e$N?dO@$G$O!"!V(BA $B$,HH?M$G$"$k!W$r(B P $B$H$7!"!V(BB $B$,HH?M(B$B$G$"$k!W$r(B Q $B$H$9(B
$B$k$H!"(B(P or Q) $B$H(B not Q $B$+$i(B P $B$rF3$$$F$$$^$9$,!"(B
((P or Q) and (not Q)) -> P $B$O<B:](B$B$K$OD>4Q<g5AO@M}$NCf$G<!$N$h$&$K$7$F>Z(B
$BL@$G$-$F$7$^$$$^$9(B:

$B:#!"(BP or Q $B$G(B not Q $B$@$H$7$F!"(BP $B$rF3$-$^$7(B$B$g$&!#(BP or Q $B$h$j!"(BP $B$+(B Q $B$+(B
$B$G>l9gJ,$1$9$k$3$H$,$G$-$^$9(B(or $B$N(B elimination rule)$B!#(B
  (1) P $B$N>l9g!#$b(B$B$A$m$s!"(BP $B$,F3$1$^$9!#(B
  (2) Q $B$N>l9g!#$3$N;~$O!"(Bnot Q $B$HL7=b$7$^$9!#L7=b$+$i$O2?$G$bF3$1$k$H(B
  $B$$$&(Brule($BL7=b$N(B elimination)$B$K$h$j!"(BP $B$,F3$1$^$9!#(B
$B7k6I!"$I$A$i$N>l9g$G$b(B P $B$,F3$1$?$N$G!"(BOK$B!#(B

$B$3$N>ZL@$r(B$B8+$k$H!"(Bor $B$K4X$9$k>l9g$o$1$H!"L7=b$+$i2?$G$b=P$k!"$H$$$&$3(B
$B$H$7$+;H$C$F$$$^$;$s!#GXM}K!$OITMW$G$9!#(B

$BD>4Q<g5AO@M}>e$G$O!"GXM}K!$OGSCfN'(B(P or not P $B$J$k(Baxiom scheme)$B$HF1CM(B
$B$G$9$+$i!"GXM}K!$O(B P $B$+(B not P $B$+$G>l9gJ,$1$9$k$3$H$r>o$K2DG=$K$9$kLr3d(B
$B$r;}$C$F$$$k$H9M$($k$3$H$,$G$-$^$9!#>e$N$h$&$J!V>C5nK!!W$O>l(B$B9gJ,$1$,$G(B
$B$-$F$7$^$C$?$"$H$G$=$N$&$A$N$$$/$D$+$N>l9g$r$D$V$7$F9T$/$H$$$&$N$G$9$+(B
$B$i!"Lr3d$,A4A30c$&$N(B$B$G$9!#(B

$B$b$C$H$b!"GXM}K!$+$iL7=b$N(B elimination $B$N5,B'$rF3$/$3$H$,$G$-$^$9$+$i!"(B
$BGXM}K!$,$"$l$P!">e$N$h(B$B$&$J!V>C5nK!!W$N?dO@(B*$B$b(B*$B2DG=$K$J$j$^$9!#$7$+$7!"(B
$BGXM}K!$,$J$/$F$b!">e$N!V>C5nK!!W$O2DG=$G$9!#(B

$BD>4Q<g(B$B5AO@M}$+$i$5$i$KL7=b$N(B elimination $B$b$H$j$N$>$$$F$7$^$C$?O@M}$H(B
$B$7$F!":G>.O@M}$H$$$&$N$,$"$j$^$9!#:G>.(B$BO@M}>e$G$O!"GXM}K!$HGSCfN'$OF1Ey(B
$B$G$J$/!"GSCfN'$HL7=b$N(B elimination $B$r9g$o$;$k$HGXM}K!$,=P$F$-$^$9!#$^(B
$B$?!"5U$K!"GXM}K!$+$iGSCfN'$HL7=b$N(B elimination $B$rF3$/$3$H$,$G$-$^$9!#(B
$B:G>.O@M}$KGXM}K!$r2C$($k$H8EE5(B$BO@M}$K$J$k$N$G$9$,!":G>.O@M}$KGSCfN'$r2C(B
$B$($F$b8EE5O@M}$K$J$j$^$;$s!#(B

$B>e$N(B((P or Q) and (not Q)) -> P $B$H$$$&(B scheme $B$O!":G>.O@M}>e$GL7=b$N(B 
elimination $B$HF1Ey$G$9!#(B

$B$J$*!"!V(BB $B$,HH?M$G$"$k$H$9$k$H!J%"%j(B$B%P%$$,$"$k$3$H$H!KL7=b$,@8$8$k!"$@(B
$B$+$i(B B $B$OHH?M$G$O$"$j$($J$$!W$H$$$&=j$G3{$5$s$,8@$&=j$N9NDjE*$JGXM}(B$BK!$r(B
$B;H$&$N$G$O$J$$$+!"$H8@$o$l$k$+$bCN$l$^$;$s!#3N$+$K$o$6$H;H$*$&$H;W$($P(B
$B;H$($k$o$1$G$9$,!"$=$N>l9g(B$B!"(Bnot Q $B$r(B introduce $B$7$?$"$H$G$9$0$K$=$l$r(B 
eliminate $B$9$k!"$H$$$&%`%@$J?dO@$r$7$F$$$^$9!#<B:]$K$O!"(B$B$=$N$h$&$J9NDj(B
$BE*$JGXM}K!$N%9%F%C%W$OITMW$G$9!#$-$A$s$H8@$&$H!"(B
  (a) P or Q $B$,F3$1$F!"(B
  (b) Q $B$r2>Dj(B$B$9$l$PL7=b$,F3$1$k$H$-!"(B
P $B$,F3$1$k!"$H$$$&$N$O!"9NDjE*$JGXM}K!$bH]DjE*$JGXM}K!$b;H$o$:$K<($;$k(B
derived rule $B$G$9!#(B

 |$B!V(B2 $B$NJ?J}:,!W$,Nc$H$7$FITE,@Z$H$$$&$N$O$*Fs?MJ}$,$9$G$K=R$Y$i$l$F$$$k$h$&$K!"(B
 |$B!V(B$BM-M}?t$G$O$J$$!W$3$H$r<($7$?$@$1!J>e$N!V(BB $B$,HH?M$G$J$$!W$3$H$,(B
 |$B$o$+$C$?$@$1!K$H$$$&E@$K$"$j$^$9!#(B
 |$B$5$i$KFM$C9~$`$H!"(B
 |  * $B!V#2$NJ?J}:,!W$H$$$&?t!J<B?t!K$O3N$+$KB8:_$9$k(B
 |  * $BL5M}?t$H$$$&$b$N$,!J<B(B$B?t$H$7$F!K3N$+$KB8:_$9$k(B
 |  * $BM-M}?t$G$J$1$l$P!JM-M}?t$G$J$$<B?t$J$i$P!KL5M}?t$G$"$k(B
 |$B$H$$$C$?$3$H$r(B$B3NG'$9$kI,MW$,$"$j$^$9!#(B

$B!VL5M}?t$H$$$&$b$N$,(B($B<B?t$H$7$F(B)$B3N$+$KB8:_$9$k!W$H$$$&$3$H$rA0$b$C$F3N(B
$B$+$a(B$B$kI,MW$O$"$j$^$;$s$h!#!V(B2$B$NJ?J}:,!W$,3N$+$K<B?t$H$7$FB8:_$9$k$N$J(B
$B$i!"$=$N$3$H$H!"!V(B2$B$NJ?J}:,!W$,M-M}(B$B?t$G$"$jF@$J$$$H$$$&>ZL@$H$+$i!"L5(B
$BM}?t$N6qBNNc$H$7$F!V(B2$B$NJ?J}:,!W$,8+$D$+$k$8$c$J$$$G$9$+!#(B
$B!V(B2$B$NJ?J}(B$B:,!W$O<B?t$G$"$C$FM-M}?t$G$J$$$3$H$,$o$+$C$?$N$@$+$i!#(B
--
$BN6C+Bg3XM}9)3XIt?tM}>pJs3X2J(B $B>.NS(B  $BAo(B |  Heaven helps those who
satoshi@rins.ryukoku.ac.jp            |      help themselves.
0775-43-7523($B3X2J;v(B$BL3<<(B) 7528($B8&5f<<(B) |  Barber shaves those who
        7524(FAX)                     |      never shave themselves.