🚀 go-pugleaf

In article <C1M82C.MI3@culle.l.chiba-u.ac.jp> tutiya@culle.l.chiba-u.ac.jp (Syun Tutiya) writes:
>$B$"$?$j$^$($_$?$$$G$9$,!"$=$NDL$j$G$O!)F10l@-$NI,MW>r7o$O4JC1(B
>$B$G$9$h$M!#(B 
>
>        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

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 
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

$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!W(B
$B$-$N$7$?(B
-- 
KINOSHITA Yoshiki [KINOSHITA is my family name]
Department of Computer Science, University of Edinburgh
James Clark Maxwell Building, The King's Buildings, Edinburgh EH9 3JZ, Scotland
[On leave from Electrotechnical Laboratory, 1-1-4 Umezono, Tsukuba, 305 Japan]