🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: fj.sci.math
Article #209

Re: Q in intutionistic math.

#209
From: Satoshi Kobayashi
Date: Wed, 11 Nov 1992 06:18
51 lines
3279 bytes
$@>.NSAo(J@$@N6C+Bg3X$G$9!#@P86$5$s$N5-;v$K>/$7$@$1JdB-$7$^$9(J$@!#(J

In article <ISHIHARA.92Nov5101428@is15e0s10.jaist-east.ac.jp> ishihara@is15e0s10.jaist-east.ac.jp (Hajime Ishihara) writes:

 |   >>$@D>4Q<g5A$G$O(J not(not(A)) -> A $@$,F3$1$^$;$s!#$=$lL5$7$G!"(J
 |   >>not(A) or not(not(A)) -> A or not(A) $@!JJX59>e(J[1]$@$H$7$^$9!K(J
 |   >>$@$rF3$/$3$H$,$G$-$?$C$1!)(J
 |   >>$@$H!"$$(J$@$&5?Ld$G$9!#(J
 |   >>
 |   >>[1] $@$,$$$($J$$$N$J$i$P!"(Jnot(A) or not(not(A)) $@$,0lHL$K=P$F$-$?$H$7$F$b(J
 |   >>$@JL$K:$$i$J$$$+$i$G$9!#(J
 |
 |$@3N$+!"(JA or not(A) <=> not(not(A)) -> A + not(A) or not(not(A)) $@$G$9!#(J

$@8D!9$N(J A $@$K$D$$$F$O3N$+$K$=$&$G$9$M!#$D$^$j!"8D!9$N(J A $@$K$D$$$F$O!"(J
  A or not(A) <=> (not(not(A)) -> A) and (not(A) or not(not(A)))
$@$,@.$jN)$A$^$9!#(J($@$3$l$OEv$?$jA0$G$9$M!#(J)
(not(not(A)) -> A) => A or not(A)$@$O0lHL$K$O%@%a!#(J
(not(A) or not(not(A))) => A or not(A) $@$b!"0lHL$K$O%@%a!#(J

$@0lJ}!"(JA or not(A) $@$H(J$@$+!"(J not(not(A)) -> A $@$H$+!"(J not(A) or
not(not(A))$@$H$+$,!"8xM}%9%-!<%^$rI=$9$N$J$iOC$O>/$70c$C$F$-(J
$@$F(J$@!"!V$9$Y$F$NO@M}<0(J A $@$K$D$$$F(J A or not(A) $@$r8xM}$H$9$k!W$3(J
$@$H$H!"!V$9$Y$F$NO@M}<0(J A $@$K$D$$$F(J not(not(A)) -> A $@$r8xM}$H(J
$@$9$k!W$3$H$H$OF1Ey$G$9$M!#(J
$@$=$&$$$&0UL#$G$O!"(J
  A or not(A) <=> not(not(A)) -> A
$@$G(J$@$9!#(J
$@$7$+$7!"!V$9$Y$F$N(J A $@$K$D$$$F(J not(A) or not(not(A)) $@$rG'$a$k!W(J
$@$3$H$O$3$l$i$h$j$b<e$$(J principle $@$G$9$M!#(J

($@$3$&$$$&$3$H$O@P86$5$s$O$9$G$K$4B8CN$N$3$H$H;W$$$^$9$,!"0l(J
$@HL$NFI<T$NJ}!9$K$H$C$F$O!"8xM}%9(J$@%-!<%^$NOC$+!"8D!9$N(J A $@$K$D(J
$@$$$F$NOC$+$o$+$j$K$/$$$+$J!"$H;W$C$?$N$G!"JdB-$7$F$_$^$7$?!#(J)

 |$@Nc$($P!"(J$@$"$k(J($@8EE5E*(J)$@DjM}$rD>4Q<g5A!V$G!W>ZL@$7$h$&$H$7$^$9!#(J
 |$@$H$3$m$,!"$I$&$d$C$F$_$F$b>ZL@$G$-$=$&$b$"$j$^(J$@$;$s!#(J
 |$@$3$&$$$&>l9g!">ZL@$G$-$J$$;v$r>ZL@$7$J$1$l$P$J$j$^$;$s!#(J
 |$@$5$i$K!"(J($@;d$O(J)$@$I$NDxEY>ZL@$7$K$/$$(J$@$N$+!)(J
 |
 | A or not(A) $@$/$i$$$+!)(J not(A) or not(not(A)) $@$/$i$$$+!)(J
 |$@$O$?$^$?(J not(not(A)) -> A $@$/$i(J$@$$$+!)(J $@$=$N$$$E$l$G$b$J$$$+!)(J

$@$3$l$b$^$?!"8xM}%9%-!<%^$NOC$@$H$9$l$P!"!V(JA or not(A) $@$/$i$$!W(J
$@$H!V(Jnot(not(A)) -> A $@$/$i$$!W$OF1$8$K$J$C$F$7$^$$$^$9$M!#(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.92Nov11151829@whale.ryukoku.ac.jp>
Path: arc1-ca.pugleaf.net!sparky!uunet!ccut!s.u-tokyo!kuis!rins!satoshi
References: <ISHIHARA.92Oct30100417@is15e0s10.jaist-east.ac.jp> <1992Oct31.052546.28018@kudpc.kyoto-u.ac.jp> <RYU.92Nov2131119@sysipk.sys.titech.ac.jp> <1992Nov2.074326.17262@kudpc.kyoto-u.ac.jp> <RYU.92Nov4105137@sysipk.sys.titech.ac.jp> <ISHIHARA.92Nov5101428@

Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!sparky!uunet!ccut!s.u-tokyo!kuis!rins!satoshi
From: satoshi@whale.ryukoku.ac.jp (Satoshi Kobayashi)
Newsgroups: fj.sci.math
Subject: Re: Q in intutionistic math.
Message-ID: <SATOSHI.92Nov11151829@whale.ryukoku.ac.jp>
Date: 11 Nov 92 06:18:29 GMT
References: <ISHIHARA.92Oct30100417@is15e0s10.jaist-east.ac.jp>
 <1992Oct31.052546.28018@kudpc.kyoto-u.ac.jp>
 <RYU.92Nov2131119@sysipk.sys.titech.ac.jp>
 <1992Nov2.074326.17262@kudpc.kyoto-u.ac.jp>
 <RYU.92Nov4105137@sysipk.sys.titech.ac.jp>
 <ISHIHARA.92Nov5101428@
Sender: news@rins.ryukoku.ac.jp
Organization: Ryukoku Univ., Seta, Japan
Lines: 51
In-reply-to: ishihara@is15e0s10.jaist-east.ac.jp's message of 5 Nov 92 01:14:28 GMT