질문이 다소 황당할 수 있겠지만, herbrand theorem을 second-order logic에서 증명할 때 skolem normal form을 이용하지 않고도 증명할 수 있나요?