使える公理を少なくしたら証明できる命題は少なくなるんだから