NetNews Usenet Archive 1992 #31/NN_1992_31.iso/spool/fj/sci/math/853

Internet Message Format | 1992-12-21 | 5.9 KB

Path: sparky!uunet!stanford.edu!sun-barr!sh.wide!wnoc-kyo!rinsgw!rins!satoshi
From: [e-mail] (Satoshi Kobayashi)
Newsgroups: fj.sci.math
Subject: Re: IZF (Re: Q in int. math.)
Message-ID: <[e-mail]>
Date: 21 Dec 92 07:48:00 GMT
References: <[e-mail]> <[e-mail]>
Sender: [e-mail]
Distribution: fj
Organization: Ryukoku Univ., Seta, Otsu, Japan
Lines: 100
In-reply-to: [e-mail]'s message of 15 Dec 92 08:46:17 GMT

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

In article <[e-mail]> [e-mail] (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
            [e-mail]
            0775-43-7523($@3X2J;vL3<<(J) 0775-43-7528($@8&(J$@5f<<(J)
            0775-43-7524(FAX)