🚀 go-pugleaf

In article <1993Jan29.202150.4384@etl.go.jp> yoshiki@etl.go.jp (KINOSHITA Yoshiki) writes:
>>
>>        a = b -> (Fa <-> Fb) for all F
>
><-> $B$O(B -> $B$G==J,$G$9!#BP>NN'$,Bg>fIW$+$H?4G[$K$J$j$^$9$,!"Bg>fIW$G$9!#(B
>$B$A$g$C$H$7$?%Q%:%k$G$9!#(B

$B$O$$!"$b$A$m$s!#$G$b!"F10l@-$HF1CM@-$H$,$D$J$,$k$H$$$&$3$H$G(B
$B$o$+$j$d$9$$$H;W$C$?$s$G$9$,!#(B

>Leibniz $B$N(B equality $B$rCN$i$J$$?M$O>e$N<0$r(B parse $B$9$k$N$,:$Fq$@$H;W$&(B
>$B$N$G$A$g$C$HJdB-$7$^$9$H!"Fs3,0J>e$N=R8lO@M}$G!"(B
>
>	EQ(x,y) $B$r(B $B"O(BP:Object$B"*(BProp. P(x)$B"?(BP(y) $B$K$h$C$FDj5A$9$k(B
>
>$B$H!J"O(BP:Object$B"*(BProp $B$OG$0U$N0lJQ?t=R8l(B P $B$K$D$$$F!"$H$$$&0UL#!K!"(BEQ $B$O(B
>$BF1CM4X78$K$J$j$^$9!#$7$+$b!"JL$KF1CM4X78(B EQ' $B$,$"$l$PI,$:(B
>
>	$B"O(Bx,y:Object. EQ'(x,y)$B"?(BEQ(x,y)
>
>$B$,@.$jN)$A$^$9!#$3$N$3$H$r$5$7$FEZ20$5$s$,!VF10l@-$NI,MW>r7o!W$H$$$C$F(B
>$B$*$i$l$k$s$@$H;W$$$^$9$,!"$A$g$C$H$o$+$j$K$/$$$G$9$M!#(BEQ $B$,(B Leibniz $B$N(B 

$B$3$C$A$NJ}$,KM$K$O$o$+$j$K$/$$!#$^$"$=$l$OJL$H$7$F!"(B

        a = b -> (Fa <-> Fb) for all F

$B$G$O!"F10l@-$rDj5A$7$F$J$$$3$H$KCm0U$7$F$/$@$5$$!#$7$?$,$C$F!"(B
$B$3$l$O!"(BLeibniz$B$NF10l@-$NH>J,$G$9!#(B


>$B:dED$5$s$,!V$$$+$J$k<jCJ$K$h$C$F$b8+J,$1$,$D$+$J$1$l$PF1$8$J$s$@!W$H$$$C(B
>$B$F$*$i$l$^$7$?$,!"$3$l$O(B Leibniz $B$N9M$($K6a$$$H;W$$$^$9!#(B

$B$H$$$&$3$H$G$9$,!"$3$l$O$$$o$f$kIT2D<1JL<TF10l86M}(B(the identity
of the indiscernibles)$B$N$[$&$G!"(B

        (Fa <-> Fb) for all F -> a = b

$B$K$"$?$j$^$9!#KM$,:G=i$K=R$Y$?$N$O!"$$$o$f$kF10l<TBeF~2DG=86(B
$BM}(B(the substitutivity of the identicals)$B$G!"$3$l$NJ}$,$O$k$+(B
$B$K<e$$$o$1$G$9$,!"(B

>equality $B$H$$$&$d$D$G$9$,!"O@M}5-9f$@$1$+$iDj5A$G$-$k$N$,L%NO$G$9!#$=(B
>$B$N$+$o$j!"9b3,O@M}!"(Bimpredicativity $B$J$s$F$b$N$rG'$a$J$$$H$$$1$J$$$o$1(B
>$B$G$9$,!#$=$l$K!"(Binductive definition $B$J$s$+$r9M$($h$&$H$9$k$H!"$3$l$@(B
>$B$1$G$O$f$k$9$.$F%@%a$H$$$&$3$H$K$9$0$J$j$^$9!#(B

$BF10l<TBeF~2DG=86M}$G$9$H!"(BF$B$NNL2=$rMW5a$7$J$$$G$b$$$$$@$m$&$H(B
$B$$$&$H$$$&$3$H$K$J$j$^$9!#$3$NE@$O0F30Fq$7$$$N$G!"$3$NA0$O!"(B
$B$H$j$"$($:(BF$B$NA4BN$H$$$&$3$H$,0UL#$r;}$D$H$$$&$3$H$G$H$$$&$3$H(B
$B$G!"6KC<$JJ]<i<g5A$+$i$O$d$d$f$k$/$7$F$*$-$^$7$?!#IT2D<1JL<T(B
$BF10l86M}$O$/$k$7$$$+$i!"F10l<TBeF~2DG=86M}$@$1$GF10l@-$rFCD'(B
$B$E$1$F$*$3$&$H$$$&$N$O!"%U%l!<%2$+$i%/%o%$%s$^$G$[$H$s$I$NE/(B
$B3X<T$K6&DL$7$F$$$^$9!#$7$+$7!"$3$l$G$O!"(B2$B$D$N$b$N$,M?$($i$l$?(B
$B$H$-!"$I$N$h$&$J$H$-$KF10l$K$J$k$+$H$$$&$3$H$r7h$a$k$?$a$N4p(B
$BAC$H$9$k$3$H$O$G$-$^$;$s!#$D$^$j!"F10l@-$N4p=`$r$7$a$9$?$a$N(B
$B4pAC$H$J$i$J$$$N$G$9!#$7$+$7!"$$$^$^$G=P$F$-$?$h$&$J4p=`0J30(B
$B$K$b!"BP>]$N<oN`$K$h$C$F$O!"$b$C$H<+A3$J4p=`$rDs0F$9$k$3$H$,(B
$B$G$-$k$7!"$^$?!"$=$N$h$&$J4p=`$r9M$($l$P!"$=$N$H$-$OIT2D<1JL(B
$B<TF10l86M}$N$h$&$J6/NO$JO@M}E*K!B'$NNO$r<Z$j$kI,MW$,$J$$$3$H(B
$B$b;v<B$G$9!#$?$H$($P!"(B($B$3$3$O!"(Bfj.ai$B$G$9$+$i(B)$B?M3J$NF10l@-$N4p(B
$B=`$H$7$F!"5-21$,F1$8$3$H$H$$$&$N$G$O$I$&$G$9$+!)5-21$NF10l@-(B
$B$O!"5-21FbMF$rI=8=$9$kL?Bj$N0lCW$H$$$&$3$H$K$7$^$9!#$"$k$$$O!"(B
$B$5$^$6$^$JBe<U$r9MN8$7$?$&$($G!"BN$N;~6uE*O"B3@-$H$$$&$N$G$O(B
$B$I$&$G$9$+!#$3$N$H$-$NO"B3@-$O!"M}A[E*$J4Q;!<T$K$h$k4Q;!2DG=(B
$B@-$K$h$C$F$-$a$k$3$H$K$7$^$9!#$3$&$9$l$P!"IT2D<1JL<TF10l86M}(B
$B$J$7$K$$$m$$$m$JBP>]$K$D$$$FF10l@-$N4p=`$rDj$a$k$3$H$,$G$-$k(B
$B$7!"$=$N$"$H$G$O!"$^$:LdBj$N$J$$F10l<TBeF~2DG=86M}$@$1$G$d$C(B
$B$F$$$1$k$H$$$&$3$H$K$J$k$G$O$J$$$G$7$g$&$+!#$*$=$i$/!"$3$N$h(B
$B$&$J9M$($O!"J]<iE*$JE/3X<T$NJ]?HE*2r7h$H$7$F$$$$$N$G$O$J$$$+(B
$B$H;W$C$F$$$^$9!#$D$^$j!"$R$H$3$H$G8@$($P!"!VF10l@-$N4p=`$O>!<j(B
$B$K7h$a$F$/$@$5$$!#$?$@$70lEY(Ba$B$H(Bb$B$,F10l$@$H$$$&$3$H$J$C$?$i!"(B
$B$=$N$"$H$O!"(Ba$B$K$D$$$F$$$($k$3$H$O!"$J$s$G$b(Bb$B$K$D$$$F8@$($k$H(B
$B$$$&$3$H$GOC$r?J$a$^$9$h!W$H$$$&$3$H$G$9!#(B

$B$7$?$,$C$F!":G6a:#$^$G$K$3$3$G5DO@$K$J$C$?$$$m$$$m$JDs0F$O!"(B
$BF10l@-$G$O$J$/!"F10l@-$N4p=`$K$D$$$F$N$b$N$@$C$?$N$G$9!#$=$N(B
$BE@!"O7GL?4$J$,$i!#(B

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