원자 초기 시퀀스의 완전성

Completeness of atomic initial sequents

시퀀스 미적분학에서, 원자 초기 시퀀스의 완전성은 초기 시퀀스 ⊢(여기서는 임의의 공식)은 오직 원자 초기 시퀀스 formula(여기서는 원자 공식)에서만 파생될 수 있다고 명시한다.이 정리는 람다 미적분학eta 확장과 유사한 역할을 하며, 컷-리밍베타 감소에는 이중 역할을 한다.전형적으로 그것은 절단 제거보다 훨씬 더 쉽게 , 의 구조에 유도를 통해 확립될 수 있다.

참조