통합검색

한 줄의 계산이 다음 줄을 낳으면 일반 증명이 될까?

11세기 알카라지와 12세기 알사마왈의 대수 저술에는 한 차수의 계산에서 다음 차수로 나아가는 절차가 나타난다. 현존 저술과 후대의 인용, 현대 연구자의 재구성을 구분하면서 이항계수 배열과 세제곱 합 공식을 검산하고, 반복되는 계산이 언제 일반 명제의 증명이 되는지 살펴본다.

증명은 결론에 들어 있는 개념만으로 다시 쓸 수 있을까요?

게르하르트 겐첸의 「Untersuchungen über das logische Schließen」 I–II(1935)를 따라, 자연연역과 시퀀트 계산에서 컷 제거와 부분식 성질이 증명의 정보를 어떻게 드러내는지 읽습니다. 14개의 문답, 15개의 생각그림과 세 가지 실험을 담았습니다.

Gerhard Gentzen, Untersuchungen über das logische Schließen I–II (1935)

산술의 증명은 끝없이 내려갈 수 있을까요?

게르하르트 겐첸의 「Die Widerspruchsfreiheit der reinen Zahlentheorie」(1936)를 따라, 산술 증명에 ε₀ 아래 순서수 표기를 붙이고 환원 때마다 값이 감소한다는 사실에서 무모순성을 얻는 과정을 읽습니다. 14개의 문답, 15개의 생각그림과 세 가지 실험을 담았습니다.

Gerhard Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie (1936)

증명 속 중간정리를 모두 걷어내도, 같은 결론에 도달할 수 있을까요?

다케우치 가이시의 《On a Generalized Logic Calculus》(1953)를 따라, 시퀀트와 컷에서 근본 추측, 증명된 보존 정리와 후속 쟁점까지 읽습니다. 14개의 문답, 15개의 생각그림과 세 가지 실험을 담았습니다.

Gaisi Takeuti, On a Generalized Logic Calculus (1953)

컷을 직접 지우지 않고도, 컷 없는 증명이 있다고 보일 수 있을까요?

다카하시 모토오의 《A proof of cut-elimination theorem in simple type-theory》(1967)를 따라, V-complex와 V-correspondence에서 람다 추상, 건전성과 반모형을 통한 비구성적 컷 제거 증명까지 읽습니다. 14개의 문답, 15개의 생각그림과 세 가지 실험을 담았습니다.

Moto-o Takahashi, A proof of cut-elimination theorem in simple type-theory (1967)