>>708
‚Ά‚α‚ ˆΣ–‘˜_‚Α‚Δ‰½‚ΜˆΣ–‘‚ͺ‚ ‚ι‚́H‚ ‚ƁAŒ‹‹ΗŽΐ”˜_‚Μ‰πŽίi\‘’j‚Ν‚Η‚€‚Θ‚ι‚ρ‚Ύ‚ζB
DedekindŽΐ”˜_‚πˆΘ‰Ί‚ΜŒφ—‚Ε’θ‹`‚·‚ι‚Ζ‚«A‚»‚Μ‰πŽί‚π‚Π‚Ζ‚Β—αŽ¦‚΅‚Δ‚έ‚Δ‚Ω‚΅‚’B
P‚π”CˆΣ‚̏qŒκ‚Ζ‚΅‚Δ
E1. Νx(x=x)
E2. ΝxΝy(x=yΘP(x)ΛP(y))
F1. ΝxΝyΝz((x+y)+z=x+(y+z))
F2. ΝxΝy(x+y=y+x)
F3. Νx(x+0=x)
F4. Νx(x+(-x)=0)
F5. ΝxΝyΝz((x*y)*z=x*(y*z))
F6. ΝxΝy(x*y=y*x)
F6. Νx(x*1=x)
F7. Νx(Κx=0Λx*x^(-1)=1)
F8. ΝxΝyΝz(x*(y+z)=x*y+x*z)
O2. ΝxΝy(x…yΘy…xΛx=y)
O3. ΝxΝyΝz(x…yΘy…zΛx…z)
O4. ΝxΝy(x…yΙy…x)
OF1. ΝxΝyΝz(x…yΛx+z…y+z)
OF2. ΝxΝyΝz(x…yΘ0…zΛxz…yz)
C1. ΝxΝy(P(x)ΘΚP(y)Λx…y)
@@@ ΛΞzΝxΝy(P(x)ΘΚP(y)Λ(x…z…y))
‚Α‚Δ‚’‚ν‚κ‚½‚Ζ‚«‚Ι‚‘A‚Ά‚α‚Ÿ‘ΞΫ—Μˆζ‚ͺ‹K’θ‚Ε‚«‚Θ‚’‚Ά‚α‚Θ‚’I‚Α‚Δ‚½‚΅‚©‹C‚Γ‚­‚ΖŽv‚€‚ρ‚Ε‚·‚―‚Η‚ΰ‚§A