헤이팅 대수 문서 원본 보기

{{위키데이터 속성 추적}}
{{대수 구조}}
[[순서론]]과 [[논리학]]에서 '''헤이팅 대수'''({{llang|en|Heyting algebra}})는 [[직관 논리]]의 명제들의 [[격자 (순서론)|격자]]와 유사한 성질을 갖는 [[격자 (순서론)|격자]]이다. 고전 논리를 나타내는 [[불 대수]]에서 일부 조건을 약화시켜 얻은 개념이다.

== 정의 ==
'''헤이팅 대수'''({{llang|en|Heyting algebra}})는 다음 조건을 만족시키는 이항 연산 <math>\implies\colon H\times H\to H</math>이 갖추어져 있는 [[유계 격자]] <math>(H,\le,\land,\lor,\top\,\bot,\implies)</math>이다.
* (함의의 성질) 모든 <math>a,b,c\in H</math>에 대하여, <math>c\land a\le b</math>와 <math>c\le a\implies b</math>가 서로 [[동치]]이다.
주어진 격자 <math>(H,\le,\land,\lor)</math> 위에 헤이팅 대수 구조가 존재한다면, 이 구조는 유일하다. 헤이팅 대수의 정의는 [[범주론]]적으로 다음과 같이 기술할 수 있다. '''헤이팅 대수'''는 다음 조건을 만족시키는 (범주로 간주한) [[부분 순서 집합]] <math>(P,\le)</math>이다.
* (<math>\land</math> 및 <math>\top</math>의 존재) 모든 유한 [[극한 (범주론)|극한]]이 존재한다.
* (<math>\lor</math> 및 <math>\bot</math>의 존재) 모든 유한 [[쌍대극한]]이 존재한다.
* (<math>\implies</math>의 존재) <math>P</math>는 [[데카르트 닫힌 범주]]이다.

헤이팅 대수에서의 '''부정''' <math>\lnot\colon H\to H</math>은 최소 원소(거짓)를 함의하는 것이다.
:<math>\lnot a=a\implies\bot</math>

== 성질 ==
=== 함의 관계 ===
다음과 같은 함의 관계가 성립한다.
:{| style="text-align: center"
|| || || || || [[완비 격자]] || ⇐ || [[완비 헤이팅 대수]] ||  ⇐ || [[완비 불 대수]]
|-
|| || || || || || || || || ⇓
|-
|| || || || || ⇓ || || ⇓ || || [[시그마 대수]]
|-
|| || || || || || || || || ⇓
|-
| [[원순서 집합]] || ⇐ || [[부분 순서 집합]] || ⇐ || [[유계 격자]] || ⇐ || 헤이팅 대수 || ⇐ || [[불 대수]]
|}

=== 불 대수가 될 조건 ===
헤이팅 대수 <math>H</math>에 대하여, 다음 조건들이 서로 [[동치]]이다.
* <math>H</math>는 [[불 대수]]이다.
* (이중 부정의 삭제) <math>\lnot\lnot\colon H\to H</math>는 [[항등 함수]]이다.
* ([[배중률]]) 모든 원소 <math>a\in H</math>에 대하여, <math>a\lor\lnot a=\top</math>이다.

== 예 ==
[[불 대수]]는 헤이팅 대수를 이룬다. 이 경우, 함의 연산은
:<math>a\implies b=\lnot a\lor b</math>
이다.

[[위상 공간 (수학)|위상 공간]] <math>X</math>의 [[열린집합]]들의 (포함 관계에 대한) [[부분 순서 집합]]은 [[완비 격자|완비]] 헤이팅 대수를 이룬다. 이 경우 헤이팅 대수의 각 연산은 다음과 같다.
{| class="wikitable"
|-
! 위상수학 !! 완비 헤이팅 대수
|-
| <math>U\subset V</math> || <math>U\le V</math>
|-
| <math>X</math> || <math>\top</math>
|-
| <math>\varnothing</math> || <math>\bot</math>
|-
| <math>U\cap V</math> || <math>U\land V</math>
|-
| <math>U\cup V</math> || <math>U\lor V</math>
|-
| <math>\textstyle\operatorname{int}\left(\bigcap_\alpha U_\alpha\right)</math> || <math>\textstyle\bigwedge_\alpha U_\alpha</math>
|-
| <math>\textstyle\bigcup_\alpha U_\alpha</math> || <math>\textstyle\bigvee_\alpha U_\alpha</math>
|-
| <math>\operatorname{int}\left((X\setminus U)\cup V\right)</math> || <math>U\implies V</math>
|-
| <math>\operatorname{int}(X\setminus U)</math> || <math>\lnot U</math>
|}

[[직관 논리|직관]] [[명제 논리]]에서, 명제들의 격자는 헤이팅 대수를 이룬다. 마찬가지로, 모든 헤이팅 대수는 어떤 [[초직관 논리]]의 명제 격자와 동형이다.

(작은) [[토포스]]에서, 모든 대상의 [[부분 대상]]의 [[부분 순서 집합]]은 헤이팅 대수를 이룬다. 즉, 토포스의 내부 논리는 [[직관 논리]]이다.

== 역사 ==
[[아런트 헤이팅]]이 [[직관 논리]]를 형식화하기 위하여 도입하였다.<ref>{{저널 인용|성=Heyting|이름=A.|저자링크=아런트 헤이팅|날짜=1930|제목=Die formalen Regeln der intuitionistischen Logik I|저널=Sitzungsberichte der Königlich Preussischen Akademie der Wissenschaften zu Berlin|쪽=42–56|jfm=56.0823.01}}</ref><ref>{{저널 인용|성=Heyting|이름=A.|저자링크=아런트 헤이팅|날짜=1930|제목=Die formalen Regeln der intuitionistischen Logik II|저널=Sitzungsberichte der Königlich Preussischen Akademie der Wissenschaften zu Berlin|쪽=57–71|jfm=56.0823.01}}</ref><ref>{{저널 인용|성=Heyting|이름=A.|저자링크=아런트 헤이팅|날짜=1930|제목=Die formalen Regeln der intuitionistischen Logik III|저널=Sitzungsberichte der Königlich Preussischen Akademie der Wissenschaften zu Berlin|쪽=158–169|jfm=56.0823.01}}</ref>

== 같이 보기 ==
* [[초직관 논리]]

== 각주 ==
{{각주}}

== 외부 링크 ==
* {{eom|title=Brouwer lattice}}
* {{매스월드|id=HeytingAlgebra|title=Heyting algebra}}
* {{nlab|id=Heyting algebra}}
* {{nlab|id=HeytAlg}}

{{전거 통제}}

[[분류:격자 이론]]
[[분류:구성주의 (수학)]]
[[분류:수리논리학]]