힐베르트 스타일과 자연 연역의 차이가 의미하는 바가 뭘까요?

[익명(119.203)]

논리학을 공리화하는 두 가지 방식은 차이가 많겠지만 일단 가장 큰 차이는 힐베르트 스타일의 기본 대상은 논리식이고,

자연 연역의 기본 대상은 sequent라는게 가장 큰 차이라고 생각하는데

이 차이가 의미하는 바가 뭘까요?

[PaulSohn(paulsohn)]

그 관점에서는 일단 추가가정을 통한 문맥의 변경이 있느냐(자연연역) 추가가정을 전부 문장으로 묶어서 들고가느냐(힐베르트연역) 정도의 차이는 있겠죠. 증명력으로서는 둘이 똑같지만, 계산론 쪽으로 가면 자연연역은 typed lambda에, 힐베르트연역은 combinator에 대응하겠고요.

[익명(119.203)]

글 썼던 것을 잊어서, 확인이 늦었습니다. 좋은 답변 감사드립니다. 계산 이론 쪽은 몰라서 ㅠ아쉽지만 이해할 수가 없네요. 더 공부하고 다시 덧글을 읽어보겠습니다.