원자 초기 시퀀스의 완전성
Completeness of atomic initial sequents시퀀스 미적분학에서, 원자 초기 시퀀스의 완전성은 초기 시퀀스 ⊢(여기서는 임의의 공식)은 오직 원자 초기 시퀀스 formula(여기서는 원자 공식)에서만 파생될 수 있다고 명시한다.이 정리는 람다 미적분학의 eta 확장과 유사한 역할을 하며, 컷-리밍과 베타 감소에는 이중 역할을 한다.전형적으로 그것은 절단 제거보다 훨씬 더 쉽게 , 의 구조에 유도를 통해 확립될 수 있다.
참조
- 가이시 다케우티.증명 이론.논리와 수학의 기초에 관한 연구 제81권.1975년 암스테르담 노스홀랜드.
- 앤 스저프 트로엘스트라와 헬무트 슈히치텐베르크.기본 증명 이론.판본: 2, 삽화, 수정.2000년 캠브리지 대학 출판부에서 발행하였다.