抜き打ちテストのパラドックスの形式化