Article View: fj.sci.math
Article #14333Re: Q in intuitionistic math.
From: Satoshi Kobayashi
Date: Thu, 03 Dec 1992 11:18
Date: Thu, 03 Dec 1992 11:18
80 lines
5359 bytes
5359 bytes
$@>.NS(J@$@N6C+Bg3X$G$9!#(J
In article <RYU.92Dec2142853@sysipi.sys.titech.ac.jp> ryu@sys.titech.ac.jp (ryu) writes:
| | |$@$3$l$OA4A3OC$7$,D7$s$8(J$@$c$C$F(J $@&X(J-$@L5L7=b$NOC$7$G$O$J$$$G$7$g$&$+!#(J
| |
| |\Omega $@L5L7=b$NOC$H$b$A$g$C$H0c$$$^$9$M!#(J
|
|$@!t(J\omega $@$G$7$g!)(J
$@$"!"$7$^$C$?!#$3$J$$$@$+$i(J\Omega $@$P$+$j2?EY$b%?%$%W$7$F$$$?$N$G!"$&$C(J
$@$+$j4V0c$($F$7(J$@$^$$$^$7$?!#(J
|$@$s!<$H!"$9$Y$F$N(J x $@$K$D$$$F(J p(x) $@$J$s$@$1$I(J $@"O(Jx p(x) $@$G$O$J$$!"$H$$$&(J
|p $@$O$"$j$^$9(J$@$h$M!#$=$NJ}$,<+A3$K2r<a$G$-$?$s$G$9$,!#(J
$@$3$3$N=j$O$A$g$C$H4qL/$G$9$M!#$3$l$O!"$9$Y$F$N(J x $@$K$D$$$F(J [p(x)] = 1
$@$@$,(J [all x.p(x)] $@!b(J 1$@$H$$$&0UL#$G$7$g$&$+!#$=$&$$$&0UL#$@$H$9$k$H!"$=(J
$@$&$$$&$3$H$O7h$7$F$"(J$@$jF@$J$$$G$9$,!#(J
| |$@$=$&$$$&%b%G%k$O<B:]$K:n$l$^$9!#(J\Omega $@$r(J [0,1] $@$NDL>o$N0LAj$K$h$k3+=8(J
| |$@9g7O(J$@$H$7$F!"(JV^(\Omega) $@$r9M$($^$9!#(JV^(\Omega) $@$K$*$1$k(J($@%G%G%-%s%H%+%C(J
| |$@%H$K$h$k(J)$@<B?t$O!"(JV $@$K$*$1$k(J [0,1] $@$+$i(J R $@$X$NO"B34X?t$KBP1~$7$^$9!#$=(J
| |$@$3$G!"(J[0,1] $@>e$N(J identity function id$@$KBP1~$9$k(J V^(\Omega) $@$N<B?t(J id~
| |$@$r9M$(!"(JP(x) $@$O(J x < id~ or x > id~ $@$H$9$l$P$h$$$N$G$9!#(J
|
|$@$7$^$C$?$"!<!"$=$&$+!#(J
|$@D>4Q<g5A$N=g=x?t$G$O(J
|a \notin b $@$+$D(J b \notin a $@"M(J a=b
|$@$,@.$jN)$?$J$$$s$@$"$"$"$"!#%9%2%(4JC1$@(J$@$C$?$s$C$@!#(J
$@$"$l(J? $@;d$N$"$2$?Nc$O=g=x?t$H$O4X78$J$$$N$G$9$,!#$R$g$C$H$7$F(J '<' $@$r=g(J
$@=x?t$NBg>.4X78$@$H(J$@;W$o$l$?$N$G$7$g$&$+!#<B?t$NBg>.4X?t$N$D$b$j$@$C$?$N$G$9$,!#(J
$@85!9!">>K\$5$s$,(J
|$@$I$&$7$F>e$N$h$&$J$3$H(J$@$r;W$$IU$$$?$+$H$$$&$H(J
|$@>e$N<0$r&8$,(J[0,1]$@$H$7$F!"%b%G%k>e$G9M$($F(J
|x$@$,M-M}?t>e$rF0$-(J
||P(x)|$@$,M-M}(J$@?t$r=|$$$?3+=89g$@$H$9$k$H!"(J
||P(x)|$@$N6&DL=89g(J($@L5M}?t$N=89g(J)$@$N3+3K(J($@6u=89g(J)$@$N:9=89g$N3+3K$O(J[0,1]$@A4BN(J
||P(x)|$@$N:9=89g(J($@0lE@(J)$@$N3+3K(J($@6u=89g(J)$@$NOB=89g$O6u=89g(J
|$@$H$J$j$^$9$N$G!"<B:]$K(JP(x)$@$rDj5A$G$-$l$P!"LLGr(J$@$$$H$*$b$C$?$o$1$G$9!#(J
$@$H$$$&$3$H$r=q$+$l$?$3$H$+$i;O$^$C$?OC$J$N$G!">>K\$5$s$N9M$($?$h$&$K(J x
$@$,M-M}(J$@?t$rF0$/$H$7$F!"(J|P(x)| = [0,1] - {x} $@$H$J$k$h$&$JNc$r:n$C$F$_$?(J
$@$i!"$3$&$$$&Nc$K$J$j$^$7$?!#$=$N8e$G$"(J$@$2$?JL$NNc$G$O!"(Jx $@$,M-M}?t$rF0$/(J
$@$h$&$K$7$^$;$s$G$7$?$,!#(J
$@$G$b!"$b$A$m$s!"=g=x?t$rMQ$$$?Nc$b:n$l$k$H(J$@;W$$$^$9$,!#(J
|$@$G$b$3$3$^$G8+$F$/$k$H!VD>4Q<g5AO@M}BN7O!W$H$$$&$b$N$O!V=89gO@$rE83+$9(J
|$@$k$K$?$j$kBN(J$@7O!W$H$OE~Dl;W$($J$/$J$C$F$-$?$s$G$9$,!#(J
$@$=$s$J$3$H$b$J$$$H;W$$$^$9$h!#8EE5E*$J=89g$NM}O@$GF3$1$k$h$&(J$@$JDjM}$HF1(J
$@MM$NDjM}$r4|BT$9$k$H!"$J$s$@!"$3$l$O!"$H$$$&$3$H$K$J$k$+$bCN$l$^$;$s$,!"(J
$@9=@.E*?t3X$K$*$$$F(J$@$O=89g$N0UL#$,8EE5E*$J=89gO@$N>l9g$H$O0c$&$s$@!"$H;W(J
$@$($P!"D>4Q<g5AO@M}>e$N=89g35G0$b$^$H$b$J$b$N$K8+(J$@$($F$-$^$9!#(J
$@!V8EE5E*$J=89gO@$rE83+$9$k$K$?$j$kBN7O!W$G$O$J$$$1$I!"!V9=@.E*$J=89gO@(J
$@$rE83+$9$k$K$?$j(J$@$kBN7O!W$J$s$G$9$h(J :-) $@$=$l$8$cEv$?$jA0$@$C$F(J? $@$G$bBg(J
$@;v$J$N$O!"9=@.E*$J=89gO@$H$$$&$N$b!"$A$c$s$H0UL#(J$@$N$"$kM}O@$K$J$C$F!"<B(J
$@:]E*$J$3$H$KLr$KN)$D5DO@$,E83+$G$-$k!"$^$H$b$J(J($@8&5f$9$k$KCM$9$k(J)$@M}O@$K(J
$@$J$s$G$9(J$@!#(J
|$@$5$b$J$/$P$d$O$j!V=89g$G$J$$$b$N!W$b<h$j07$o$J$$$H!"!"!"(J
|$@!t$3$3$G$$$&=89g$O%+%s%H!<%k$NDj5A$H(J$@$G$b;W$C$F2<$5$$!#(J
$@!V=89g$G$J$$$b$N!W$H$$$&$N$O!"2?$r;X$7$F$*$C$7$c$C$F$$$k$N$G$7$g$&(J?
$@%"%H%`$r;}$D=8(J$@9gO@$r9M$($k$H$$$&$3$H$G$7$g$&$+(J?
$@<B$O!"9=@.E*?t3X$NBgDq$NM}O@$G$O!"=89g$G$J$$$b$N$r07$$$^$9!#$3$NE@(J$@$G!"(J
IZF $@$ONc30E*$G$9!#(J(IZF $@$K%"%H%`$rF~$l$F$"$kK\$b$"$k$,!D!#(J)$@$@$C$F!"(J($@8D!9(J
$@$N(J)$@<+A3?t$H$+M-M}?t$H$+$,(J$@=89g$@$J$s$F!"IaDL$N?t3X<T$b$U$@$s$=$s$J$3$H(J
$@;W$C$A$c$$$J$$$7!"$=$s$J$U$&$K$J$s$G$b$+$s$G$bL5M}$d$j=8(J$@9g$GDj5A$9$k$J(J
$@$s$FIT<+A3$G$7$g$&(J? $@IaDL!"9=@.E*?t3X$G$O!"<B?t$r=89g$r;H$o$:$KDj5A$7$^(J
$@$9!#$7$D$3$$$h$&(J$@$G$9$,!"(JIZF $@$r8+$FJQ$@$H;W$o$l$?$H$7$F$b!"JQ$J$N$OD>4Q(J
$@<g5AO@M}$8$c$J$/$F!"(JIZF $@$,FC<l$J$s$@$H;W$C$F2<(J$@$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)
Technical Details
Message-ID:
<SATOSHI.92Dec3201827@whale.math.ryukoku.ac.jp>Path:
arc1-ca.pugleaf.net!sparky!uunet!ccut!sh.wide!wnoc-kyo!rinsgw!rins!satoshiReferences:
<526@keu02.rtri.or.jp> <RYU.92Nov14014631@sysipk.sys.titech.ac.jp> <530@keu02.rtri.or.jp> <RYU.92Nov17082028@sysipk.sys.titech.ac.jp> <544@keu02.rtri.or.jp> <SHINGO.92Nov27194549@ipc02.rtri.or.jp> <RYU.92Nov28090325@sysipk.sys.titech.ac.jp> <SATOSHI.9Show Full Headers
Complete Article Headers
X-Google-Language: Japanese,JIS X-Google-Thread: f4956,8af676e5bd3e6401 X-Google-Attributes: gidf4956,public X-Google-ArrivalTime: 1992-12-03 03:28:54 PST Path: arc1-ca.pugleaf.net!sparky!uunet!ccut!sh.wide!wnoc-kyo!rinsgw!rins!satoshi From: satoshi@whale.math.ryukoku.ac.jp (Satoshi Kobayashi) Newsgroups: fj.sci.math Subject: Re: Q in intuitionistic math. Message-ID: <SATOSHI.92Dec3201827@whale.math.ryukoku.ac.jp> Date: 3 Dec 92 11:18:27 GMT References: <526@keu02.rtri.or.jp> <RYU.92Nov14014631@sysipk.sys.titech.ac.jp> <530@keu02.rtri.or.jp> <RYU.92Nov17082028@sysipk.sys.titech.ac.jp> <544@keu02.rtri.or.jp> <SHINGO.92Nov27194549@ipc02.rtri.or.jp> <RYU.92Nov28090325@sysipk.sys.titech.ac.jp> <SATOSHI.9 Sender: news@rins.ryukoku.ac.jp Distribution: fj Organization: Ryukoku Univ., Seta, Otsu, Japan Lines: 80 In-reply-to: ryu@sys.titech.ac.jp's message of 2 Dec 92 05:28:53 GMT