🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: fj.sci.math
Article #14317

Re: Q in intuitionistic math.

#14317
From: Satoshi Kobayashi
Date: Mon, 30 Nov 1992 10:09
69 lines
3646 bytes
$@>.NSAo(J@$@N6C+Bg3X$G$9!#(J

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

 |{0,1}$@$N$Y$-=89g$N7o(J$@$G$9$,(J
 |$@>.NS@h@8$N!V9=@.E*%W%m%0%i%_%s%0$N4pAC!W$G!"(J
 |$@4X?t6u4V(JA->Bool$@$H(JA$@$N$Y$-%/%i%9$N0c$$(J
 |$@$H$$$&(J$@9`L\$,$"$j$^$7$F!"$3$l$rFI$a$P(J
 |$@0lL\NFA3$G$7$?!#(J
 |($@Cp!'>e$N(JBool$@$O(Jtrue,false$@$h$j$J$k%/%i%9(J)

($@CfN,(J)

 |b$@$,(Ja$@$NItJ,%/%i%9$H$7$F(J
 |$@$"$k(Jf:A->Bool$@$r$H$C$F(J
 |f_inverse({true})$@$H(Jb$@$,F1$8301d$r$b$D$H$O$+$.$i$J$$(J
 |$@$H$$$&$3$H$G!"$?$H$($P!"8EE5=89gO@$G$O(J
 |f(x)= true (x in b)
 |    = false (Not(x in b))
 |$@$G>l9gJ,(J$@$1$9$k$3$H$G!"(Jb$@$KBP1~$9$k(Jf$@$,$D$/$l$^$9$,(J
 |$@D>4Q<g5A$G$OGSCfN'$,;H$($J$$$N$G(J
 |$@$$$D$b(Jf$@$,B8:_$9$k$H$O8B(J$@$i$J$$$?$a$H$$$&$3$H$G$9!#(J
 |
 |$@%/%i%9$r=89g$HFI$_BX$($l$P!"F1$8$3$H$,$$$($k$G$7$g$&!#(J

$@$^$"!"$=$&$$$&(J$@$3$H$G$9!#$?$@$7!"!V9=@.E*%W%m%0%i%_%s%0$N4pAC!W$G07$C$F(J
$@$$$k%/%i%9$H$$$&$d$D$O!"301dE*$G$O$J$$=89g35(J$@G0$J$N$G!"$A$g$C$H$@$1Cm0U(J
$@$,I,MW$G$9$1$I!#Nc$($P!"6u$J%/%i%9$,L58B$K$"$C$?$j$9$k!#$3$l$O!"301dE*(J
$@$K$O(J$@Ey$7$/$F$bFbJq$,Ey$7$/$J$$%/%i%9$,$?$/$5$s=P$F$/$k$+$i$G$9!#(J

 |$@!t6571(J
 |$@!tI42s$NEj9F$h$j0l2s$NFI=q(J(^^;)

 |$@$5$F!"<ALd$J$N$G$9$,(J
 |$@&8$H$7$F0LAj6u4V$N3+=89g$NB+$r$H$k$H$7$^$9!#(J
 |$@3+=89g$OM-8B2s$N6&DL=89g(J$@$HG$0U2s$NOB=89g$NA`:n$G3+=89g$N>r7o$rJ]$A$^$9$,(J
 |$@$3$l$r;H$C$FLLGr$$Nc$r9M$($F$_$^$7$?!#(J
 |$@Nc$($P(J
 |Not(All x (P(x))) = 1
 |$@$G(J
 |Exist x (Not (P(x))) = 0
 |$@$H$J$k$h$&$J(JP(x)$@$O<B:]$K$"$k$N$G$7$g$&$+!#(J
 |
 |$@$I$&$7$F>e$N$h$&$J$3$H$r;W$$IU$$$?$+$H$$$&$H(J
 |$@>e$N<0$r&8$,(J[0,1]$@$H$7$F!"%b%G%k>e$G9M$($F(J

$@$3$l$O!"(J$@$b$A$m$s!"(J\Omega $@$,(J($@DL>o$N0LAj$K$h$k(J)$@0LAj6u4V(J [0,1] $@$N3+=89g7O(J
$@$H$$$&0UL#$G$9$h$M!#(J

 |x$@$,M-M}?t>e$rF0(J$@$-(J
 ||P(x)|$@$,M-M}?t$r=|$$$?3+=89g$@$H$9$k$H!"(J

$@$3$l$O!"M-M}?t(J x $@$r=|$$$?3+=89g!"$H$$$&$3$H$G$9$M(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
                                                ^^^^^^
$@$3$l$O(J([0,1] $@$rA46u4V$H$7$?$H$-$N(J)$@Jd=89g$H$$$&$3$H$G$9$+(J?

 ||P(x)|$@$N:9=89g(J($@0l(J$@E@(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$$$H$*$b$C$?$o$1$G$9(J$@!#(J
 |
 |$@$b$A$m$s(JP(x)$@$O%b%G%k$K0MB8$7$J$$$b$N$H$7$^$9!#(J

$@%b%G%k$r6qBNE*$K$H$i$J$$$H$G$-$J$$$G$9!#(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.92Nov30190959@whale.ryukoku.ac.jp>
Path: arc1-ca.pugleaf.net!sparky!uunet!ccut!sh.wide!wnoc-kyo!kuis!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>

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-11-30 03:05:48 PST
Path: arc1-ca.pugleaf.net!sparky!uunet!ccut!sh.wide!wnoc-kyo!kuis!rins!satoshi
From: satoshi@whale.ryukoku.ac.jp (Satoshi Kobayashi)
Newsgroups: fj.sci.math
Subject: Re: Q in intuitionistic math.
Message-ID: <SATOSHI.92Nov30190959@whale.ryukoku.ac.jp>
Date: 30 Nov 92 10:09:59 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>
Sender: news@rins.ryukoku.ac.jp
Distribution: fj
Organization: Ryukoku Univ., Seta, Japan
Lines: 69
In-reply-to: shingo@ipc02.rtri.or.jp's message of 27 Nov 92 10:45:49 GMT