🚀 go-pugleaf

In article <2630@tansei1.tansei.cc.u-tokyo.ac.jp> hogura@tansei.cc.u-tokyo.ac.jp (Hiroaki Ogura) writes:
>In article <2598@tansei1.tansei.cc.u-tokyo.ac.jp> I wrote:
>> $BNc$($P!"5-9fO@M}$N7A<0E*>ZL@$K$*$$$F!"O@M}<0#B$KBP$7$F>ZL@$,(B
>>$B$"$k>l9g$K!"!V#B$O>ZL@2DG=$G$"$k!W$rI=$9!"(B" |-$B#B(B " $B$N(B "|-" $B$H(B
>>$B$$$&5-9f(B ( latex $B$G$$$&$H$3$m$N(B \vdash $B$G$9(B) $B$O!"IaDL2?$HH/2;(B
>>$B$9$k$N$G$7$g$&$+(B?
>$B$H$$$&<ALd$KBP$7!"KLN&@hC<Bg$NIMED$5$s$+$i(B
>    article <NAO.92Jul15172530@mimo.jaist-east.ac.jp>
>$B$K$F2sEz$r$$$?$@$-$^$7$?!#(B
>$B$^$H$a$^$9$H!"(B
> $B!&(B D. van Dalen, Logic and Structure (2nd ed.), 1983, Springer-Verlag
>    $B$NCf$G$O!"(B "|-" $B$O(B "turnstile" $B$H8F$V$H$7$F$$$k!#(B
> $B!&(B $BIMED$5$s$4<+?H$O(B "|-" $B$r(B "$B$H(B" $B$HFI$s$G$$$k!#(B
># "turnstile" $B$r<-=q$G0z$$$?$i(B "$B2sE>OSLZ(B"$B$H$$$&0UL#$G!"$I$&$d$i(B "|-"
># $B$H$$$&5-9f$r;k3PE*$J%$%a!<%8$KB*$($FFI$s$G$$$k!"$H$$$&$N$,0lHLE*$J(B
># $B$h$&$G$9$M!#(B

$B$$$(!"$=$s$J$3$H$O$J$$$G$7$g$&!#>ZL@O@$N?M!9$O!"(B"|-B"$B$r!V#B(B
$B$O>ZL@2DG=$G$"$k!W!V#B$K$O>ZL@$,$"$k!W$HFI$s$G$$$k$N$G$O$J$$(B
$B$G$7$g$&$+!#(B($BFI$^$J$$$G!"$?$@=q$/$@$1$N$3$H$,B?$$$N$G$O$J$$(B
$B$G$7$g$&$+!#(B)"$B%?!<%s%9%?%$%k%S!<(B"$B$J$s$FFI$`?M$O$$$J$$$H;W$$(B
$B$^$9!#$3$N5-9f$NL>A0$O!"$?$7$+$K!"$"$k@$3&$G$O(Bturnstile$B$G$9(B
$B$,!"(B1980$BG/Be8eH>$N%9%?%s%U%)!<%IBg3X$N0l6y$G$O!"(Bturnstile$B$H(B
$B$$$($P$`$7$m(B"|="$B$H$$$&5-9f$N$3$H$G$7$?!#$b$H$b$H$3$N5-9f$O!"(B
Gottlob Frege$B$,(B1879$BG/$KCx=q(B Begriffsschrift $B$GF3F~$7$?$b$N$G(B
$B$9!#$=$N$H$-$O!"=DK@$NItJ,$r(BUrteilsstrich($BH=CG@~(B)$B!"(B
$B2#K@$NItJ,$r(BInhaltsstrich($BFbMF@~(B)$B$HFI$s$G$$$^$7$?!#(B1893$BG/$K$O!"(B
$B8e<T$r$?$s$K(Bder wagerechte Strich$B$H8F$V$h$&$K$J$j$^$7$?!#$=$N(B
$B$&$A!"L565M\$JO@M}3X<T(B(Martin Lof$B$J$I$O65M\$,$"$j$^$9$,(B)$B$,$3(B
$B$l$r$R$H$D$N5-9f$H$7$F$"$D$+$&$h$&$K$J$C$?$N$G$9!#$7$?$,$C$F!"(B
$B$^$@$3$N8mI5$NNr;K$OD{@52DG=$G$"$k$H;W$$$^$9!#$=$s$J$H$-$KFI(B
$B$_J}$J$s$+5$$K$7$J$$$G$/$@$5$$!#(B

$BEZ20(B($B@iMUBg3X(B)