Logic-ml $B$N3'MM!$(B

$B$3$s$P$s$O!$ElKLBg3X$NKYH*2B9($G$9!%(B 7$B7n(B20$BF|!J6b!K$KElKLBg3X$K$F2<5-%;%_%J!<$r9T$$$^$9$N$G!$6=L#$N$"$kJ}$O$<$R$4;22C$/$@$5$$!%(B $BFs9V1i$4$6$$$^$9!%(B

************************************************************************* $BF|;~!'(B7$B7n(B20$BF|!J6b!K(B15:30$B!A(B17:00 $B>l=j!'ElKLBg3X(B $BKL@DMU;3%-%c%s%Q%9(B $BM}3X9gF1Eo(B 1201$B9f<<(B

$B-!(B15:30$B!A(B16:00 $B9V1i<T!'(B $B;3:j!!Ip(B $B!J(B $BElKLBg3XBg3X1!!&M}3X8&5f2J(B $B!K(B

$B%?%$%H%k!'(B The Optimal Bounded Marriage Theorem

$B%"%V%9%H%i%/%H!'(B J. Hirst showed that WKL_0 is equivalent over RCA_0 to the assertion that every bounded marriage problem satisfying Hall condition has a solution. In this talk, arranging the result, we mainly prove that ACA_0 is equivalent over RCA_0 to the assertion that every bounded marriage problem of the finite total utility satisfying Hall condition has an optimal solution.

$B-"(B16:00$B!A(B17:00 $B9V1i<T!'(B $B2,K\(B $B7=;K(B $B!J@gBf9bEy@lLg3X9;!&Am9g2J3X7O!K(B

$B%?%$%H%k!'(B $BL?BjMMAj&L7W;;$N0l3,3HD%$K$D$$$F(B

$B%"%V%9%H%i%/%H!'(B $BK\H/I=$G$O!$0l3,MMAj&L7W;;(B($BL?BjMMAj&L7W;;$N0l3,3HD%(B)$B$H$=$N<~JU>u67$K$D$$$F2r@b$9$k!%$^$:!$0l3,MMAj&L7W;;$r9=C[$9$k$K;j$kGX7J$H$7$F!$7A<0<jK!$K$D$$$F=R$Y$k!%(B $B<!$K!$L?BjMMAj&L7W;;$H0l3,=R8lO@M}$r9g$o$;$F!$0l3,MMAj&L7W;;$rDj5A$9$k!%$=$N8e!$0l3,MMAj&L7W;;$N@-<A$N$&$A!$40A4@-$HI=8=NO$K$D$$$F=R$Y$k!%$5$i$K!$0l3,MMAj&L7W;;$NE,MQNc$H$7$F!$%;%^%U%)$K$h$kAj8_GS=|$NBEEv@->ZL@$r>R2p$9$k!%:G8e$K!$$^$H$a$H4XO"2]Bj$N>R2p$r9T$&!%(B

*************************************************************************

$B0J>e$G$9!%(B $B%;%_%J!<>pJs$N>:YEy$O2<5-@gBf%m%8%C%/$N%[!<%`%Z!<%8$+$i$b$4Mw$$$?$@$1$^$9!%(B https://sites.google.com/site/sendailogichomepage/

$BKYH*!!2B9((B -- -- $BElKLBg3XBg3X1!!!M}3X8&5f2J(B $B?t3X@l96!!;:3X41O"7H8&5f0w(B E-mail: [email protected]