🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: fj.sci.math
Article #14352

Re: Q in intuitionistic math.

#14352
From: Satoshi Kobayashi
Date: Tue, 08 Dec 1992 09:29
88 lines
6000 bytes
$@>.NS(J@$@N6C+Bg3X$G$9!#(J

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

 |>   $@$5$b$J$/$P(J$@$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$G$b;W$C$F2<(J$@$5$$!#(J
 |
 |$@$=$&GyA3$H$$$o$l$F$b$M$(!#(J
 |($@$b$7!V%U%!%8!<!W$K$D$$$F8@$o$l$F$$$k$N$G$7$?$i!"JL$KD>4Q<g5A(J$@$G$J$/$F$b(J
 |$@7A<0<g5A$G$b!V%U%!%8!<!W$JO@M}$O$"$j$^$9!#MW$OCf4VCM$r??56CM$K$b$D$h$&(J
 |$@$J$b$N$J$i$P!"$=(J$@$N??56CM$NB+$K1~$8$?%U%!%8!<O@M}$,$"$k$o$1$G$7$F!"$3$l$O(J
 |$@;d$N0U8+$G$O$J$/$F!"C]Fb30;K;a(J($@$7$+$7$$$m$$(J$@$m$J$H$3$m$K$G$F$/$k$J$"(J^^;)
 |$@$,!V?t%;%_!W$G$$$C$F$*$j$^$9!#(J)

$@$?$@!"C]Fb@h@8$N8@$C$F$*$i$l$k%U%!%8!<(J$@$H$$$&$N$O!"IaDL$K%U%!%8!<$r$d$C(J
$@$F$$$k?MC#$,9M$($F$$$k%U%!%8!<$H$O$+$J$j0c$&46$8$,$7$^$9$1$I$M!#(J

 |$@;d$H$7$F$O!"8=:_$N(J($@=89gO@0J30$N(J)$@?t3X$G$O!"$"$^$j6/NO$JBN7O$OI,MW$G$J$$(J
 |$@5$$,$7$^$9!#:G6aN.9T$N!V5U?t(J$@3X!W$K$h$l$P!"Bg35$N?t3X$K$*$1$kDjM}$O#23,(J
 |$@$N;;=Q$NBN7O$G==J,$G!"<B?t$NG;EY$h$jBg$-$J=89g$J$s$F$^$:(J$@IaDL$OMQ$$$J$$!#(J

$@$=$&$G$9$M!#(J2$@3,$G!"$7$+$b!"(Jcomprehension axiom $@$rAjEv<e$$7A$K@)8B$7$?(J
$@BN7O$G$b$+$J$j(J$@$N$3$H$,>ZL@$G$-$k$H$$$&$3$H$,!"5U?t3X$N8&5f$K$h$C$F$o$+$C(J
$@$F$$$k$h$&$G$9!#(J($@;d$OA4A3$/$o$7$/$J$$$G$9$,(J$@!#(J)

$@@)8B$J$7$N(J($@=>$C$F$b$A$m$s(J impredicative $@$J(J)comprehension $@$r;}$D(J2$@3,$N;;(J
$@=Q$GBgDq$N?t3X$,E83+$G$-$k(J$@!"$H$$$&$N$O!"$b$A$m$s5U?t3X$h$j0JA0$N$:$C$H(J
$@@N$+$i$o$+$C$F$$$^$9$7$M!#(J

 |$@A*Br8xM}$K$7$?$C$F!"2D;;$N(J$@$b$N$G!"BgDq$O4V$K9g$$$^$9!#(J

$@$=$&$G$9$M!#$5$i$K!"0MB8A*Br8xM}$,$"$l$P!"$[$H$s$I(J OK $@$G$9$M!#$3$l$O!"(J
$@%Y%k%J%$%9$"$?$j$,D4$Y$F$$$?$O$:$G$9!#$4B8$8$NDL$j!"0MB8A*Br8xM}$+$i2D(J
$@;;A*Br8xM}$,F3$1$^$9!#(J

 |$@0lJ}(J$@!"L5L7=b@-$K$D$$$F$O%2%s%D%'%s$N<+A3?tO@$K$D$$$F$N>ZL@0JMh!"L\I8$H(J
 |$@$7$F$O2r@O(J($@<B?tO@(J)$@$NL5L7=b@-$N>Z(J$@L@$H$$$&$N$,$"$j!"$3$l$K$D$$$F$O!VC]Fb(J
 |$@$N4pK\M=A[!W$G!"9b3,(J($@#23,(J)$@O@M}$K$h$k%+%C%H=|5n$r9=@.E*$K>ZL@(J$@$G$-$l$P!"(J
 |$@2r@O$NL5L7=b@-$,8@$($k$H$$$&$3$H$G$9!#!VC]Fb$N4pK\M=A[!W$O%b%G%kO@E*$K(J

$@$3$3$N=j$K>/$7%3(J$@%a%s%H$,$"$j$^$9!#(J

$@$^$:!">>K\$5$s$K!"$H$$$&$h$j$O!"0lHL$NFI<T$NJ}!9$N$?$a$NJdB-!#9b3,(J(2$@3,(J)
$@;;=Q$r2r@O(J(analysis)$@$H8F$V$N$O!"?t3X4pACO@20$5$s$,>!<j$K$D$1$?8F$SJ}$G!"(J
$@8=<B$K?t3X<T$,8&5f$7$F$$$k2r@O3X$K$A$g(J$@$&$IBP1~$9$kM}O@$@!"$H$$$&$o$1$G(J
$@$O$"$j$^$;$s!#8=:_$N2r@O3X$NBgDq$NDjM}$,>ZL@$G$-$k$O$:$@!"$H$$$&$3$H(J$@$G(J
$@$=$&$$$&L>A0$K$J$C$F$$$k$N$G$7$g$&$,!#(J

$@<!$K!"9b3,O@M}$N%+%C%H=|5n$r!V9=@.E*!W$K>ZL@$G$-$l$P2r@O$N(J$@L5L7=b@-$,8@(J
$@$($k!"$H$$$&$/$@$j$K$D$$$F!#8@$o$l$F$$$k$3$H$K4V0c$$$O$J$$$N$G$9$,!">/(J
$@$7$P$+$j;d$N0U8+$r(J$@!D!#(J
  $@$^$:!"!V9=@.E*!W$H=q$+$l$?$N$O!"(J($@GSCfN'$&$s$L$s$NOC$H$$$&$h$j$O!"(J)$@C](J
$@FbN.$NM-8B$NN)>l$K4p$E$/(J reduction method $@$G!"$H$$$&0UL#$@$H;W$$$^$9$N(J
$@$G!"0J2<$=$N$D$b$j$G=q$-$^$9$,!">ZL@$,!V9=@.E*!W$G$"$m$&(J$@$,$J$+$m$&$,!"(J
$@%+%C%H=|5n$,>ZL@$G$-$l$P2r@O$NL5L7=b@-$O8@$($k$H;W$$$^$9!#$"$^$jC]FbN.(J
$@$K$3$@$o$i$J$/$F(J$@$b$$$$$s$8$c$J$$$+$J!"$H;d$O;W$C$F$$$^$9!#(J($@$D$$$G$K8@(J
$@$&$H!"%+%C%H=|5n0J30$NJ}K!$GL5L7=b@-$r>ZL@$7$F$b(J$@$$$$$o$1$G$9$7!#(J)
$@$H$$$&$o$1$J$N$G!"(J

 |$@$$$($k$N$G$9$,!"$=$l$OHs9=@.E*$J$N$G!"$$$^$@2r@O$NL5L7=b@-$O>Z(J$@L@$5$l$F(J
 |$@$$$^$;$s!#<B?tO@$K$D$$$F$9$i!"$=$&$$$&>u67$G$9$+$i!"$`$7$m(JIZF$@$h$j<e$/(J

$@Hs9=@.E*$G$"$C$F$b!"(J$@$b$C$H$b$i$7$$>ZL@$,$"$l$P(J($@$=$l$r?.$8$k8B$j(J)$@L5L7=b(J
$@@-$O>ZL@$5$l$?$H9M$($l$P$$$$!"$H;d$O;W$$$^$9!#C]Fb(J$@M=A[$N%b%G%kO@E*$J>Z(J
$@L@$,!"2r@O$NL5L7=b@->ZL@$H$7$F8+$?;~$K$b$C$H$b$i$7$$$+$I$&$+$O!"$^$?JL(J
$@$NOC$G$9$,(J$@!#;d<+?H$O!"2r@O$NL5L7=b@-$K$OJL$KLdBj$O$J$$$H;W$C$F$$$^$9!#(J

$@$$$d!"$I$&$b!">>K\$5$s$NOC$NCf?4E*$J<gD%(J$@$H$O%:%l$?$h$&$J%3%a%s%H$P$+$j(J
$@$7$FOC$rC&@~$5$;$F$9$_$^$;$s!#$7$+$b!"%1%A$P$+$j$D$1$F$$$k$h$&$J46$8$G(J$@!#(J
$@0-5$$O$J$$$s$G$9$1$I!"$I$&$b:Y$+$$;v$P$+$j5$$K$J$k%?%A$G$7$F!"$+$s$Y$s(J
$@$7$F2<$5$$!#(J

$@>>K\$5$s$N<gD%(J$@$NA4BNE*$J<g;](J($@B?J,!"2<$K0zMQ$7$?$h$&$J$3$H$r<g$K8@$o$l(J
$@$?$+$C$?$N$@$H;W$$$^$9$,(J)$@$K$D$$$F$O!";d$OA4$/(J$@;?@.$G$9!#(J

 |$@$F$b!"$b$C$H9=@.E*$JM}O@$G!"2r@O$J$I$,E83+$G$-$kJ}$,LLGr$$(J($@$9$/$J$/$H(J
 |$@$b!"%"%k%4%j%9%`(J$@Ey$K$D$$$F$OF@$k=j$,Bg$-$$(J)$@$H;W$$$^$9!#(J

$@<B$O!"(JBishop style $@$N9=@.E*2r@O3X$K$D$$$F$O!"Hs>o$K<e$$M}O@$G(J$@$b==J,$@(J
$@$H9M$($i$l$F$$$F!">ZL@O@E*$J6/$5$,%Z%"%N;;=Q$HF1$8$/$i$$$7$+$J$$M}O@$G(J 
OK $@$N$h$&$G$9!#(J($@5U$K(J$@9M$($k$H!"%Z%"%N;;=Q$C$F7k9=6/NO$J$s$G$9$h$M!#$I$&(J
$@$bIaDL$N?t3X<T$K$O!"%Z%"%N;;=Q$H$$$&$N$O!"$4$/4JC1(J$@$J;;=Q$7$+$G$-$J$$$H(J
$@;W$C$F$$$k?M$,$$$k$h$&$G$9$1$I!#(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.92Dec8182903@whale.math.ryukoku.ac.jp>
Path: arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!sun-barr!sh.wide!wnoc-kyo!rinsgw!rins!satoshi
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

Show 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-08 01:42:41 PST
Path: arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!sun-barr!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.92Dec8182903@whale.math.ryukoku.ac.jp>
Date: 8 Dec 92 09:29:03 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: 88
In-reply-to: shingo@ipc02.rtri.or.jp's message of 4 Dec 92 05:41:53 GMT