빈 타입

유형 이론에서 빈 유형 또는 부조리 유형(일반적으로 $0{\displaystyle \mathbb{}}$ ${\$은 항이 없는 유형입니다.이러한 유형은 귀무 공생(nullary coproduct)으로 정의될 수 있습니다(즉, 유형 없음의 분리 합).^[1]폴리모픽 유형 ∀ t${\displaystyle .t}$ ${\displaystyle \forall$ t$.t}$로 정의할 수도 있습니다.

임의의 유형 $P$ ${\displaystyle P}$에 대해$$유형 ¬ ${\displaystyle P}$ ${\displaystyle \neg P}$는 ${\displaystyle P}$ → 0 ${\displaystyle P\to \mathbb {0}}($으)로 정의됩니다$.$ 표기법에서 알 수 있듯이, $유형$ 0 ${\displaystyle \mathbb {0}}$의 항은 잘못된 명제이고, 유형 ¬ ${\displaystyle P}$ ${\displaystyle \neg P}$의 항은 명제 P의 반증입니다.

형식 이론에 빈 형식을 포함할 필요는 없습니다.빈 형식은 일반적으로 고유하지 않습니다.^[2]예를 들어 ${\displaystyle T}$ → 0 ${\displaystyle T\to \mathbb {0}}$도 $거주$하는 T ${\displaystyle$ T$}$에 대해 사용할 수 없습니다$.$

형식 시스템에 빈 형식이 포함되어 있으면 맨 아래 형식도 사람이 살지 않아야 하므로 구분이 없으며 둘 다 ⊥ ${\displaystyle \bot}($으)로 표시됩니다$.$

참고문헌