🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: fj.sci.math
Article #265

Re: Q in intuitionistic math.

#265
From: Shingo MATSUMOTO
Date: Mon, 16 Nov 1992 03:07
81 lines
4031 bytes
$@>>K\!wE4F;Am8&(J

In article <RYU.92Nov14014631@sysipk.sys.titech.ac.jp> ryu@sys.titech.ac.jp (ryu) writes:
> $@$K$7$F$b!VH=Dj$G$-$J$$!J#4$D$G$"$k$H$$$&!K$3$H!"$rM}2r$7$?!W$H$O!)(J

$@0J2<;2>H!#(J

 |> z in y -> z in {0,1} $@$rK~$?$9(J y $@$,%?%"%"%"%/%5%s!V:_$k!W$+$i$8$c$"$J$+$C(J
 |> $@$?$C$1!)$H$$$&$N$,!"$=$b$=$b8@$$$?$+$C$?$3$H$G$9!#(J
 |> $@!t:G=i$C$+$i$3$&8@$($PNI$+$C$?$s$@!#(J
 |
 |$@$?$/$5$s$J$s$+$J$$$h!#$=$l$3$=!V8m2r!W(J

> $@$($($H!"(J{0} $@$N(J V^$@&8(J $@$X$NKd$a9~$_$r(J {0}' $@$H$7$^$9$M!#(J
> A $@$r(J A(0) $@$,#1$K$J$i$J$$$@$1$G$=$NB>$O(J {0}' $@$HF1$8%b%N$@$H$7$^$9$M!#(J
> $@$9$k$H!"(J
> [x in A] = A(0) cup [x=0] $@$G(J [x in {0}'] = 1 cup [x=0] $@$G$9$h$M!#(J
> $@$9$k$H!"(J
forall x [x in A -> x in {0}'] = 1 $@$K8+$($^$;$s$+!)(J
> $@$G$b$C$F#1$G$b$$$$$s$G$7$g!#$=$&$$$&0UL#$G$b%V!<%kCM%b%G%k$H0l=o$J$s$G(J
> $@$7$g!)(J
> $@$b$C$H$b!V0lHL$K$O#1$K$J$i$J$$!W$N$G$7$g$&$,!#(J

$@!)>e$NJ8>O$N0UL#$,$h$/$o$+$i$s$,!#(J

$@!!$H$$$&$3$H$G!";d$J$j$K@0M}$7$^$7$?!#(J
1.$@$^$:!"(Jx$@$,(J{},{0},{1},{0,1}$@$N$I$l$+$KEy$7$$$H$9$l$P(J
$@!!(Jx$@$,(J{0,1}$@$NItJ,=89g$G$"$k$H$$$&$N$O(J
$@!!$I$s$J%b%G%k$G$b??56CM$O#1(J

2.$@<!$K!"(Jx$@$,(J{},{0},{1},{0,1}$@$N$I$l$G$b$J$1$l$P(J
$@!!(Jx$@$,(J{0,1}$@$NItJ,=89g$G$"$k$H$$$&$N$O(J
$@!!$I$s$J%b%G%k$G$b??56CM$O#0(J

3.$@<B$O!">e$N#2$D$N$[$+$K(J1.$@!"(J2.$@$N$I$A$i$G$b$J$$!"$9$J$o$A!"(J
$@!!(Jx$@$,(J{},{0},{1},{0,1}$@$N$I$l$+$G$"$k$+!"$G$J$$$+$o$+$i$J$$(J
$@!!$H$$$&>l9g$,$"$k!#(J
$@!!$3$N>l9g(J
$@!!(Jx$@$,(J{0,1}$@$NItJ,=89g$G$"$k$H$$$&$N$O(J
$@!!%b%G%k$K$h$C$F??56CM$O$3$H$J$k!#(J

$@!!$@$+$i!"%b%G%k$K$h$C$F$O(J
$@!!(J3.$@$N$h$&$J(J x$@$K$D$$$F(J
$@!!??56CM$,#1$G$"$k$H$9$l$P(J
 $@!V%?%/%5%s!W$"$k$h$&$K$_$($k!#(J

$@!J$A$J$_$K(J3.$@$K$"$?$k(Jx$@$O8EE5=89gO@>e$G$OB8:_$7$J$$$b$N$G$"$k$+$i(J
$@!!6qBNE*$K$"$k(Jx$@$,$"$C$F!"$=$l$,(J{0,1}$@$NItJ,=89g$G$"$k$H$$$&$3$H$H(J
$@!!$O$A$g$C$H$3$H$J$k!#!K(J

$@!!$b$A$m$s!"B>$N%b%G%k$G$O#1$G$J$$$3$H$,$"$k$o$1$G(J
$@!!$=$&$$$C$?4QE@$+$i$9$l$P!"G$0U$N%b%G%k$G#1$H$J$k>l9g0J30$N(J
$@!!FC<l$JNc$K$D$$$F9M$($k$N$O!"0UL#$,$J$$!#(J

$@!!MWE@$H$7$F(J
1.$@#4$D0J30$K??56CM$,#1$H$J$k%b%G%k$,$"$k$N$G(J
$@!!#4$D$G$"$k$3$H$O>ZL@$G$-$J$$!#(J
2.$@$7$+$7$J$,$i!"G$0U$N%b%G%k$G??56CM$,#1$K$J$k$N$O(J
$@!!#4$D$7$+$J$$!#(J
$@!!$H$$$&$3$H$G$9$M!#(J
$@!!$@$+$i#4$D$G$"$k$H>ZL@$G$-$J$$$o$1$G$9$M!#(J

 |> $@!t$*<j?t$r$*$+$1$7$F$*$j$^$9$,!"$^$"!"$3$l$b!V9=@.<g5A?t3X$NIa5Z$N$?$a!W(J
 |> $@!t$@$H;W$C$F$$$?$@$1$l$P!"!"!"(J
 |
 |$@FbMF$+$i$9$k$H!"$H$F$b$=$&$O$*$b$($s$,!#(J(^^;)

> $@$=$G$9$M!#(J

> $@$G!":#EY$3$=!"%[%s%H$K:#EY$3$=!"??LLL\$J<ALd!#(J
> $@JL$K(J V^$@&8(J $@$C$F!V40A4!W$8$c$"$J$$$s$G$7$g!)(J

$@40A4$@$C$?$i!"D>4Q<g5A$O$$$i$J$$$N$G$O!#(J(^^;)

$@!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](J
$@!!!!!!!!!!E4E4E4E4!!!!!!>>K\??8c(J (Shingo Matumoto)$@!!!!!!!!!!!!!!!!!!!!!!!!!!!!(J
$@!!!!!!!!!!E4!!!!!!E4!!!!(Jshingo@ipc02.rtri.or.jp$@!!!!!!!!!!!!!!(J $@!!!!!!!!!!!!!!!!(J
$@!!!!!!!!!!E4!!E4E4!!!!!!")#1#8#5!!El5~ET9qJ,;{;T8wD.#2!]#8!]#3#8!!!!!!!!!!!!!!(J
$@!!E4!!!!!!E4!!!!E4!!!!!!E4F;Am9g5;=Q8&5f=j!!M"Aw%7%9%F%`I>2A8&5f<<!!!!!!!!!!!!(J
$@!!!!E4E4E4!!!!!!!!E4!!!!#0#4#2#5!]#7#3!]#7#3#0#6!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!(J
$@!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!]!](J
Technical Details
Message-ID: <530@keu02.rtri.or.jp>
Path: arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!sun-barr!sh.wide!wnoc-kyo!kyu-cs!lab!utogw!sectrl!keu02!ipc02!shingo
References: <526@keu02.rtri.or.jp> <RYU.92Nov14014631@sysipk.sys.titech.ac.jp>

Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!sun-barr!sh.wide!wnoc-kyo!kyu-cs!lab!utogw!sectrl!keu02!ipc02!shingo
From: shingo@ipc02.rtri.or.jp (Shingo MATSUMOTO)
Newsgroups: fj.sci.math
Subject: Re: Q in intuitionistic math.
Message-ID: <530@keu02.rtri.or.jp>
Date: 16 Nov 92 03:07:03 GMT
References: <526@keu02.rtri.or.jp> <RYU.92Nov14014631@sysipk.sys.titech.ac.jp>
Sender: news@keu02.rtri.or.jp
Reply-To: shingo@ipc02.rtri.or.jp (Shingo MATSUMOTO)
Distribution: fj
Organization: Railway Technical Research Institute
Lines: 81