🚀 go-pugleaf

$@>.NS(J@$@N6C+Bg3X$G$9!#(J

In article <568@keu02.rtri.or.jp> shingo@ipc02.rtri.or.jp (Shingo MATSUMOTO) writes:

 |$@!!>e$NK\$O!"$$$o$f$kD>4Q<g5A=89gO@$K$D$$$F=R$Y$?$b$N$G$O$J$$!#$$$o$f$kD>4Q<g5A(J

$@$=$&$J$s$G$9(J! $@$"$N(J$@%?%$%H%k$K$b4X$o$i$:$M!#(J

 |$@!!$5$F!"7A<0<g5A$HD>4Q<g5A$H$r!"#Z#F#C$N%b%G%kFb$GHf$Y$F$_$l$P!"(J
 |$@!VA4IT(J$@O"7k$J0LAj6u4V!W$H!V0lHL$N0LAj6u4V!W(J
 |$@$KBP1~$9$k!#(J

$@=EH"$N$9$_$r$D$D$/$h$&$G$9$_$^$;$s$,!"!VA4ITO"7k(J$@!W$H$$$&$N$H$O$A$g$C$H(J
$@0c$&$N$G$O(J?

 |$@!!C]Fb$NK\$G$O!"D>4Q<g5A$N@-<A$O!"%b%G%k$X$NBP1~$K$h$C$F!"0LAj6u(J$@4V$N@-<A$H$7$F(J
 |$@2r<a$5$l$k!#D>4Q<g5A$K$OB>$K!"(JBKF-$@2r<a$H$+!"<B8=2DG=@-$K$h$k2r<a$,$"$k$,!"$=$l(J

$@$($((J$@$H!"$3$N(J BKF $@$H$$$&$N$O(J BHK $@$N$3$H$G$9$+(J? $@$=$&$$$&8F$SJ}$b$"$C$?$+(J
$@$J(J? $@$=$l$H$bJL$N$b$N$G$7$g$&$+(J? $@$"(J$@!"$R$g$C$H$9$k$H!"(JBeth-Kripke $@$+$J(J? 
$@$9$k$H;D$j$N(J F $@$O2?$@$m$&(J?  Forcing $@$+$J(J?

 |$@$>$l$O!"0l1~FHN)$N$b(J$@$N$H9M$($?J}$,$h$$$h$&$@!#(J

$@>/$J$/$H$b!"<B8=2DG=@-$O0LAj6u4V$NOC$H$OA4A3JL$@$H;W$C$F$$$$$H;W$$$^$9!#(J

 |$@!!$J$*!"$3$N7o$G$O!"N6C+Bg3X$N>.NS@h@8$K$O!"$$$m$$$m$H65$($F$$$?$@$-$^$7$?!#(J
 |$@!!46<U$$$?$7$F$*$j$^(J$@$9!#(J

$@$I$&$$$?$7$^$7$F!#;d$b$7$P$i$/(JV(\Omega)$@4X78$rJY6/$7$F$J$/$F!"?'!9K:$l(J
$@$F$$$?$3$H$b$"$j!"5-21$r(J refresh $@$G$-$FM-1W$G$7$?$7!"LLGr$$5DO@$G!"3Z(J
$@$7$^$;$F$b$i$$$^$7$?!#(J

$@$^$"!"%M%C%H%o!<%/$G$O$*8_$$=u$1(J$@9g$$$H$$$&$3$H$G!#(J
#fj.sci.math $@=u$19g$$1?F0!#(J<- $@$3$l$,8@$$$?$+$C$?$N(J :-)
--
			$@N6C+Bg3XM}9)3XIt?tM}>p(J$@Js3X2J(J    $@>.NS(J  $@Ao(J
			satoshi@whale.ryukoku.ac.jp
			0775-43-7523($@3X2J;vL3<<(J) 0775-43-7528($@8&5f<<(J)
			0775-43-7524(FAX)

$B>>K\!w?t3X2J$/$:$l(B

$BD>4Q<g5A$N2r<a$N0c$$(B($B%b%G%k$N0c$$(B)$B$K$D$$$F!"JdB-$7$^$9!#(B

In article <568@keu02.rtri.or.jp> shingo@ipc02.rtri.or.jp (Shingo MATSUMOTO) writes:
$B!dC]Fb$NK\$G$O!"D>4Q<g5A$N@-<A$O!"%b%G%k$X$NBP1~$K$h$C$F!"(B$B0LAj6u4V$N@-<A$H$7$F(B
$B!d2r<a$5$l$k!#D>4Q<g5A$K$OB>$K!"(BBKF-$B2r<a$H$+!"<B8=2DG=@-$K$h$k2r<a$,$"$k$,!"(B
$B!d$=(B$B$l$>$l$O!"0l1~FHN)$N$b$N$H9M$($?J}$,$h$$$h$&$@!#(B

$B$=$&8@$($P!"3^;a$,%a!<%k$G!"(B
$B!V(BBKF-interpretation$B$O(B$B==J,7A<02=$5$l$F$$$J$$!W(B
$B$H$$$&$N$G!"$=$s$J$3$H$O$J$$!"(B
$B!V(Brealizability-interpretation$B$G!"7A<02=$5$l$F(B$B$$$k!W(B
$B$H=R$Y$?$H$3$m!"(B
$B!V(Bor$B$N2r<a$,L@$i$+$K0[$J$k!W(B
$B$H$$$&!#=i$a$O2?$r8@$C$F$$$k$s$@$3$$$D$O$H$*$b$C(B$B$?$,(B
$B!V(BV($B&8(B)$B$G$O!"(B|A or B| = 1 $B$@$+$i$H$$$C$F(B |A|=1 $B$+(B |B|=1$B$G$"$k$H$O$$$($J$$!W(B
$B$N0UL#$@$H5$$,IU$$$?(B$B!#(B
$B$=$l$OA4$/$=$N$H$*$j$G$"$k!#;d$O$I$A$i$+$H$$$($P!"GSCfN'1>!9$h$j!"5"G<E*(B
$B$J$b$N$r=E;k$7$?$3$H$K6=L#(B$B$,$"$k$N$G!"$=$NJ}8~$G@bL@$7$F$7$^$C$?$N$@$,!"(B
$B:G=i$+$i!"0LAj6u4V$N@-<A$H$7$F!"@bL@$7$?$[$&$,$h$+$C$?(B$B$H8e2y$7$F$$$k!#(B

($B$b$C$H$b!"(BIZF$B$N$h$&$JBN7O$G$O!"(Brealizability-interpretation$B$,$G$-$k$H$O(B
$B;d<+?H!"$O(B$B$8$a$+$i9M$($F$O$$$J$+$C$?$,!#$3$N$3$H$+$i$b!"C1$J$kGSCfN'$N5q(B
$BH]$H$$$&0UL#$ND>4Q<g5A$H!"9=@.E*$H$$$&(B$B35G0$O0[$J$k$b$N$H$$$($k$h$&$@!#(B)

$B$H$3$m$G!">e$N#2$D$N2r<a$K$D$$$F!"9M$($k$&$A$K(B
$B$"$k5?Ld$,@8$8$F$-$^(B$B$7$?!#(B

V($B&8(B)$B$O!"9b3,D>4Q<g5AO@M}$N7wO@E*2r<a$H$7$F$N%H%]%9$H$_$J$;$k$N$G$7$g$&!#(B
($B$b$A$m$s!"%H%]%9$K(B$B$D$$$F!"CN$C$F$$$k$o$1$G$O$"$j$^$;$s$,(B)
$B$H$$$&$3$H$G!"D>4Q<g5AO@M}$K$^$:7wO@E*$J2r<a$,$"$j$^$9!#(B
$B0lJ}(B$B$G$O!"0lHL$ND>4Q<g5AO@M}$h$j69$$HO0O$N$b$N$G$9$,(B
$B9=@.E*$JM}O@$KBP$9$k<B8=2DG=@-2r<a$,$"$j$^$9!#(B
$B5?Ld$H(B$B$$$&$N$O!"7wO@E*2r<a$H!"<B8=2DG=@-2r<a$H$O!"(B
$B$I$&$$$&4X$o$j$,$"$k$N$G$7$g$&$+$H$$$&$3$H$G$9!#(B
$BC<E*$K$$(B$B$($P!"(B
$B5"G<E*$J35G0$O!"7wO@$N$I$N$h$&$J35G0$KBP1~$9$k$+(B
$B$H$$$&$3$H$G$9!#(B

$B>>K\!w?t3X2J$/$:$l$G$9!#(B

$B$^$?!":Y$+$$$H$3$m$G%P%0$C$F$7$^$$$^(B$B$7$?!#(B

In article <SATOSHI.92Dec14202116@whale.math.ryukoku.ac.jp> satoshi@whale.math.ryukoku.ac.jp (Satoshi Kobayashi) writes:
$B!d(B    |$B!!$5$F!"7A<0<g5A$HD>4Q<g5A$H$r!"#Z#F#C$N%b%G%kFb$GHf$Y$F$_$l$P!"(B
$B!d(B    |$B!VA4ITO"7k$J0LAj6u4V!W$H!V0lHL$N0LAj6u4V!W(B
$B!d(B    |$B$KBP1~$9$k!#(B

$B!d(B   $B=EH"$N$9$_$r$D$D$/$h$&$G$9$_(B$B$^$;$s$,!"!VA4ITO"7k!W$H$$$&$N$H$O$A$g$C$H(B
$B!d(B   $B0c$&$N$G$O(B?

$B$"!"$I$&$b$9$_$^$;$s!#7A<0<g5A$NGSCfN'$,(B$B!"ITO"7k@-$K$"$?$k$3$H$O!"$o$+$C$?(B
$B$N$G$9$,!"$I$&$b!"0lHL$N0LAj$KBP$7$F!"$I$&$$$&0LAj$r$H$k$H!"7A<0<g(B$B5A$N%b%G(B
$B%k$H$J$jF@$k$+$K$D$$$F!">/!9%-!<$,$9$Y$C$F$7$^$$$^$7$?!#$?$H$($P!"N%;60LAj(B
$B$@$H!"7A<0<g5A$N%b(B$B%G%k$K$J$j$^$9!#(B

  $B$"$H!"(BMeta theory$B$G!"%U%)%m!<$7$FD:$$$?!"%b%G%k$N9=@.K!$G!"(BV($B&8(B)$B$,8EE5(B
$BO@M}$G$D$/(B$B$i$l$k$H$$$&$N$O!";d$bG'<1$7$F$*$j$^$9!#D>4Q<g5A$N%b%G%k$r!"$I(B
$B$N$h$&$K9=@.$7$h$&$H!">ZL@$G$-$k$3$H!"(B$BG$0U$N%b%G%k$G??$G$"$k$3$H$NFbMF$K(B
$B$O1F6A$7$J$$$H$$$$$?$+$C$?$o$1$G$9!#(B
($B$3$s$J$3$H!"$o$6$o$6$$$o$J$/(B$B$F$b!"$"$?$j$^$($G$9$,(B^^;)

    |$B!!C]Fb$NK\$G$O!"D>4Q<g5A$N@-<A$O!"%b%G%k$X$NBP1~$K$h$C$F!"0LAj6u4V$N(B$B@-<A$H$7$F(B
    |$B2r<a$5$l$k!#D>4Q<g5A$K$OB>$K!"(BBKF-$B2r<a$H$+!"<B8=2DG=@-$K$h$k2r<a$,$"$k$,!"$=$l(B

$B!d(B   $B$($($H!"$3$N(B BKF $B$H$$$&$N$O(B BHK $B$N$3$H$G$9$+(B? $B$=$&$$$&8F$SJ}$b$"$C$?$+(B
$B!d(B   $B$J(B? $B$=$l$H$bJL$N$b$N$G$7$g(B$B$&$+(B? $B$"!"$R$g$C$H$9$k$H!"(BBeth-Kripke $B$+$J(B? 
$B!d(B   $B$9$k$H;D$j$N(B F $B$O2?$@$m$&(B?  Forcing $B$+$J(B?

$B$9$_$^$;(B$B$s!#(BBHK(=Brouwer-Heyting-Kolmogorov)$B$N8m$j$G$9!#(B
$BM>7W$J5$$r2s$5$;$F$7$^$C$?$h$&$G$9$M!#(B
$B$d$O$j!"IaCJ;H(B$B$o$J$$8@MU$O!"4V0c$$$d$9$$(B(^^;)

    |$B$>$l$O!"0l1~FHN)$N$b$N$H9M$($?J}$,$h$$$h$&$@!#(B

$B!d(B   $B>/$J$/$H$b(B$B!"<B8=2DG=@-$O0LAj6u4V$NOC$H$OA4A3JL$@$H;W$C$F$$$$$H;W$$$^$9!#(B

$B$d$O$j!"$=$&$G$9$+!#(B
$B$J$K$+!"4XO"$,$"(B$B$k$+$H;W$$!"$$$m$$$m$H9M$($F$7$^$C$?$b$N$G!#(B

$B!d(B   $B$^$"!"%M%C%H%o!<%/$G$O$*8_$$=u$19g$$$H$$$&$3$H$G!#(B
$B!d(B   #fj.sci.math $B=u$19g$$1?F0!#(B<- $B$3$l$,8@$$$?$+$C$?$N(B :-)

fj.sci.math$B$b!"B830<N$F$?$b$N$G$O$J$$$G(B$B$9$M!#(B:-)

$@>.NS(J@$@N6C+Bg3X$G$9!#<+J,$N5-;v$K%U%)%m!<$7$^$9!#(J

In article <SATOSHI.92Dec14202116@whale.math.ryukoku.ac.jp> satoshi@whale.math.ryukoku.ac.jp (Satoshi Kobayashi) writes:

 | |$@!!$5$F!"7A<0<g5A$HD>4Q<g5A$H$r!"#Z#F#C$N%b%G%kFb$GHf$Y$F$_$l$P!"(J
 | |$@!VA4IT(J$@O"7k$J0LAj6u4V!W$H!V0lHL$N0LAj6u4V!W(J
 | |$@$KBP1~$9$k!#(J
 |
 |$@=EH"$N$9$_$r$D$D$/$h$&$G$9$_$^$;$s$,!"!VA4(J$@ITO"7k!W$H$$$&$N$H$O$A$g$C$H(J
 |$@0c$&$N$G$O(J?

$@$3$l$@$1$G$OIT?F@Z$+$H;W$&$N$G!"6qBNE*$KH?Nc$r$"$2$^$9!#M-(J$@M}?tBN(J Q $@$O!"(J
$@DL>o$N0LAj$N$b$H$GA4ITO"7k$G$9$,!"$=$N3+=89g$NB+$O(JBoolean $@$G$O$"$j$^$;(J
$@$s$M!#(J

 | |$@!!C](J$@Fb$NK\$G$O!"D>4Q<g5A$N@-<A$O!"%b%G%k$X$NBP1~$K$h$C$F!"0LAj6u4V$N@-<A$H$7$F(J
 | |$@2r<a$5$l$k!#D>4Q<g5A$K(J$@$OB>$K!"(JBKF-$@2r<a$H$+!"<B8=2DG=@-$K$h$k2r<a$,$"$k$,!"$=$l(J
 |
 |$@$($($H!"$3$N(J BKF $@$H$$$&$N$O(J BHK $@$N$3$H$G(J$@$9$+(J? $@$=$&$$$&8F$SJ}$b$"$C$?$+(J
 |$@$J(J? $@$=$l$H$bJL$N$b$N$G$7$g$&$+(J? $@$"!"$R$g$C$H$9$k$H!"(JBeth-Kripke $@$+$J(J? 
 |$@$9$k$H;D$j$N(J F $@$O2?$@$m$&(J?  Forcing $@$+$J(J?

$@>>K\$5$s$NJL$N5-;v$r8+$?=j$G$O!"(JBHK $@$HF1$8$b$N$N$h$&$G(J$@$9$M!#;d$O(JBHK$@$H(J
$@$$$&8@$$J}$7$+8+$?$3$H$,$J$$$N$G$9$,!"(JBKF $@$H$$$&8@$$J}$,=P$F$$$kJ88%$r(J
$@CN$C$F$$$kJ}$,(J$@$"$C$?$i65$($F2<$5$$!#(J
--
			$@N6C+Bg3XM}9)3XIt?tM}>pJs3X2J(J    $@>.NS(J  $@Ao(J
			satoshi@whale.ryukoku.ac.jp
			0775-43-7523($@3X2J;vL3<<(J) 0775-43-7528($@8&5f<<(J)
			0775-43-7524(FAX)

$@@P86!wKLN&@hC<Bg$G$9!#(J

In article <SHINGO.92Dec17130040@ipc02.rtri.or.jp> shingo@ipc02.rtri.or.jp (Shingo MATSUMOTO) writes:

   >>$@!d(J   $@>/$J$/$H$b!"(J$@<B8=2DG=@-$O0LAj6u4V$NOC$H$OA4A3JL$@$H;W$C$F$$$$$H;W$$$^$9!#(J
   >>
   >>$@$d$O$j!"$=$&$G$9$+!#(J
   >>$@$J$K(J$@$+!"4XO"$,$"$k$+$H;W$$!"$$$m$$$m$H9M$($F$7$^$C$?$b$N$G!#(J

$@;d$b$^$@%-%A%s$HJY6/$7$F$$$J$$$N$G$9$,!"<B8=(J$@2DG=@-$H0LAj6u4V7O(J($@AX!&%H%]%9$J$I$b(J
$@4^$`(J)$@$N%b%G%k$N4X78$K$D$$$F$O!"0J2<$NJ88%$,;29M$K$J$k$N$G$O$J$$$G(J$@$7$g$&$+!)(J

	Hyland, J.M.E
	The effective topos
	Troelstra, A.S. and D. van Dalen eds.,
	The L.E.J. Brouwer Centenary Symposium
	165-216

$@$^$?!"(J

	Troelstra, A.S. and D. van Dalen
	Constructivism in Mathematics, Vol. 2
	13.8 (724-729)

$@$K4JC1$J2r@b$,$G$F$$$^$9!#(J

$@ITJY6/$J$b$N$GE*$O$:$l$J%3%a%s%H$@$C$?$i(J$@%4%a%s%J%5%$!#(J

--
------------------------------------------------------------------------
$@@P86(J  $@:H(J : $@KLN&@hC<2J3X5;=QBg3X1!Bg3X(J $@>pJs2J3X8&5f2J!J>pJsO@M}3X!K(J
TEL: 0761-51-1206, FAX: 0761-51-1338, e-mail: ishihara@jaist-east.ac.jp

$@>.NS(J@$@N6C+Bg3X$G(J$@$9!#(J

In article <SHINGO.92Dec17130040@ipc02.rtri.or.jp> shingo@ipc02.rtri.or.jp (Shingo MATSUMOTO) writes:

 |$@!d(J    |$@!!$5$F!"7A<0<g5A$HD>4Q<g5A$H$r!"#Z#F#C$N%b%G%kFb$GHf$Y$F$_$l$P!"(J
 |$@!d(J    |$@!VA4ITO"7k(J$@$J0LAj6u4V!W$H!V0lHL$N0LAj6u4V!W(J
 |$@!d(J    |$@$KBP1~$9$k!#(J
 |
 |$@!d(J   $@=EH"$N$9$_$r$D$D$/$h$&$G$9$_$^$;$s$,(J$@!"!VA4ITO"7k!W$H$$$&$N$H$O$A$g$C$H(J
 |$@!d(J   $@0c$&$N$G$O(J?
 |
 |$@$"!"$I$&$b$9$_$^$;$s!#7A<0<g5A$NGSCfN'$,!"(J$@ITO"7k@-$K$"$?$k$3$H$O!"$o$+$C$?(J
 |$@$N$G$9$,!"$I$&$b!"0lHL$N0LAj$KBP$7$F!"$I$&$$$&0LAj$r$H$k$H!"7A<0<g(J$@5A$N%b%G(J
 |$@%k$H$J$jF@$k$+$K$D$$$F!">/!9%-!<$,$9$Y$C$F$7$^$$$^$7$?!#$?$H$($P!"N%;60LAj(J
 |$@$@$H!"7A<0<g5A(J$@$N%b%G%k$K$J$j$^$9!#(J

$@$=$&$G$9$M!#N%;60LAj$J$i$b$A$m$s$=$&$J$j$^$9!#B?J,!"N%;66u4V$K$J$i$J$$(J
$@>l9g$G$b(J$@!"J,N%$G$-$J$$$h$&$J(J2$@E@$rF10l;k$7$F$D$V$7$?6u4V$,N%;6$K$J$k$s(J
$@$8$c$J$$$+$J(J?$@0c$C$?$+$J(J?($@%A%'%C%/$7$F$_(J$@$F2<$5$$(J)

$@$H$3$m$G!"$3$&$$$&J8L.$G!V7A<0<g5A!W$H$$$&8@MU$r;H$&$N$O$I$&$b;d$K$O0c(J
$@OB46$,$"$k$N$G$9$,!#(J$@!V7A<0<g5A!W$NCf?4E*$J;WA[$O(J($@Bg$6$C$Q$K8@$&$H(J)$@!V7A(J
$@<0E*$K$d$k$3$H!W$K$"$k$h$&$K;W$&$N$G!#3N$+$K7A<0<g(J$@5A$r$H$J$($?%R%k%Y%k(J
$@%H$OGSCfN'$r<i$kN)>l$G(J Brouwer $@$H%1%s%+$7$F$^$7$?$,!#(J
$@$3$3$NJ8L.$G$O!"!V8EE5O@M}(J$@!W$H=q$$$?J}$,NI$$5$$,$7$^$9!#(J

$@$D$$$G$G$9$,!"0LAj6u4V$N@5B'3+=89g$NA4BN$r??M}CM$H$9$k$H!"8EE5O@M}$,@.(J
$@N)$9$k!"$H$$$&8+J}$b$"$j$^$9$M!#B?J,$4B8$8$@$m$&$H;W$$$^$9$1$I!#$b$A$m(J
$@$s!"$=$N>l9g!"3+=89g$NB+$N>l9g(J$@$H$O!"0c$&1i;;$,F~$C$F$$$^$9$1$I!#(J

 |$@!d(J   $@$($($H!"$3$N(J BKF $@$H$$$&$N$O(J BHK $@$N$3$H$G$9$+(J? $@$=$&$$$&8F$S(J$@J}$b$"$C$?$+(J
 |$@!d(J   $@$J(J? $@$=$l$H$bJL$N$b$N$G$7$g$&$+(J? $@$"!"$R$g$C$H$9$k$H!"(JBeth-Kripke $@$+$J(J? 
 |$@!d(J   $@$9$k(J$@$H;D$j$N(J F $@$O2?$@$m$&(J?  Forcing $@$+$J(J?
 |
 |$@$9$_$^$;$s!#(JBHK(=Brouwer-Heyting-Kolmogorov)$@$N8m$j$G$9!#(J

$@$"!"$=$&$@$C$?$s$G$9$+!#0B?4$7$^$7$?!#(J

 |$@!d(J   $@>/$J$/$H$b!"<B8=2DG=@-$O0LAj6u4V$NOC$H$OA4A3JL$@$H;W$C(J$@$F$$$$$H;W$$$^$9!#(J
 |
 |$@$d$O$j!"$=$&$G$9$+!#(J
 |$@$J$K$+!"4XO"$,$"$k$+$H;W$$!"$$$m$$$m$H9M$($F$7$^$C$?$b(J$@$N$G!#(J

$@$3$l$K$D$$$F$O!"JL$N5-;v$G>/$7=q$-$^$7$?$N$G!"$*FI$_2<$5$$!#(J
--
			$@N6C+Bg3XM}9)3XIt?tM}>pJs3X(J$@2J(J    $@>.NS(J  $@Ao(J
			satoshi@whale.ryukoku.ac.jp
			0775-43-7523($@3X2J;vL3<<(J) 0775-43-7528($@8&5f<<(J)
			0775-43-7524(FAX)

$@>.NS(J@$@N6C+Bg3X$G$9!#D9$$$G$9!#(J

In article <SHINGO.92Dec15174617@ipc02.rtri.or.jp> shingo@ipc02.rtri.or.jp (Shingo MATSUMOTO) writes:

 |($@$b$C$H$b!"(JIZF$@$N$h$&$JBN7O$G$O(J$@!"(Jrealizability-interpretation$@$,$G$-$k$H$O(J
 |$@;d<+?H!"$O$8$a$+$i9M$($F$O$$$J$+$C$?$,!#$3$N$3$H$+$i$b!"(J$@C1$J$kGSCfN'$N5q(J
 |$@H]$H$$$&0UL#$ND>4Q<g5A$H!"9=@.E*$H$$$&35G0$O0[$J$k$b$N$H$$$($k$h$&$@!#(J)

$@;d$b0[$J$k(J$@$b$N$@$H;W$$$^$9!#(J

$@$H$3$m$G!"(JIZF $@$KBP$7$F$b!"<B$O(J realizability interpretation $@$rDj5A$9$k(J
$@$3$H$O$G$-(J$@$F!"$=$l$r;H$C$F!"$"$kDxEY(J metamathematical $@$J7k2L$r=P$9$3$H(J
$@$O$G$-$^$9!#$?$@!"$"$k0UL#$G$O$"$^$j%Q%C(J$@$H$7$J$$(J interpretation $@$J$N$G(J
$@$9$,!#$/$o$7$/$O!"(JM.J.Beeson: Foundations of Constructive Mathematics 
$@$N$h$&$JK\$r$4$i$s2<$5$$!#(J($@87L)$K$$$&$H!"$3$NK\$G07$C$F$$$k$N$O!"C]Fb(J
$@@h@8$NK\$N(J IZF $@$G$O$J$/$F!"$=$l(J$@$r$A$g$C$H$@$1JQ7A$7$?$b$N$J$N$G$9$,!#(J)

$@$I$&$$$&0UL#$G%Q%C$H$7$J$$$+!"$H$$$&$H!"(Je \r all x.A (e $@$O(J all x.A $@$r(J 
realize $@$9$k(J)$@$NDj5A$,!"(J
	all x.(ex \r A)   $@!D!D(J(a)
$@$G$O$J$/$F!"(J
	all x.(e \r A)    $@!D!D(J(b)
$@$K$J$C$F$$$k$N$G$9!#$D$^$j!"(Je $@$,=89g(J x $@$r<u$1<h$k(J operation $@$K$J$C$F$$(J
$@$^$;$s!#$3$l$O!"(JBHK $@$N9M$(J}$+(J$@$i$9$k$HJQ$J46$8$,$7$^$9!#$=$l$G!"%Q%C$H(J
$@$7$J$$!"$H8@$C$?$N$G$9!#>>K\$5$s$,!V(Jrealizability interpretation $@$,$G(J
$@$-$k$H$O9M$($F$$$J$+$C$?!W$H8@$o$l$?$N$O!"(J(a) $@$N$h$&$J7A$N(J 
interpretation $@$,$G$-$=$&$K$O;W(J$@$o$l$J$+$C$?!"$H$$$&$3$H$J$N$G$O$J$$$+!"(J
$@$HA[A|$7$F$$$k$N$G$9$,!"$I$&$G$9$+!#(J

$@$3$N(J interpretation $@$G(J$@$O!"(Jexists $@$N2r<a$bJQ$K$J$C$F$$$F!"(Je \r exists x.A
$@$NDj5A$O!"(J
	p_0(e) \r A[x/p_1(e)]   $@!D!D(J(c)
$@$G$O$J(J$@$/$F!"(J
	exists x.(e \r A)       $@!D!D(J(d)
$@$N$h$&$K$J$C$F$7$^$C$F$$$^$9!#(J(p_0,p_1 $@$O(J pair $@$rJ,2r$9$k(J projection 
$@$G$9!#(J)

$@$3$N2r<a$O!"9b3,;;=Q$KBP$9$k(J Kreisel-Troelstra $@$N(J realizability
interpretation $@$r(J IZF $@$N>l9g$K>F$-D>$7$?$b$N$K$J$C$F$$$^$9!#(J

$@:#!"(J2$@3,$N;;=Q$K$*$$$F!"=89g$rAv$kJQ?t$r(J X,Y $@$J$I$NBgJ8;z$G(J$@I=$9$3$H$K$7(J
$@$^$9!#(Jn,m $@$J$I$O!"<+A3?t$rAv$k$H$7$^$9!#(JKreisel-Troelstra $@$N(J 
realizability $@$G$O!"(Jall n.A $@$d!"(Jexists n.A $@$N2r<a$OIaDL$K$J$C$F$$$k$N(J
$@$G$9$,!"(Jall X.A $@$d(J exists X.A $@$N2r<a$O!"(J
	e \r all X.A = all X.(e \r A)    $@!D!D(J(b')
	e \r exists X.A = exists X.(e \r A)       $@!D!D(J(d')
$@$N$h$&$K$J$C$F$$$^$9!#(J$@$3$l$i$,$A$g$&$I>e$N(J (b),(d)$@$KBP1~$7$F$$$^$9!#(J
$@$3$l$rMQ$$$k$H!"<!$N$3$H$,>ZL@$G$-$^$9(J:
	(2$@3,$N;;=Q$,L5(J$@L7=b$J$i(J)2$@3,$N;;=Q$K(J
	all X.exists n.A(X,n) -> exists m.all X.A(X,m)  $@!D!D(J(e)
	$@$r$D$12C$($F$bL5L7=b!#(J
$@$J$<$J$i!"(J(e) $@$O(J realizable $@$@$+$i$G$9!#(J

(e) $@$O0l8+4qL/$K8+$($^$9$,!"$3$N$3$H$O!"(J($@301dE*$J(J)$@=89g$KBP(J$@$7$F<+A3?t$r(J
$@BP1~$5$;$k$h$&$J4X?t$G9=@.E*$J$b$N$ODj?t4X?t$7$+:n$l$J$$!"$H$$$&$3$H$+(J
$@$i$9$k$H!"<B$O<+A3(J$@$J$N$G$9!#(J

$@Dj?t4X?t$G$J$$$b$N$,:n$l$?$H$9$k$H!"(Jnot P or not not P $@$H$$$&(J 
principle $@$,F3$1$F$7$^$$$^(J$@$9!#:#!"2>$K(J f(X) =/= f(Y) $@$G$"$k$H$7$^$9!#(J
$@$=$3$G!"(JZ = {x in X | P} union {y in Y | not P} $@$HDj5A$7$F(J$@$d$j$^$9!#(J
$@<+A3?tF1;V$NEyCM@-$O7hDj2DG=$J$N$G!"(Jf(Z) = f(X) $@$+!"(Jf(Z) =/= f(X) $@$+$G(J
$@>l9gJ,$1$9$k$3$H$,$G(J$@$-$^$9!#(J
(i) f(Z) = f(X) $@$N$H$-(J: $@2>$K(J not P $@$@$H$9$k$H!"301d@-$N8xM}$K$h$j!"(JZ = Y $@$J$N$G!"(J
f(Z) = f(Y) =/= f(X) $@$H$J$C$FL7=b!#$h$C$F!"(Jnot not P.
(ii) f(Z) =/= f(X) $@$N$H$-(J: $@2>$K(J P $@$@$H$9$k$H!"301d@-$N8xM}(J$@$K$h$j!"(JZ = X $@$J$N$G!"(J
f(Z) = f(X) $@$H$J$C$FL7=b!#$h$C$F!"(Jnot P.
(i),(ii)$@$h$j!"(Jnot P or not not P $@$,F3(J$@$1$^$7$?!#(J
($@$3$3$G!"301d@-$N8xM}$rMQ$$$?$3$H!"(JP $@$,M?$($i$l$?;~$K(J {x in X | P} $@$N(J
$@$h$&$J=89g$,:n$l$k$3(J$@$H$rMQ$$$?$3$H$KCm0U$7$F2<$5$$!#FC$K!"301d@-$N8xM}(J
$@$OK\<AE*$G$9!#(J)

$@$3$N$3$H$+$i$b$o$+$k$h$&$K!"=89g$r(J$@0z?t$H$7$F<u$1$H$C$F!"2?$i$+$N7W;;$r(J
$@$9$k$h$&$J9=@.E*$J%*%Z%l!<%7%g%s$H$$$&$N$O!"$J$+$J$+9M$($K$/$$$N(J$@$G$9!#(J
($@NS?8$5$s$H;d$NK\$G07$C$F$$$k$h$&$J!"301d@-8xM}$N@.N)$7$J$$=89g$NM}O@(J
$@$G$O$^$?OC$,JL$G$9$,!#(J)

(e) $@$N$h$&$J(J principle $@$O!"(Juniformity principle $@$H8F$P$l$F$$$F!"%i%`%@(J
$@7W;;$N7?M}O@$K$*$1$k(J polymorphism $@$H?<$/4X78$7$F$$$^$9!#(J

 |$@$H$3$m$G!">e$N#2$D$N2r<a$K$D$$$F!"9M$($k$&$A$K(J
 |$@$"$k5?Ld$,@8$8$F$-$^$7(J$@$?!#(J
 |
 |V($@&8(J)$@$O!"9b3,D>4Q<g5AO@M}$N7wO@E*2r<a$H$7$F$N%H%]%9$H$_$J$;$k$N$G$7$g$&!#(J
 |($@$b$A$m$s!"%H%](J$@%9$K$D$$$F!"CN$C$F$$$k$o$1$G$O$"$j$^$;$s$,(J)
 |$@$H$$$&$3$H$G!"D>4Q<g5AO@M}$K$^$:7wO@E*$J2r<a$,$"$j$^$9!#(J
 |$@0lJ}$G$O!"0lHL$ND>4Q<g5AO@M}$h$j69$$HO0O$N$b$N$G$9$,(J
 |$@9=@.E*$JM}O@$KBP$9$k<B8=2DG=@-2r<a$,$"$j$^$9(J$@!#(J
 |$@5?Ld$H$$$&$N$O!"7wO@E*2r<a$H!"<B8=2DG=@-2r<a$H$O!"(J
 |$@$I$&$$$&4X$o$j$,$"$k$N$G$7$g$&$+$H$$$&$3$H$G(J$@$9!#(J
 |$@C<E*$K$$$($P!"(J
 |$@5"G<E*$J35G0$O!"7wO@$N$I$N$h$&$J35G0$KBP1~$9$k$+(J
 |$@$H$$$&$3$H$G$9!#(J

$@$3$l$K$D(J$@$$$F$O!"@P86$5$s$N5-;v$H!";d$NJL$N5-;v$N(J effective topos $@$NOC(J
$@$r;2>H$7$F2<$5$$!#(J
--
			$@N6C+Bg3XM}9)3X(J$@It?tM}>pJs3X2J(J    $@>.NS(J  $@Ao(J
			satoshi@whale.ryukoku.ac.jp
			0775-43-7523($@3X2J;vL3<<(J) 0775-43-7528($@8&(J$@5f<<(J)
			0775-43-7524(FAX)

$B>>K\!w?t3X2J$/$:$l$G$9!#(B

In article <SATOSHI.92Dec21153914@whale.math.ryukoku.ac.jp> satoshi@whale.math.ryukoku.ac.jp (Satoshi Kobayashi) writes:
> |$B$"!"$I$&$b$9$_$^$;$s!#(B$B7A<0<g5A$NGSCfN'$,!"ITO"7k@-$K$"$?$k$3$H$O!"$o$+$C$?(B
> |$B$N$G$9$,!"$I$&$b!"0lHL$N0LAj$KBP$7$F!"$I$&$$$&(B$B0LAj$r$H$k$H!"7A<0<g5A$N%b%G(B
> |$B%k$H$J$jF@$k$+$K$D$$$F!">/!9%-!<$,$9$Y$C$F$7$^$$$^$7$?!#$?$H$($P!"N%;6(B$B0LAj(B
> |$B$@$H!"7A<0<g5A$N%b%G%k$K$J$j$^$9!#(B

> $B$=$&$G$9$M!#N%;60LAj$J$i$b$A$m$s$=$&$J$j$^$9!#B?J,!"N%;6(B$B6u4V$K$J$i$J$$(B
> $B>l9g$G$b!"J,N%$G$-$J$$$h$&$J(B2$BE@$rF10l;k$7$F$D$V$7$?6u4V$,N%;6$K$J$k$s(B
> $B$8$c$J$$$+$J(B?$B0c$C$?$+$J(B?($B%A%'%C%/$7$F$_$F2<$5$$(B)

$B!!N%;6$NB>$K$b!"N%;6!uL)Ce$NAH$_$"$o$;$G$b!"3+=89g$NJd=89g$,$^$?(B$B3+=89g$K(B
$B$J$k$h$&$J$b$N$G$"$l$P!J$[$H$s$I(BBoole$BB+$NDj5A$KEy$7$/$J$C$F$7$^$$$^$7$?$,!K(B
$B$$$$$h$&$G$9!#$^(B$B$?>.NS@h@8$NJdB-$5$l$?@5B'3+=89g$H$$$&8+J}$b$"$j$^$9!#3N$+(B
$B$K1i;;$,B?>/0c$C$F$*$j$^$9$,!#(B

$B!!$5$i$K!"(B$B0LAj$K$3$@$o$i$J$1$l$P!"2DB,$J=89g$NB+$r$b$A$$$F!"#Z#F#C$N%b%G%k(B
$B$r$D$/$k$H$$$&J}K!$,$"$j$^$9!#(B

$B!!Fq(B$BGH!]@>B<$N!V8xM}E*=89gO@!W$N0l@a$G!"#V!J#B!K$r$3$N$h$&$K$H$i$($?$H$-$K!"(B
$B$=$NCf$G$N<B?t$O!"2DB,$J4X?t(B$B$KBP1~$9$k$H$$$&2U=j$,$"$j$^$7$?!##V!J#B!K$K$*$1(B
$B$kHyJ,J}Dx<0O@$d(B Fourier$BJQ49$K$D$$$F$O!"8&5f$N2ACM$,(B$B$"$k$H$b=R$Y$F$*$j$^$9!#(B
$B$3$N$"$?$j$OC]Fb@h@8$N8&5f$NF05!$HAjDL$:$k$b$N$,$"$k$h$&$J5$$,$7$^$9!#(B

> $B$H(B$B$3$m$G!"$3$&$$$&J8L.$G!V7A<0<g5A!W$H$$$&8@MU$r;H$&$N$O$I$&$b;d$K$O0c(B
> $BOB46$,$"$k$N$G$9$,!#!V7A<0<g5A(B$B!W$NCf?4E*$J;WA[$O(B($BBg$6$C$Q$K8@$&$H(B)$B!V7A(B
> $B<0E*$K$d$k$3$H!W$K$"$k$h$&$K;W$&$N$G!#3N$+$K7A<0<g5A$r$H$J(B$B$($?%R%k%Y%k(B
> $B%H$OGSCfN'$r<i$kN)>l$G(B Brouwer $B$H%1%s%+$7$F$^$7$?$,!#(B
> $B$3$3$NJ8L.$G$O!"!V8EE5O@M}!W$H(B$B=q$$$?J}$,NI$$5$$,$7$^$9!#(B

$B!!$=$&$G$9$M!#$3$3$G$O!"GSCfN'$,@.N)$D$+$I$&$+$H$$$&%l%Y%k$NOC$G$9$+$i(B
$BD>(B$B4Q<g5AO@M}$KBP$7$F$O!"8EE5O@M}$H$$$&$[$&$,E,@Z$G$7$?!#(B

$B!!$H$3$m$G!"(B IZF$B$N(B realizability$B$K$D$$$F$O!">\(B$B$7$$2r@b$r$7$F$$$?$@$-$^(B
$B$7$F!"$"$j$,$H$&$4$6$$$^$9!#(B 
$B!!(Brealizability$B$K$D$$$F$O!"2?$i$+$N!V<B9T2DG=$J(B$BA`:n!W!J%W%m%0%i%`$N$h$&(B
$B$J!K$H$$$&G'<1$G$7$?$N$G!"$"$"$$$&$b$N$,(B realizability interpretation$B$H(B
$B$$$&(B$B$N$O!"$?$7$+$K%T%s$H$3$J$$$b$N$,$"$j$^$9!#(B
$B!J$b$A$m$s!"J86g$r$$$C$F$$$k$o$1$G$O$"$j$^$;$s!#!K(B

> $B$3$N(B$B$3$H$+$i$b$o$+$k$h$&$K!"=89g$r0z?t$H$7$F<u$1$H$C$F!"2?$i$+$N7W;;$r(B
> $B$9$k$h$&$J9=@.E*$J%*%Z%l!<%7%g%s(B$B$H$$$&$N$O!"$J$+$J$+9M$($K$/$$$N$G$9!#(B
> ($BNS?8$5$s$H;d$NK\$G07$C$F$$$k$h$&$J!"301d@-8xM}$N@.N)$7$J$$=8(B$B9g$NM}O@(B
> $B$G$O$^$?OC$,JL$G$9$,!#(B)

$B!!?t3X20$H$$$&$h$j!"7W;;5!20$K$J$C$F$7$^$C$?:#$G$O!"#P#X$N$h$&$J$b(B$B$N$b(B
$B$=$l$J$j$K<+A3$J46$8$,$7$^$9!#%W%m%0%i%`$O!"301dE*$K$O$H$i$($K$/$$$b$N(B
$B$G$9$+$i!#(B

$B!!$5$F!"$3$NOC(B$BBj$b$+$J$j9b>0$J$b$N$K$J$C$F$^$$$j$^$7$?!#;d$OITJY6/$N7j$r(B
$BKd$a$k$Y$/!"G/KvG/;O$O!"$I$3$+$N;3$NCf$X$G(B$B$bO6$C$FJY3X$KNe$`=jB8$G$9$N$G(B
$B!"EvJ,(Bfj.sci.math$B$H$O$*$5$i$P$$$?$7$^$9!#(B(^^;)

$B!!>.NS@h@8$r$O$8$a!"%U(B$B%)%m!<$7$F$$$?$@$$$?3'MM!"(B
  $B$"$j$,$H$&$4$6$$$^$7$?!#(B

$B!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](B$B!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](B
$B!!!!!!!!!!E4E4E4E4!!!!!!>>K\??8c(B (Shingo Matumoto)$B!!!!!!!!!!!!!!!!!!(B$B!!!!!!!!!!(B
$B!!!!!!!!!!E4!!!!!!E4!!!!(Bshingo@ipc02.rtri.or.jp$B!!!!!!!!!!!!!!(B $B!!!!!!!!!!!!!!!!(B
$B!!!!!!!!!!E4(B$B!!E4E4!!!!!!")#1#8#5!!El5~ET9qJ,;{;T8wD.#2!]#8!]#3#8!!!!!!!!!!!!!!(B
$B!!E4!!!!!!E4!!!!E4!!!!!!E4F;Am9g5;(B$B=Q8&5f=j!!M"Aw%7%9%F%`I>2A8&5f<<!!!!!!!!!!!!(B
$B!!!!E4E4E4!!!!!!!!E4!!!!#0#4#2#5!]#7#3!]#7#3#0#6!!!!!!!!(B$B!!!!!!!!!!!!!!!!!!!!!!(B
$B!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](B