순서론 과 논리학 에서 헤이팅 대수 (영어 : Heyting algebra )는 직관 논리 의 명제들의 격자 와 유사한 성질을 갖는 격자 이다. 고전 논리를 나타내는 불 대수 에서 일부 조건을 약화시켜 얻은 개념이다.
헤이팅 대수 (영어 : Heyting algebra )는 다음 조건을 만족시키는 이항 연산
⟹ ⟹ -->
: : -->
H
× × -->
H
→ → -->
H
{\displaystyle \implies \colon H\times H\to H}
유계 격자
(
H
,
≤ ≤ -->
,
∧ ∧ -->
,
∨ ∨ -->
,
⊤ ⊤ -->
⊥ ⊥ -->
,
⟹ ⟹ -->
)
{\displaystyle (H,\leq ,\land ,\lor ,\top \,\bot ,\implies )}
(함의의 성질) 모든
a
,
b
,
c
∈ ∈ -->
H
{\displaystyle a,b,c\in H}
c
∧ ∧ -->
a
≤ ≤ -->
b
{\displaystyle c\land a\leq b}
c
≤ ≤ -->
a
⟹ ⟹ -->
b
{\displaystyle c\leq a\implies b}
동치 이다. 주어진 격자
(
H
,
≤ ≤ -->
,
∧ ∧ -->
,
∨ ∨ -->
)
{\displaystyle (H,\leq ,\land ,\lor )}
범주론 적으로 다음과 같이 기술할 수 있다. 헤이팅 대수 는 다음 조건을 만족시키는 (범주로 간주한) 부분 순서 집합
(
P
,
≤ ≤ -->
)
{\displaystyle (P,\leq )}
(
∧ ∧ -->
{\displaystyle \land }
⊤ ⊤ -->
{\displaystyle \top }
극한 이 존재한다.
(
∨ ∨ -->
{\displaystyle \lor }
⊥ ⊥ -->
{\displaystyle \bot }
쌍대극한 이 존재한다.
(
⟹ ⟹ -->
{\displaystyle \implies }
P
{\displaystyle P}
데카르트 닫힌 범주 이다. 헤이팅 대수에서의 부정
¬ ¬ -->
: : -->
H
→ → -->
H
{\displaystyle \lnot \colon H\to H}
¬ ¬ -->
a
=
a
⟹ ⟹ -->
⊥ ⊥ -->
{\displaystyle \lnot a=a\implies \bot }
다음과 같은 함의 관계가 성립한다.
헤이팅 대수
H
{\displaystyle H}
동치 이다.
H
{\displaystyle H}
불 대수 이다.(이중 부정의 삭제)
¬ ¬ -->
¬ ¬ -->
: : -->
H
→ → -->
H
{\displaystyle \lnot \lnot \colon H\to H}
항등 함수 이다.
(배중률 ) 모든 원소
a
∈ ∈ -->
H
{\displaystyle a\in H}
a
∨ ∨ -->
¬ ¬ -->
a
=
⊤ ⊤ -->
{\displaystyle a\lor \lnot a=\top }
불 대수 는 헤이팅 대수를 이룬다. 이 경우, 함의 연산은
a
⟹ ⟹ -->
b
=
¬ ¬ -->
a
∨ ∨ -->
b
{\displaystyle a\implies b=\lnot a\lor b}
이다.
위상 공간
X
{\displaystyle X}
열린집합 들의 (포함 관계에 대한) 부분 순서 집합 은 완비 헤이팅 대수를 이룬다. 이 경우 헤이팅 대수의 각 연산은 다음과 같다.
위상수학
완비 헤이팅 대수
U
⊂ ⊂ -->
V
{\displaystyle U\subset V}
U
≤ ≤ -->
V
{\displaystyle U\leq V}
X
{\displaystyle X}
⊤ ⊤ -->
{\displaystyle \top }
∅ ∅ -->
{\displaystyle \varnothing }
⊥ ⊥ -->
{\displaystyle \bot }
U
∩ ∩ -->
V
{\displaystyle U\cap V}
U
∧ ∧ -->
V
{\displaystyle U\land V}
U
∪ ∪ -->
V
{\displaystyle U\cup V}
U
∨ ∨ -->
V
{\displaystyle U\lor V}
int
-->
(
⋂ ⋂ -->
α α -->
U
α α -->
)
{\displaystyle \textstyle \operatorname {int} \left(\bigcap _{\alpha }U_{\alpha }\right)}
⋀ ⋀ -->
α α -->
U
α α -->
{\displaystyle \textstyle \bigwedge _{\alpha }U_{\alpha }}
⋃ ⋃ -->
α α -->
U
α α -->
{\displaystyle \textstyle \bigcup _{\alpha }U_{\alpha }}
⋁ ⋁ -->
α α -->
U
α α -->
{\displaystyle \textstyle \bigvee _{\alpha }U_{\alpha }}
int
-->
(
(
X
∖ ∖ -->
U
)
∪ ∪ -->
V
)
{\displaystyle \operatorname {int} \left((X\setminus U)\cup V\right)}
U
⟹ ⟹ -->
V
{\displaystyle U\implies V}
int
-->
(
X
∖ ∖ -->
U
)
{\displaystyle \operatorname {int} (X\setminus U)}
¬ ¬ -->
U
{\displaystyle \lnot U}
직관 명제 논리 에서, 명제들의 격자는 헤이팅 대수를 이룬다. 마찬가지로, 모든 헤이팅 대수는 어떤 초직관 논리 의 명제 격자와 동형이다.
(작은) 토포스 에서, 모든 대상의 부분 대상 의 부분 순서 집합 은 헤이팅 대수를 이룬다. 즉, 토포스의 내부 논리는 직관 논리 이다.
아런트 헤이팅 이 직관 논리 를 형식화하기 위하여 도입하였다.[ 1] [ 2] [ 3]
↑ 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 . ↑ 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 . ↑ 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 .
